File tree Expand file tree Collapse file tree 3 files changed +10
-6
lines changed
regression/cbmc/pragma_cprover_enable_disable_multiple Expand file tree Collapse file tree 3 files changed +10
-6
lines changed Original file line number Diff line number Diff line change @@ -7,10 +7,12 @@ int main()
7
7
8
8
#pragma CPROVER check push
9
9
#pragma CPROVER check enable "pointer-overflow"
10
- #pragma CPROVER check enable "pointer-overflow" // should not print an error message
10
+ // should not print an error message
11
+ #pragma CPROVER check enable "pointer-overflow"
11
12
#pragma CPROVER check push
12
13
#pragma CPROVER check disable "pointer-primitive"
13
- #pragma CPROVER check enable "pointer-primitive" // should print an error message
14
+ // PARSE_ERROR
15
+ #pragma CPROVER check enable "pointer-primitive"
14
16
#pragma CPROVER check pop
15
17
#pragma CPROVER check pop
16
18
return 0 ;
Original file line number Diff line number Diff line change 25
25
#include < util/ieee_float.h>
26
26
#include < util/invariant.h>
27
27
#include < util/make_unique.h>
28
- #include < util/options.h>
29
28
#include < util/message.h>
29
+ #include < util/options.h>
30
30
#include < util/pointer_expr.h>
31
31
#include < util/pointer_offset_size.h>
32
32
#include < util/pointer_predicates.h>
@@ -1856,7 +1856,7 @@ optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
1856
1856
class flag_resett
1857
1857
{
1858
1858
public:
1859
- // / \brief Store the current value of \p flag and
1859
+ // / \brief Store the current value of \p flag and
1860
1860
// / then set its value to \p new_value.
1861
1861
// / \returns true if the flag was already seen before
1862
1862
bool set_flag (bool &flag, bool new_value)
@@ -1877,7 +1877,7 @@ class flag_resett
1877
1877
return seen_flags.find (&flag) != seen_flags.end ();
1878
1878
}
1879
1879
1880
- // / \brief Restore the values of all flags that have been
1880
+ // / \brief Restore the values of all flags that have been
1881
1881
// / modified via `set_flag`.
1882
1882
~flag_resett ()
1883
1883
{
Original file line number Diff line number Diff line change @@ -123,7 +123,9 @@ class ansi_c_parsert : public parsert
123
123
124
124
void copy_item (const ansi_c_declarationt &declaration)
125
125
{
126
- assert (declaration.id () == ID_declaration);
126
+ INVARIANT (
127
+ declaration.id () == ID_declaration,
128
+ " Expected `ID_declaration`, got `" + declaration.id () + " `" );
127
129
parse_tree.items .push_back (declaration);
128
130
}
129
131
You can’t perform that action at this time.
0 commit comments