diff --git a/regression/cbmc/scanf1/big-endian.desc b/regression/cbmc/scanf1/big-endian.desc new file mode 100644 index 00000000000..6a4549ce627 --- /dev/null +++ b/regression/cbmc/scanf1/big-endian.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.i +--big-endian +^EXIT=10$ +^SIGNAL=0$ +^\*\* 8 of 8 failed +-- +^warning: ignoring diff --git a/regression/cbmc/scanf1/main.c b/regression/cbmc/scanf1/main.i similarity index 57% rename from regression/cbmc/scanf1/main.c rename to regression/cbmc/scanf1/main.i index 55ca6a4af5f..960ceda8498 100644 --- a/regression/cbmc/scanf1/main.c +++ b/regression/cbmc/scanf1/main.i @@ -1,6 +1,3 @@ -#include -#include - int main(void) { char c=0; @@ -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; } diff --git a/regression/cbmc/scanf1/no-simplify.desc b/regression/cbmc/scanf1/no-simplify.desc new file mode 100644 index 00000000000..d2cc73330b1 --- /dev/null +++ b/regression/cbmc/scanf1/no-simplify.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.i +--little-endian --no-simplify +^EXIT=10$ +^SIGNAL=0$ +^\*\* 8 of 8 failed +-- +^warning: ignoring diff --git a/regression/cbmc/scanf1/test.desc b/regression/cbmc/scanf1/test.desc index b20bfc6b36a..346519020ae 100644 --- a/regression/cbmc/scanf1/test.desc +++ b/regression/cbmc/scanf1/test.desc @@ -1,6 +1,6 @@ CORE -main.c - +main.i +--little-endian ^EXIT=10$ ^SIGNAL=0$ ^\*\* 8 of 8 failed