-
Notifications
You must be signed in to change notification settings - Fork 13
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add regression-tests/toh-contract-translation/Answers
- Loading branch information
Ola Wingbrant (sssowo)
committed
May 31, 2024
1 parent
be699b7
commit 971f955
Showing
1 changed file
with
212 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |