-
Notifications
You must be signed in to change notification settings - Fork 10
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Temporary commit: show results of ./hip testcases/ex5.c
- Loading branch information
1 parent
29575e4
commit 20c1200
Showing
3 changed files
with
275 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,147 @@ | ||
|
|
||
| !!! **tpdispatcher.ml#492:init_tp by default: | ||
| !!! **tpdispatcher.ml#391:set_tp z3 | ||
| !!!Full processing file "testcases/ex5.c" | ||
| Parsing file "testcases/ex5.c" by cil parser... | ||
| GCC Preprocessing... | ||
| gcc -I ../ -I /usr/lib/x86_64-linux-gnu/glib-2.0/include/ -C -E testcases/ex5.c -o testcases/ex5.c.prep | ||
| **cilparser.ml#1298:Not Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "void " -> "void_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:void | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data void_star { | ||
| void value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "void_star" -> "data void_star { | ||
| void value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Not Found "void *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "void *" -> "void_star_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:void * | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data void_star_star { | ||
| void_star value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "void_star_star" -> "data void_star_star { | ||
| void_star value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Not Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "int " -> "int_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:int | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data int_star { | ||
| int value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "int_star" -> "data int_star { | ||
| int value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Not Found "int *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "int *" -> "int_star_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:int * | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data int_star_star { | ||
| int_star value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "int_star_star" -> "data int_star_star { | ||
| int_star value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Not Found "char " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "char " -> "char_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:char | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data char_star { | ||
| int value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "char_star" -> "data char_star { | ||
| int value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1086:Not Found "p" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "int *" in tbl_pointer_typ | ||
| **cilparser.ml#1124:Found "int_star_star" in tbl_data_decl | ||
| **cilparser.ml#1474:Not Found "p" in tbl_addr_info | ||
| **cilparser.ml#1136:Adding "p" -> "addr_p" to tbl_addr_info | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1474:Not Found "tmp" in tbl_addr_info | ||
| **cilparser.ml#1474:Found "p" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1474:Not Found "tmp" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1474:Not Found "a" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "int *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1669:Found "p" in tbl_addr_info | ||
|
|
||
| !!! processing primitives "["prelude.ss"] | ||
|
|
||
| Starting z3... | ||
|
|
||
| !!! **WARNING****astsimp.ml#9346:Post-condition has existentially quantified free vars, error position: ./prelude.ss_613:10_613:25:[(q,)] | ||
| !!! **WARNING****astsimp.ml#9346:Post-condition has existentially quantified free vars, error position: ./prelude.ss_608:22_608:39:[(p,)] | ||
| !!! **WARNING****astsimp.ml#9346:Post-condition has existentially quantified free vars, error position: testcases/ex5.c_131:11_131:26:[(v,)] | ||
| Starting Omega.../home/koo/.bin/oc | ||
|
|
||
| !!!WARNING : uninterpreted free variables [l,h] in specification. | ||
| !!! **typechecker.ml#3649:start check_proc:[a_86] | ||
|
|
||
| Checking procedure foo$int_star... | ||
|
|
||
| Proving precondition in method free$int_star_star Failed. | ||
| (may) cause: Nothing_to_do?no proper match (type error) found for: Type: Root | ||
| LHS: addr_p'::void_star<Anon_2372>@M | ||
| RHS: addr_p'::int_star_star<Anon_39>@M | ||
| root_inst: None | ||
| lhs_rest: tmp'::int_star<Anon_2349>@M * a_86'::void_star<x>@M | ||
| rhs_rest: emp | ||
| alias set: [addr_p',addr_p']rhs_inst: []rhs_infer: None | ||
|
|
||
| Context of Verification Failure: testcases/ex5.c_131:11_131:26 | ||
|
|
||
| Last Proving Location: testcases/ex5.c_135:13_135:14 | ||
|
|
||
| Procedure foo$int_star FAIL.(2) | ||
|
|
||
|
|
||
| Exception Failure("Proving precond failed") Occurred! | ||
|
|
||
|
|
||
| Error(s) detected when checking procedure foo$int_star | ||
| Stop z3... 163 invocations | ||
| Stop Omega... 100 invocations | ||
| 0 false contexts at: () | ||
|
|
||
| !!! log(small):(0.352367,659) | ||
| Total verification time: 0.989302 second(s) | ||
| Time spent in main process: 0.852892 second(s) | ||
| Time spent in child processes: 0.13641 second(s) | ||
| Z3 Prover Time: 0.009457 second(s) |
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,127 @@ | ||
|
|
||
| !!! **tpdispatcher.ml#492:init_tp by default: | ||
| !!! **tpdispatcher.ml#391:set_tp z3 | ||
| !!!Full processing file "testcases/ex5.c" | ||
| Parsing file "testcases/ex5.c" by cil parser... | ||
| GCC Preprocessing... | ||
| gcc -I ../ -I /usr/lib/x86_64-linux-gnu/glib-2.0/include/ -C -E testcases/ex5.c -o testcases/ex5.c.prep | ||
| **cilparser.ml#1298:Not Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "void " -> "void_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:void | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data void_star { | ||
| void value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "void_star" -> "data void_star { | ||
| void value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Not Found "void *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "void *" -> "void_star_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:void * | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data void_star_star { | ||
| void_star value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "void_star_star" -> "data void_star_star { | ||
| void_star value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Not Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "int " -> "int_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:int | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data int_star { | ||
| int value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "int_star" -> "data int_star { | ||
| int value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Not Found "int *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "int *" -> "int_star_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:int * | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data int_star_star { | ||
| int_star value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "int_star_star" -> "data int_star_star { | ||
| int_star value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Not Found "char " in tbl_pointer_typ | ||
| **cilparser.ml#1316:Adding "char " -> "char_star" to tbl_pointer_typ | ||
|
|
||
| !!! **cilparser.ml#1318:core_type:char | ||
| !!! **cilparser.ml#1319:new ddecl for pointer type: | ||
| data char_star { | ||
| int value@ | ||
| } | ||
| **cilparser.ml#1320:Adding "char_star" -> "data char_star { | ||
| int value@ | ||
| } | ||
| " to tbl_data_decl | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1086:Not Found "p" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "int *" in tbl_pointer_typ | ||
| **cilparser.ml#1124:Found "int_star_star" in tbl_data_decl | ||
| **cilparser.ml#1474:Not Found "p" in tbl_addr_info | ||
| **cilparser.ml#1136:Adding "p" -> "addr_p" to tbl_addr_info | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "char " in tbl_pointer_typ | ||
| **cilparser.ml#1474:Not Found "tmp" in tbl_addr_info | ||
| **cilparser.ml#1474:Found "p" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1474:Not Found "tmp" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "int " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1474:Not Found "a" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "int *" in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "void " in tbl_pointer_typ | ||
| **cilparser.ml#1669:Found "p" in tbl_addr_info | ||
| **cilparser.ml#1474:Not Found "s" in tbl_addr_info | ||
| **cilparser.ml#1298:Found "char " in tbl_pointer_typ | ||
| **cilparser.ml#1298:Found "char " in tbl_pointer_typ | ||
|
|
||
| !!! processing primitives "["prelude.ss"] | ||
|
|
||
| Starting z3... | ||
|
|
||
| !!! **WARNING****astsimp.ml#9346:Post-condition has existentially quantified free vars, error position: ./prelude.ss_613:10_613:25:[(q,)] | ||
| !!! **WARNING****astsimp.ml#9346:Post-condition has existentially quantified free vars, error position: ./prelude.ss_608:22_608:39:[(p,)] | ||
| !!! **WARNING****astsimp.ml#9346:Post-condition has existentially quantified free vars, error position: testcases/ex5.c_131:11_131:26:[(v,)] | ||
| Starting Omega.../home/koo/.bin/oc | ||
|
|
||
| !!!WARNING : uninterpreted free variables [l,h] in specification. | ||
| Last Proving Location: testcases/ex5.c_128:0_137:1 | ||
|
|
||
| ERROR: at testcases/ex5.c_136:7_136:10 | ||
| Message: OpAssign : lhs and rhs do not match 2 | ||
| Stop z3... 48 invocations | ||
| Stop Omega... 14 invocations caught | ||
|
|
||
| Exception occurred: Failure("OpAssign : lhs and rhs do not match 2") | ||
| Error3(s) detected at main |
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