******************************************************* Listing of SPARK Text SPARK95 Examiner with VC and RTC Generator Release 7.3 / 01.06 Demonstration Version ******************************************************* DATE : 28-FEB-2010 12:47:45.24 Line 1 --# main_program; 2 procedure Main 3 --# derives ; 4 is 5 procedure AC1(X : in out Float; I: in Integer; 6 M : out Boolean ) 7 --# derives X from *, I & M from I; 8 is begin 9 M := True; 10 end AC1; !!! ( 1) Flow Error : 35: Importation of the initial value of variable X is ineffective [Explanatory note: The meaning of this message is explained in Section 4.2 of Appendix A]. !!! ( 2) Flow Error : 31: The variable X is exported but not (internally) defined. !!! ( 3) Flow Error : 30: The variable I is imported but neither referenced nor exported. !!! ( 4) Flow Error : 50: X is not derived from the imported value(s) of X, I [Explanatory note: The item before "is not derived ..." is an export or function return value and the item(s) after are imports of the subprogram. The message indicates that a dependency, stated in the dependency relation (derives annotation) or implied by the function signature is not present in the code. The absence of a stated dependency is always an error in either code or annotation.]. !!! ( 5) Flow Error : 50: M is not derived from the imported value(s) of I [Explanatory note: The item before "is not derived ..." is an export or function return value and the item(s) after are imports of the subprogram. The message indicates that a dependency, stated in the dependency relation (derives annotation) or implied by the function signature is not present in the code. The absence of a stated dependency is always an error in either code or annotation.]. 11 -- 12 procedure AC2(X : in out Float; I: in Integer; 13 M : out Boolean ) 14 --# derives X from *, I & M from I; 15 is 16 begin 17 M := I mod 2 = 0; 18 end AC2; !!! ( 6) Flow Error : 35: Importation of the initial value of variable X is ineffective [Explanatory note: The meaning of this message is explained in Section 4.2 of Appendix A]. !!! ( 7) Flow Error : 31: The variable X is exported but not (internally) defined. !!! ( 8) Flow Error : 50: X is not derived from the imported value(s) of X, I [Explanatory note: The item before "is not derived ..." is an export or function return value and the item(s) after are imports of the subprogram. The message indicates that a dependency, stated in the dependency relation (derives annotation) or implied by the function signature is not present in the code. The absence of a stated dependency is always an error in either code or annotation.]. 19 -- 20 procedure AC3(X : in out Float; I: in Integer; 21 M : out Boolean ) 22 --# derives X from *, I & M from I; 23 is 24 begin 25 M := I mod 2 = 0; 26 if M then 27 X:= 2**I; -- conversione implicita 28 end if; 29 end AC3; +++ Flow analysis of subprogram AC3 performed: no errors found. 30 -- 31 procedure AC4(X : out Float; I: in Integer; 32 M : out Boolean ) 33 --# derives X from *, I & M from I; ^9 *** ( 9) Semantic Error :162: Importation of X is incompatible with its parameter mode [Explanatory note: Issued if a parameter appears as an import to a procedure when it is of parameter mode out.]. 34 is 35 begin 36 M := I mod 2 = 0; 37 if M then 38 X:= 2**I; -- conversione implicita 39 end if; 40 end AC4; 41 -- 42 procedure AC5(X : out Float; I: in Integer; 43 M : out Boolean ) 44 --# derives X,M from I; 45 is 46 begin 47 M := I mod 2 = 0; 48 if M then 49 X:= 2**I; -- conversione implicita 50 end if; 51 end AC5; ??? ( 10) Warning :602: The undefined initial value of X may be used in the derivation of X [Explanatory note: Here XXX is a non-imported variable, and YYY is an export, of a procedure subprogram.]. 52 -- 53 procedure AC6(X : out Float; I: in Integer; 54 M : out Boolean ) 55 --# derives X,M from I; 56 is 57 begin 58 M := I mod 2 = 0; 59 if M then 60 X:= 2**I; -- conversione implicita 61 else 62 X := 0.0; 63 end if; 64 end AC6; +++ Flow analysis of subprogram AC6 performed: no errors found. 65 -- 66 procedure AC7(X : out Float; I: in Integer; 67 M : out Boolean ) 68 --# derives X,M from I; 69 is 70 begin 71 M := I mod 2 = 0; 72 if M then 73 X:= 1.0; 74 else 75 X := 0.0; 76 end if; 77 end AC7; +++ Flow analysis of subprogram AC7 performed: no errors found. 78 79 begin 80 null; 81 end Main; +++ Flow analysis of subprogram Main performed: no errors found. --End of file--------------------------------------------------