Skip to content

Commit

Permalink
Do not use assert without prior declaration
Browse files Browse the repository at this point in the history
The built-in variant is __CPROVER_assert
  • Loading branch information
tautschnig committed Jun 6, 2018
1 parent 7c053bf commit f2c60cf
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 4 deletions.
2 changes: 1 addition & 1 deletion regression/cpp/Resolver10/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ struct B: A
{
i = 1;
A();
assert(i==1);
__CPROVER_assert(i==1, "");
}
};

Expand Down
4 changes: 2 additions & 2 deletions regression/cpp/Resolver11/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ struct A
int main()
{
A a;
assert(a.test()==false);
__CPROVER_assert(a.test() == false, "");
const A a2;
assert(a2.test()==true);
__CPROVER_assert(a2.test() == true, "");
}
2 changes: 1 addition & 1 deletion regression/cpp/Template_Parameters1/main.ii
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,6 @@ T<int, 10> some_T;

int main()
{
assert(some_T.value==10);
__CPROVER_assert(some_T.value == 10, "");
}

0 comments on commit f2c60cf

Please sign in to comment.