Theory of heaps translation (again)

regression-tests/runalldirs

@@ -25,6 +25,7 @@ run_test ./rundir math-arrays  "" -assert -dev -t:60
 run_test ./rundir quantifiers "" -assert -dev -t:60
 run_test ./rundir interpreted-predicates "" -assert -dev -t:60
 run_test ./rundir properties "" -assert -dev -t:60
+run_test ./rundir toh-contract-translation "" -dev -t:60
 #run_test ./rundir ParametricEncoder ""
 
 if [ $ERRORS -ne 0 ]; then

regression-tests/toh-contract-translation/Answers

@@ -0,0 +1,212 @@
+
+get-1.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for get */
+/*@
+  requires p == n && n_init >= 1;
+  ensures ((\result == 0 && 0 >= \old(*n)) || \result >= 0) && r1 == \old(r1) && n_init == \old(n_init) && \old(n) == n;
+*/
+================================================================================
+
+SAFE
+
+get-2.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+java.lang.Exception: Predicate generation failed
+(error "Predicate generation failed")
+Other Error: Predicate generation failed
+
+incdec-1.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for decrement */
+/*@
+  requires \true;
+  ensures a_init == \old(a_init) && b_init == \old(b_init) && a == \old(a) && b == \old(b);
+*/
+/* contracts for increment */
+/*@
+  requires val == a;
+  ensures \old(val) == a && a_init == \old(a_init) && b_init == \old(b_init) && \old(val) == \old(a) && b == \old(b);
+*/
+================================================================================
+
+SAFE
+
+incdec-2.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for decrement */
+/*@
+  requires \true;
+  ensures a_init == \old(a_init) && a == \old(a);
+*/
+/* contracts for increment */
+/*@
+  requires val == a;
+  ensures \old(val) == a && a_init == \old(a_init);
+*/
+================================================================================
+
+SAFE
+
+incdec-3.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+(error "Out of Memory")
+Out of Memory
+
+max-1.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for findMax */
+/*@
+  requires x == a && y == b;
+  ensures ((a_init == \result && \result >= b_init) || (b_init - a_init >= 1 && b_init == \result)) && r == \old(r) && a_init == \old(a_init) && b_init == \old(b_init) && \old(a) == a && \old(b) == b;
+*/
+================================================================================
+
+SAFE
+
+max-2.c
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for findMax */
+/*@
+  requires max == r && x == a && y == b;
+  ensures (\old(b_init) - \old(a_init) >= 1 || \old(a_init) >= \old(b_init)) && a == \old(x) && b == \old(y) && r == \old(max) && \old(a_init) == a_init && \old(b_init) == b_init;
+*/
+================================================================================
+
+SAFE
+
+multadd-1.c
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: The following clause has different terms with the same name (term: b:12)
+main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post).
+
+Warning: The following clause has different terms with the same name (term: result:13)
+main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post).
+
+Warning: The following clause has different terms with the same name (term: a:11)
+main_12(@h_post, a_post, b_post, result_post, a_init_post, b_init_post) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13), addTwoNumbers_post(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13, @h_post, a_post, b_post, result_post, a_init_post, b_init_post).
+
+Warning: The following clause has different terms with the same name (term: b:12)
+addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13).
+
+Warning: The following clause has different terms with the same name (term: result:13)
+addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13).
+
+Warning: The following clause has different terms with the same name (term: a:11)
+addTwoNumbers_pre(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13) :- main39_3(@h, a:11, b:12, result:13, a_init:14, b_init:15, a:11, b:12, result:13).
+
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for addTwoNumbers */
+/*@
+  requires \true;
+  ensures a == \old(a) && b == \old(b) && result == \old(result) && a_init == \old(a_init) && b_init == \old(b_init);
+*/
+/* contracts for multiplyByTwo */
+/*@
+  requires num == a;
+  ensures \old(num) == a && \old(num) == \old(a) && b == \old(b) && result == \old(result) && a_init == \old(a_init) && b_init == \old(b_init);
+*/
+================================================================================
+
+SAFE
+
+multadd-2.c
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+(error "Out of Memory")
+Out of Memory
+
+multadd-3.c
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int_ptr" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for addNumbers */
+/*@
+  requires c == result1 && result == result1;
+  ensures \old(c) == c && a == \old(a) && b == \old(b) && result2 == \old(result2) && a_init == \old(a_init) && b_init == \old(b_init) && c_init == \old(c_init) && \old(c) == result1;
+*/
+/* contracts for multiplyNumbers */
+/*@
+  requires c == result1;
+  ensures \old(c) == \old(result1) && \old(c) == c && a == \old(a) && b == \old(b) && result2 == \old(result2) && a_init == \old(a_init) && b_init == \old(b_init) && c_init == \old(c_init) && \old(c) == result1;
+*/
+================================================================================
+
+SAFE
+
+truck-1.c
+Warning: no definition of function "non_det_int" available
+Warning: no definition of function "non_det_int" available
+(error "Out of Memory")
+Out of Memory
+
+truck-2.c
+
+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+Init:
+                                                             main21_1(emptyHeap, 0, 0, 0, emptyHeap, 0, 0, 0)                                                              
+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+                                                                                     |                                                                                     
+                                                                                     |                                                                                     
+                                                                                     V                                                                                     
+ main46_22(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Truck(Truck(5, nthAddr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, emptyHeap, 0, 0, 0, 1) 
+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+Final:
+ main46_22(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Truck(Truck(5, nthAddr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, emptyHeap, 0, 0, 0, 1) 
+---------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+Failed assertion:
+
+UNSAFE

regression-tests/toh-contract-translation/get-1.c

@@ -0,0 +1,34 @@
+
+int r1;
+int n_init;
+
+/*@contract@*/
+int get(int* p) {
+    if (*p <= 0) {
+        return 0;
+    } else {
+        *p = *p - 1;
+        return 1 + get(p);
+    }
+}
+
+int* n;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  r1 = non_det_int();
+  n_init = non_det_int();
+  n = non_det_int_ptr();
+
+  assume((n_init > 0));
+
+  n = (int*) malloc(sizeof(*n));
+  *n = n_init;
+  r1 = get(n);
+
+  assert(((r1 >= n_init) && (r1 <= n_init)));
+}

regression-tests/toh-contract-translation/get-2.c

@@ -0,0 +1,34 @@
+
+int r1;
+int n_init;
+
+
+int get(int* p) {
+    if (*p <= 0) {
+        return 0;
+    } else {
+        *p = *p - 1;
+        return 1 + get(p);
+    }
+}
+
+int* n;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  r1 = non_det_int();
+  n_init = non_det_int();
+  n = non_det_int_ptr();
+
+  assume((n_init > 0));
+
+  n = (int*) malloc(sizeof(*n));
+  *n = n_init;
+  r1 = get(n);
+
+  assert(((r1 >= n_init) && (r1 <= (n_init * n_init))));
+}

regression-tests/toh-contract-translation/incdec-1.c

@@ -0,0 +1,40 @@
+int a_init;
+int b_init;
+
+/*@contract@*/
+void increment(int* val) {
+    (*val)++;
+}
+
+/*@contract@*/
+void decrement(int* val) {
+    (*val)--;
+}
+
+int *a;
+int *b;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  a_init = non_det_int();
+  b_init = non_det_int();
+  a = non_det_int_ptr();
+  b = non_det_int_ptr();
+
+  assume(1);
+
+  a = (int*) malloc(sizeof(*a));
+  b = (int*) malloc(sizeof(*b));
+
+  *a = a_init;
+  *b = b_init;
+
+  increment(a);
+  decrement(b);
+
+  assert(((*a == (a_init + 1)) && (*b == (b_init - 1))));
+}

regression-tests/toh-contract-translation/incdec-2.c

@@ -0,0 +1,34 @@
+int a_init;
+
+/*@contract@*/
+void increment(int* val) {
+    (*val)++;
+}
+
+/*@contract@*/
+void decrement(int* val) {
+    (*val)--;
+}
+
+int *a;
+
+extern int non_det_int();
+extern int* non_det_int_ptr();
+
+void main()
+{
+  //Non-det assignment of global variables
+  a_init = non_det_int();
+  a = non_det_int_ptr();
+
+  assume(1);
+
+  a = (int*) malloc(sizeof(*a));
+
+  *a = a_init;
+
+  increment(a);
+  decrement(a);
+
+  assert((*a == a_init));
+}