Skip to content

Commit 98c5484

Browse files
tautschnigtautschnig
committed
Add cbmc-from-CVS regression tests
Move the remaining tests from cbmc-from-CVS to cbmc and fix their test specifications to work with current CBMC. This enables otherwise unused tests.
1 parent 276b8d7 commit 98c5484

File tree

147 files changed

+76
-93
lines changed

Some content is hidden

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

147 files changed

+76
-93
lines changed

‎regression/cbmc-from-CVS/Makefile

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

‎regression/cbmc-from-CVS/Malloc4/test.desc

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

‎regression/cbmc-from-CVS/Malloc5/test.desc

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

‎regression/cbmc-from-CVS/Malloc8/test.desc

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

‎regression/cbmc-from-CVS/Pointer3/test.desc

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

‎regression/cbmc-from-CVS/Pointer31/test.desc

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

‎regression/cbmc-from-CVS/return2/test.desc

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

‎regression/cbmc-from-CVS/Array_Access1/main.c renamed to ‎regression/cbmc/Array_Access1/main.c

File renamed without changes.

‎regression/cbmc-from-CVS/Array_Access1/test.desc renamed to ‎regression/cbmc/Array_Access1/test.desc

File renamed without changes.

‎regression/cbmc-from-CVS/Array_Access2/main.c renamed to ‎regression/cbmc/Array_Access2/main.c

File renamed without changes.

0 commit comments

Comments
 (0)