Merge pull request #559 from smackers/fix-failing-regressions

Move failing regressions due to #550 to the failing folder
smackers · Apr 10, 2020 · 32f5f91 · 32f5f91
2 parents d833a6f + 20f4db6
commit 32f5f91
Show file tree

Hide file tree

Showing 7 changed files with 5 additions and 10 deletions.
diff --git a/test/c/ntdrivers/floppy_false.i.cil.c → test/c/failing/floppy_false.i.cil.c b/test/c/ntdrivers/floppy_false.i.cil.c → test/c/failing/floppy_false.i.cil.c
@@ -2,6 +2,7 @@
 
 // @expect error
 
+// see: https://github.com/smackers/smack/issues/554
 extern char __VERIFIER_nondet_char(void);
 extern int __VERIFIER_nondet_int(void);
 extern long __VERIFIER_nondet_long(void);

diff --git a/test/c/ntdrivers/floppy_true.i.cil.c → test/c/failing/floppy_true.i.cil.c b/test/c/ntdrivers/floppy_true.i.cil.c → test/c/failing/floppy_true.i.cil.c
@@ -2,6 +2,7 @@
 
 // @expect verified
 
+// see: https://github.com/smackers/smack/issues/554
 extern char __VERIFIER_nondet_char(void);
 extern int __VERIFIER_nondet_int(void);
 extern long __VERIFIER_nondet_long(void);

diff --git a/test/c/ntdrivers/parport_false.i.cil.c → test/c/failing/parport_false.i.cil.c b/test/c/ntdrivers/parport_false.i.cil.c → test/c/failing/parport_false.i.cil.c
@@ -2,6 +2,7 @@
 
 // @expect error
 
+// see: https://github.com/smackers/smack/issues/554
 extern char __VERIFIER_nondet_char(void);
 extern int __VERIFIER_nondet_int(void);
 extern long __VERIFIER_nondet_long(void);

diff --git a/test/c/ntdrivers/parport_true.i.cil.c → test/c/failing/parport_true.i.cil.c b/test/c/ntdrivers/parport_true.i.cil.c → test/c/failing/parport_true.i.cil.c
@@ -2,6 +2,7 @@
 
 // @expect verified
 
+// see: https://github.com/smackers/smack/issues/554
 extern char __VERIFIER_nondet_char(void);
 extern int __VERIFIER_nondet_int(void);
 extern long __VERIFIER_nondet_long(void);

diff --git a/test/c/pthread/regression_525_malloc.c → test/c/failing/regression_525_malloc.c b/test/c/pthread/regression_525_malloc.c → test/c/failing/regression_525_malloc.c
@@ -3,6 +3,7 @@
 #include <stdlib.h>
 
 // @expect verified
+// see: https://github.com/smackers/smack/issues/555
 // https://github.com/smackers/smack/issues/525
 
 pthread_t tid1;

diff --git a/test/c/failing/null_dereference_fail.c → .../c/failing/unallocated_dereference_fail.c b/test/c/failing/null_dereference_fail.c → .../c/failing/unallocated_dereference_fail.c
diff --git a/test/c/memory-safety/ununallocated_dereference_fail.c b/test/c/memory-safety/ununallocated_dereference_fail.c