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 75331b6 commit 486fd49Copy full SHA for 486fd49
regression/contracts/function_check_05/main.c
@@ -0,0 +1,16 @@
1
+#include <assert.h>
2
+
3
+int foo(int* x)
4
+__CPROVER_ensures(__CPROVER_return_value == 1)
5
+{
6
+ *x = 1;
7
+ return 1;
8
+}
9
10
+int main() {
11
+ int y = 0;
12
+ int z = foo(&y);
13
+ assert(y == 0);
14
+ assert(z == 1);
15
+ return 0;
16
regression/contracts/function_check_05/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG # Contract checking does not properly havoc function calls
+main.c
+--check-code-contracts
+^\[main.assertion.1\] assertion x == 0: FAILURE$
+^\[main.assertion.2\] assertion y == 1: SUCCESS$
+^\[foo.1\] : SUCCESS$
+^VERIFICATION SUCCESSFUL$
0 commit comments