Skip to content

Commit

Permalink
Test only works with simplification enabled
Browse files Browse the repository at this point in the history
... and simplification is only performed for byte_extract_little_endian.
  • Loading branch information
tautschnig committed Jul 7, 2018
1 parent 8187bdd commit 26803f7
Show file tree
Hide file tree
Showing 4 changed files with 26 additions and 13 deletions.
8 changes: 8 additions & 0 deletions regression/cbmc/scanf1/big-endian.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
KNOWNBUG
main.i
--big-endian
^EXIT=10$
^SIGNAL=0$
^\*\* 8 of 8 failed
--
^warning: ignoring
19 changes: 8 additions & 11 deletions regression/cbmc/scanf1/main.c → regression/cbmc/scanf1/main.i
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
#include <stdio.h>
#include <assert.h>

int main(void)
{
char c=0;
Expand All @@ -23,14 +20,14 @@ int main(void)
__CPROVER_scanf("%p", &p);
__CPROVER_scanf("%s", buffer);

assert(c==0); // may fail
assert(si==0); // may fail
assert(i==0); // may fail
assert(f==0); // may fail
assert(d==0); // may fail
assert(li==0); // may fail
assert(p==0); // may fail
assert(buffer[0]==0); // may fail
__CPROVER_assert(c == 0, "may fail");
__CPROVER_assert(si == 0, "may fail");
__CPROVER_assert(i == 0, "may fail");
__CPROVER_assert(f == 0, "may fail");
__CPROVER_assert(d == 0, "may fail");
__CPROVER_assert(li == 0, "may fail");
__CPROVER_assert(p == 0, "may fail");
__CPROVER_assert(buffer[0] == 0, "may fail");

return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc/scanf1/no-simplify.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
KNOWNBUG
main.i
--little-endian --no-simplify
^EXIT=10$
^SIGNAL=0$
^\*\* 8 of 8 failed
--
^warning: ignoring
4 changes: 2 additions & 2 deletions regression/cbmc/scanf1/test.desc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c

main.i
--little-endian
^EXIT=10$
^SIGNAL=0$
^\*\* 8 of 8 failed
Expand Down

0 comments on commit 26803f7

Please sign in to comment.