-
Notifications
You must be signed in to change notification settings - Fork 63
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add a regression test for one part of issue #641.
- Loading branch information
Brian Huffman
committed
Aug 28, 2020
1 parent
e7fb2e1
commit be206a8
Showing
5 changed files
with
53 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,2 @@ | ||
test.bc : test.c | ||
clang -c -emit-llvm -g -o test.bc test.c |
Binary file not shown.
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,12 @@ | ||
#include <stdint.h> | ||
#include <stdlib.h> | ||
|
||
uint64_t glob; | ||
|
||
uint64_t *foo () { | ||
return &glob; | ||
} | ||
|
||
int bar () { | ||
return (foo() == &glob); | ||
} |
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,38 @@ | ||
// This test checks whether we can verify a spec that says a function | ||
// returns a fresh pointer, when in actuality the function returns | ||
// a global. It is a regression test for saw-script issue #641. | ||
// https://github.com/GaloisInc/saw-script/issues/641 | ||
|
||
bc <- llvm_load_module "test.bc"; | ||
|
||
let i64 = llvm_int 64; | ||
|
||
fails ( | ||
crucible_llvm_verify bc "foo" [] false | ||
do { | ||
crucible_alloc_global "glob"; | ||
crucible_execute_func []; | ||
x <- crucible_alloc i64; | ||
crucible_return x; | ||
} | ||
z3 | ||
); | ||
|
||
/* | ||
bar_ov0 <- | ||
crucible_llvm_verify bc "bar" [foo_ov] false | ||
do { | ||
crucible_execute_func []; | ||
crucible_return (crucible_term {{ 0 : [32] }}); | ||
} | ||
z3; | ||
*/ | ||
|
||
bar_ov1 <- | ||
crucible_llvm_verify bc "bar" [] false | ||
do { | ||
crucible_alloc_global "glob"; | ||
crucible_execute_func []; | ||
crucible_return (crucible_term {{ 1 : [32] }}); | ||
} | ||
z3; |
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 @@ | ||
$SAW test.saw |