We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 360d666 commit 52248e7Copy full SHA for 52248e7
testsuite/gnat2goto/tests/separate_subprog/p.adb
@@ -11,5 +11,7 @@ procedure P (X : in out integer) is
11
Old_X : constant Integer := X;
12
begin
13
Inc (X);
14
+ -- The following assert should succeed if the possibility
15
+ -- overflow is ignored.
16
pragma Assert (X = Old_X + 1);
17
end P;
testsuite/gnat2goto/tests/separate_subprog/test.out
@@ -1,3 +1,3 @@
1
[2] file p-inc.asu line 6 assertion: SUCCESS
2
-[1] file p.adb line 14 assertion: FAILURE
+[1] file p.adb line 16 assertion: FAILURE
3
VERIFICATION FAILED
0 commit comments