Documentation

How Polyspace Evaluates Function and Procedure Parameters

Polyspace® applies by-copy semantics and a left-to-right evaluation order for parameter passing. You can use Polyspace to verify your Ada code provided your compiler implements:

  • Left-to-right evaluation for subprogram parameters. Consider the following code.

    1 with ada.integer_text_io; 
    2     use  ada.integer_text_io; 
    3     procedure test1 is 
    4        x,y,z,r : integer; 
    5      
    6       function f (x : integer) return integer 
    7       is 
    8        begin 
    9         z := 0; 
    10        return  x + 1; 
    11      end f; 
    12    begin 
    13      x := 10; 
    14      y := 20; 
    15      z := 10; 
    16      R := y / Z + F(x); 
    17      pragma assert(R = 13); -- green ASRT 
    18      put(R); 
    19    end;
    In this example, Polyspace verification implements left-to-right evaluation and generates a green ASRT check.

  • By-copy semantics for subprogram parameters. Consider the following code.

    1     procedure Test2 
    2     is 
    3      
    4      type Rec is 
    5       record 
    6        F,G: Integer; 
    7       end record; 
    8      
    9       R: Rec; 
    10      Result : Integer; 
    11     
    12      procedure Multiply (X, Y : in Rec; Z : out Rec)
    13        
    14      is 
    15       begin 
    16        z := (0,0); 
    17        Z.F := X.F * Y.F; 
    18        Z.G := X.G * Y.G; 
    19       end Multiply; 
    20     
    21    begin 
    22     R := (10,10); 
    23     Result := 100; 
    24     Multiply (R,R,R); 
    25     Result := Result/R.F; 
    26     pragma assert (Result = 1); -- green ASRT
    27    end Test2; 
    In this example, Polyspace verification implements by-copy semantics and generates a green ASRT check.

The green checks generated indicate that the code conforms to the Ada standard, which states that The execution of a program is erroneous if its effect depends on which mechanism is selected by the implementation. See Formal Parameter Modes.

Was this topic helpful?