Skip to content

Commit 03103d3

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.
1 parent eaa8345 commit 03103d3

File tree

41 files changed

+2
-23
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

+2
-23
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

File renamed without changes.

‎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

File renamed without changes.

‎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

File renamed without changes.

‎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

File renamed without changes.

‎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

File renamed without changes.

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

File renamed without changes.

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

File renamed without changes.

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

File renamed without changes.

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

File renamed without changes.

‎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

File renamed without changes.

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

File renamed without changes.

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

File renamed without changes.

‎regression/array-refinement/Array_UF18/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

File renamed without changes.

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

File renamed without changes.

‎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

File renamed without changes.

‎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

File renamed without changes.

‎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

File renamed without changes.

‎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

File renamed without changes.

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

File renamed without changes.

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

File renamed without changes.

‎regression/array-refinement/Array_UF7/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

File renamed without changes.

‎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

File renamed without changes.

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

File renamed without changes.

0 commit comments

Comments
 (0)