Download SPARK Toolset Release Note 9

Tool Development and Support
SPARK Toolset Release Note 9
RN
Issue: 3.19
function F1 (X : Integer) return Integer;
--# pre X * X <= Integer'Last and
--#
X * X >= 0 ;
--# return X * X;
6
7
8
9
10
11
12
function F2 ( Y : Integer) return Integer;
--# pre Y * Y <= Integer'Last and
--#
Y * Y >= 0;
--# return Y * Y
begin
return F1 (Y);
end F2;
For path(s) from start to precondition check associated with
statement of line 11:
function_f2_1.
H1:
y * y <= integer__last .
H2:
y * y >= 0 .
H3:
y >= integer__first .
H4:
y <= integer__last .
->
C1:
y * y <= integer__last .
C2:
y * y >= 0 .
C3:
y >= integer__first .
C4:
y <= integer__last .
For path(s) from start to finish:
function_f2_2.
H1:
y * y <= integer__last .
H2:
y * y >= 0 .
H3:
y >= integer__first .
H4:
y <= integer__last .
H5:
y * y <= integer__last .
H6:
y * y >= 0 .
H7:
y >= integer__first .
H8:
y <= integer__last .
H9:
f1(y) >= integer__first .
Page 21 of 51