From 971f95501cf9371197f530362f5c4d52c60eb269 Mon Sep 17 00:00:00 2001 From: "Ola Wingbrant (sssowo)" Date: Fri, 31 May 2024 14:40:33 +0200 Subject: [PATCH] Add regression-tests/toh-contract-translation/Answers --- .../toh-contract-translation/Answers | 212 ++++++++++++++++++ 1 file changed, 212 insertions(+) diff --git a/regression-tests/toh-contract-translation/Answers b/regression-tests/toh-contract-translation/Answers index e69de29..50873c8 100644 --- a/regression-tests/toh-contract-translation/Answers +++ b/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