Skip to content

Commit c8725cb

Browse files
authored
Merge pull request diffblue#2536 from tautschnig/debian8
Test only works with simplification enabled
2 parents d6565ec + 26803f7 commit c8725cb

File tree

4 files changed

+26
-13
lines changed

4 files changed

+26
-13
lines changed
+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
main.i
3+
--big-endian
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\*\* 8 of 8 failed
7+
--
8+
^warning: ignoring

regression/cbmc/scanf1/main.c renamed to regression/cbmc/scanf1/main.i

+8-11
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,3 @@
1-
#include <stdio.h>
2-
#include <assert.h>
3-
41
int main(void)
52
{
63
char c=0;
@@ -23,14 +20,14 @@ int main(void)
2320
__CPROVER_scanf("%p", &p);
2421
__CPROVER_scanf("%s", buffer);
2522

26-
assert(c==0); // may fail
27-
assert(si==0); // may fail
28-
assert(i==0); // may fail
29-
assert(f==0); // may fail
30-
assert(d==0); // may fail
31-
assert(li==0); // may fail
32-
assert(p==0); // may fail
33-
assert(buffer[0]==0); // may fail
23+
__CPROVER_assert(c == 0, "may fail");
24+
__CPROVER_assert(si == 0, "may fail");
25+
__CPROVER_assert(i == 0, "may fail");
26+
__CPROVER_assert(f == 0, "may fail");
27+
__CPROVER_assert(d == 0, "may fail");
28+
__CPROVER_assert(li == 0, "may fail");
29+
__CPROVER_assert(p == 0, "may fail");
30+
__CPROVER_assert(buffer[0] == 0, "may fail");
3431

3532
return 0;
3633
}
+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
main.i
3+
--little-endian --no-simplify
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\*\* 8 of 8 failed
7+
--
8+
^warning: ignoring

regression/cbmc/scanf1/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
2-
main.c
3-
2+
main.i
3+
--little-endian
44
^EXIT=10$
55
^SIGNAL=0$
66
^\*\* 8 of 8 failed

0 commit comments

Comments
 (0)