Skip to content

Commit

Permalink
Merge pull request diffblue#2536 from tautschnig/debian8
Browse files Browse the repository at this point in the history
Test only works with simplification enabled
  • Loading branch information
tautschnig authored Jul 7, 2018
2 parents d6565ec + 26803f7 commit c8725cb
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 c8725cb

Please sign in to comment.