Skip to content

Commit 879afa2

Browse files
committed
Enable cpp-from-CVS regression tests
Moving them to cbmc-cpp as they test VERIFICATION results, with few exceptions that were safe to be placed in the cpp folder. Adding `#include <cassert>` as needed.
1 parent ac11ec8 commit 879afa2

File tree

596 files changed

+938
-866
lines changed

Some content is hidden

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

596 files changed

+938
-866
lines changed

regression/cpp-from-CVS/Address_of_Method1/main.cpp renamed to regression/cbmc-cpp/Address_of_Method1/main.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
struct x
23
{
34
void f();
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG winbug macos-assert-broken
2+
main.cpp
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

regression/cpp-from-CVS/Anonymous_members1/main.cpp renamed to regression/cbmc-cpp/Anonymous_members1/main.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
typedef unsigned DWORD;
23
typedef signed LONG;
34
typedef long long LONGLONG;
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE winbug macos-assert-broken
2+
main.cpp
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)