File tree 8 files changed +30
-36
lines changed 8 files changed +30
-36
lines changed Original file line number Diff line number Diff line change 1
- #include < cassert>
2
-
3
1
int const C=10 ;
4
2
5
3
int main ()
6
4
{
7
- assert (C== 10 );
5
+ __CPROVER_assert (C == 10 , " " );
8
6
9
7
// this is *not* allowed
10
8
((int &)C)=20 ;
Original file line number Diff line number Diff line change
1
+ #ifdef __GNUC__
2
+ #define NOTHROW __attribute__ ((nothrow))
3
+ #else
4
+ #define NOTHROW
5
+ #endif
6
+
1
7
namespace std {
2
8
// cmath
3
- __inline float abs (float x) __attribute__((nothrow)) ;
4
- __inline double abs (double x) __attribute__((nothrow)) ;
5
- __inline long double abs (long double x) __attribute__((nothrow)) ;
9
+ __inline float abs (float x) NOTHROW ;
10
+ __inline double abs (double x) NOTHROW ;
11
+ __inline long double abs (long double x) NOTHROW ;
6
12
}
7
13
8
14
namespace std {
9
15
extern " C" {
10
- int abs (int ) __attribute__((nothrow)) ;
16
+ int abs (int ) NOTHROW ;
11
17
}
12
18
extern " C++" {
13
- inline long abs (long n) __attribute__((nothrow)) ;
14
- inline long long abs (long long n) __attribute__((nothrow)) ;
19
+ inline long abs (long n) NOTHROW ;
20
+ inline long long abs (long long n) NOTHROW ;
15
21
}
16
22
}
17
23
Original file line number Diff line number Diff line change 1
- #include < cassert>
2
-
3
1
struct A
4
2
{
5
3
int i;
Original file line number Diff line number Diff line change 1
- #include < cassert>
2
-
3
1
struct A
4
2
{
5
3
bool func () { return false ; }
Original file line number Diff line number Diff line change 1
- #include < cassert>
2
-
3
1
// V depends on Ty
4
2
template <typename Ty, Ty V>
5
3
class T
Original file line number Diff line number Diff line change 1
- CORE
1
+ KNOWNBUG
2
2
main.cpp
3
3
4
4
^EXIT=0$
Original file line number Diff line number Diff line change 1
- #include < cassert>
2
-
3
1
enum E1 { e1 } e1_var;
4
2
enum E2 { e2 } e2_var;
5
3
@@ -23,19 +21,19 @@ struct some_struct
23
21
24
22
int main ()
25
23
{
26
- assert (f (0 )== 0 );
27
- assert (f (e1 )== 1 );
28
- assert (f (e2 )== 2 );
29
- assert (f (e1_var)== 1 );
30
- assert (f (e2_var)== 2 );
31
-
32
- assert (g (0 )== 0 );
33
- assert (g (e1 )== 1 );
34
- assert (g (e2 )== 0 );
35
- assert (g (e1_var)== 1 );
36
- assert (g (e2_var)== 0 );
37
-
38
- assert (f (some_struct_var.i )== 0 );
39
- assert (f (some_struct_var.e1 )== 1 );
40
- assert (f (some_struct_var.e2 )== 2 );
24
+ __CPROVER_assert (f (0 ) == 0 , " " );
25
+ __CPROVER_assert (f (e1 ) == 1 , " " );
26
+ __CPROVER_assert (f (e2 ) == 2 , " " );
27
+ __CPROVER_assert (f (e1_var) == 1 , " " );
28
+ __CPROVER_assert (f (e2_var) == 2 , " " );
29
+
30
+ __CPROVER_assert (g (0 ) == 0 , " " );
31
+ __CPROVER_assert (g (e1 ) == 1 , " " );
32
+ __CPROVER_assert (g (e2 ) == 0 , " " );
33
+ __CPROVER_assert (g (e1_var) == 1 , " " );
34
+ __CPROVER_assert (g (e2_var) == 0 , " " );
35
+
36
+ __CPROVER_assert (f (some_struct_var.i ) == 0 , " " );
37
+ __CPROVER_assert (f (some_struct_var.e1 ) == 1 , " " );
38
+ __CPROVER_assert (f (some_struct_var.e2 ) == 2 , " " );
41
39
}
Original file line number Diff line number Diff line change 1
- #include < cassert>
2
-
3
1
typedef decltype (nullptr ) nullptr_t;
4
2
5
3
static_assert (nullptr ==0 , " nullptr==0" );
@@ -20,7 +18,7 @@ int main()
20
18
21
19
char buffer[10 ];
22
20
void *p=my_null, *q=buffer;
23
- assert (q!= nullptr );
21
+ __CPROVER_assert (q != nullptr , " " );
24
22
25
23
something (nullptr );
26
24
}
You can’t perform that action at this time.
0 commit comments