Skip to content

Commit 8be2f36

Browse files
tautschnigtautschnig
committed
Add array-refinement regression tests
Moving these tests from a dedicated folder to cbmc to run them, also making use of all three configurations that the cbmc folder is being tested with. (Unnecessary) GCC attributes were removed to make sure tests can be used on all platforms.
1 parent 3aa0141 commit 8be2f36

File tree

41 files changed

+24
-45
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+24
-45
lines changed

‎regression/array-refinement/Makefile

Lines changed: 0 additions & 21 deletions
This file was deleted.

‎regression/array-refinement/Array_UF1/main.c renamed to ‎regression/cbmc/Array_UF1/main.c

File renamed without changes.

‎regression/array-refinement/Array_UF1/test.desc renamed to ‎regression/cbmc/Array_UF1/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF10/main.c renamed to ‎regression/cbmc/Array_UF10/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
int __VERIFIER_nondet_int();
44

‎regression/array-refinement/Array_UF10/test.desc renamed to ‎regression/cbmc/Array_UF10/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF11/main.c renamed to ‎regression/cbmc/Array_UF11/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF11/test.desc renamed to ‎regression/cbmc/Array_UF11/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF12/main.c renamed to ‎regression/cbmc/Array_UF12/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF12/test.desc renamed to ‎regression/cbmc/Array_UF12/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF13/main.c renamed to ‎regression/cbmc/Array_UF13/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF13/test.desc renamed to ‎regression/cbmc/Array_UF13/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF14/main.c renamed to ‎regression/cbmc/Array_UF14/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
extern void __VERIFIER_assume(int);
44
void __VERIFIER_assert(int cond) {

‎regression/array-refinement/Array_UF14/test.desc renamed to ‎regression/cbmc/Array_UF14/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE thorough-paths
22
main.c
33
--arrays-uf-always --no-propagation --refine-arrays --unwind 6
44
^EXIT=10$

‎regression/array-refinement/Array_UF15/main.c renamed to ‎regression/cbmc/Array_UF15/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
extern void __VERIFIER_assume(int);
44
void __VERIFIER_assert(int cond) {

‎regression/array-refinement/Array_UF18/test.desc renamed to ‎regression/cbmc/Array_UF15/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE thorough-paths
22
main.c
33
--arrays-uf-always --no-propagation --refine-arrays --unwind 11
44
^EXIT=0$

‎regression/array-refinement/Array_UF16/main.c renamed to ‎regression/cbmc/Array_UF16/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
extern int __VERIFIER_nondet_int(void);
44
void __VERIFIER_assert(int cond) {

‎regression/array-refinement/Array_UF16/test.desc renamed to ‎regression/cbmc/Array_UF16/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF17/main.c renamed to ‎regression/cbmc/Array_UF17/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF17/test.desc renamed to ‎regression/cbmc/Array_UF17/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE thorough-paths
22
main.c
33
--arrays-uf-always --no-propagation --refine-arrays --unwind 9
44
^EXIT=0$

‎regression/array-refinement/Array_UF18/main.c renamed to ‎regression/cbmc/Array_UF18/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF15/test.desc renamed to ‎regression/cbmc/Array_UF18/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF19/main.c renamed to ‎regression/cbmc/Array_UF19/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF6/test.desc renamed to ‎regression/cbmc/Array_UF19/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE thorough-paths
22
main.c
33
--arrays-uf-always --no-propagation --refine-arrays --unwind 3
44
^EXIT=10$

‎regression/array-refinement/Array_UF2/main.c renamed to ‎regression/cbmc/Array_UF2/main.c

File renamed without changes.

‎regression/array-refinement/Array_UF2/test.desc renamed to ‎regression/cbmc/Array_UF2/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF20/main.c renamed to ‎regression/cbmc/Array_UF20/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
extern char __VERIFIER_nondet_char();
44

‎regression/array-refinement/Array_UF20/test.desc renamed to ‎regression/cbmc/Array_UF20/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF3/main.c renamed to ‎regression/cbmc/Array_UF3/main.c

File renamed without changes.

‎regression/array-refinement/Array_UF3/test.desc renamed to ‎regression/cbmc/Array_UF3/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF4/main.c renamed to ‎regression/cbmc/Array_UF4/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF4/test.desc renamed to ‎regression/cbmc/Array_UF4/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--arrays-uf-always --no-propagation --refine-arrays --unwind 2
44
^EXIT=0$

‎regression/array-refinement/Array_UF5/main.c renamed to ‎regression/cbmc/Array_UF5/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF5/test.desc renamed to ‎regression/cbmc/Array_UF5/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF6/main.c renamed to ‎regression/cbmc/Array_UF6/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF7/test.desc renamed to ‎regression/cbmc/Array_UF6/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE thorough-paths
22
main.c
33
--arrays-uf-always --no-propagation --refine-arrays --unwind 3
44
^EXIT=10$

‎regression/array-refinement/Array_UF7/main.c renamed to ‎regression/cbmc/Array_UF7/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF19/test.desc renamed to ‎regression/cbmc/Array_UF7/test.desc

File renamed without changes.

‎regression/array-refinement/Array_UF8/main.c renamed to ‎regression/cbmc/Array_UF8/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF8/test.desc renamed to ‎regression/cbmc/Array_UF8/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--arrays-uf-always --no-propagation --refine-arrays --unwind 6
44
^EXIT=0$

‎regression/array-refinement/Array_UF9/main.c renamed to ‎regression/cbmc/Array_UF9/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
1+
extern void __VERIFIER_error();
22

33
void __VERIFIER_assert(int cond) {
44
if (!(cond)) {

‎regression/array-refinement/Array_UF9/test.desc renamed to ‎regression/cbmc/Array_UF9/test.desc

File renamed without changes.

0 commit comments

Comments
 (0)