File tree Expand file tree Collapse file tree 2 files changed +4
-5
lines changed Expand file tree Collapse file tree 2 files changed +4
-5
lines changed Original file line number Diff line number Diff line change @@ -38,7 +38,7 @@ void goto_symext::symex_assign(
38
38
if (statement==ID_function_call)
39
39
{
40
40
DATA_INVARIANT (
41
- !side_effect_expr.operands ().empty ()
41
+ !side_effect_expr.operands ().empty (),
42
42
" function call stamement expects non-empty list of side effects" );
43
43
44
44
if (side_effect_expr.op0 ().id ()!=ID_symbol)
Original file line number Diff line number Diff line change @@ -18,10 +18,9 @@ void goto_symext::symex_start_thread(statet &state)
18
18
if (state.guard .is_false ())
19
19
return ;
20
20
21
- // we don't allow spawning threads out of atomic sections
22
- // this would require amendments to ordering constraints
23
- INVARIANT (state.atomic_section_id ==0 ,
24
- " start_thread in atomic section detected" );
21
+ INVARIANT (state.atomic_section_id == 0 ,
22
+ " spawning threads out of atomic sections is not allowed; "
23
+ " this would require amendments to ordering constraints" );
25
24
26
25
// record this
27
26
target.spawn (state.guard .as_expr (), state.source );
You can’t perform that action at this time.
0 commit comments