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

regression/cpp-from-CVS/Assignment1/main.cpp renamed to regression/cbmc-cpp/Assignment1/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 A { int i;};
23

34
struct B
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

regression/cpp-from-CVS/Class_Members1/main.cpp renamed to regression/cbmc-cpp/Class_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
class t
23
{
34
public:
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int main()
23
{
34
int s=0;
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int main()
23
{
34
bool b;
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
char a[1];
23
char b[2];
34

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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
class t1
23
{
34
public:
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

regression/cpp-from-CVS/Constructor12/main.cpp renamed to regression/cbmc-cpp/Constructor12/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 A
23
{
34
int i;
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int g;
23
class A {
34
public:
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
class t1
23
{
34
public:
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
class x
23
{
34
public:
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

regression/cpp-from-CVS/Constructor4/main.cpp renamed to regression/cbmc-cpp/Constructor4/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
int *q;
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
class x
23
{
34
private:
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int counter=1;
23

34
struct T
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
// Default Initialization of arrays
23
class B
34
{
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int main()
23
{
34
unsigned i = 1;
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

regression/cpp-from-CVS/Conversion6/main.cpp renamed to regression/cbmc-cpp/Conversion6/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 A
23
{
34
int i;
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

regression/cpp-from-CVS/Conversion_Operator2/main.cpp renamed to regression/cbmc-cpp/Conversion_Operator2/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 B
23
{
34
int i;
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

regression/cpp-from-CVS/Conversion_Operator3/main.cpp renamed to regression/cbmc-cpp/Conversion_Operator3/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 A {
23
int i;
34
};
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

regression/cpp-from-CVS/Conversion_Operator4/main.cpp renamed to regression/cbmc-cpp/Conversion_Operator4/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 A
23
{
34
static const int* const i = 0;
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
// #include <assert.h>
23

34
int f(int d=1)
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int func(int i = 0) {return i;}
23

34
int main()
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int global;
23

34
class test_class {
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int main(int argc, char* argv[])
23
{
34
float x = 0.1;

regression/cbmc-cpp/Float1/test.desc

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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
class A {
23
int i;
34
friend class B;

regression/cbmc-cpp/Friend5/test.desc

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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
// test default arguments
23

34
int f(int a, int b=2, int c=3)
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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
bool func(const int& i) {return false;}
23
bool func(const int* i) {return true;}
34

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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
#include <cassert>
12
int f(int x)
23
{
34
assert(x==1);

0 commit comments

Comments
 (0)