Skip to content

Commit 567636a

Browse files
committed
Construct side_effect_expr_nondett with a source location
Construction without a source location is deprecated.
1 parent 4eb7d04 commit 567636a

File tree

3 files changed

+6
-4
lines changed

3 files changed

+6
-4
lines changed

src/goto-analyzer/taint_analysis.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,8 @@ bool taint_analysist::operator()(
289289
t->make_function_call(call);
290290
calls.add_instruction()->make_goto(end.instructions.begin());
291291
goto_programt::targett g=gotos.add_instruction();
292-
g->make_goto(t, side_effect_expr_nondett(bool_typet()));
292+
g->make_goto(
293+
t, side_effect_expr_nondett(bool_typet(), symbol.location));
293294
}
294295

295296
goto_functionst::goto_functiont &entry=

src/util/nondet.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,8 +54,8 @@ symbol_exprt generate_nondet_int(
5454

5555
// Assign the symbol any non deterministic integer value.
5656
// int_type name_prefix::nondet_int = NONDET(int_type)
57-
instructions.add(
58-
code_assignt(nondet_symbol, side_effect_expr_nondett(int_type)));
57+
instructions.add(code_assignt(
58+
nondet_symbol, side_effect_expr_nondett(int_type, source_location)));
5959

6060
// Constrain the non deterministic integer with a lower bound of `min_value`.
6161
// ASSUME(name_prefix::nondet_int >= min_value)

unit/analyses/dependence_graph.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,8 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]")
7272

7373
code_ifthenelset if_block(
7474
equal_exprt(
75-
side_effect_expr_nondett(int_type), from_integer(0, int_type)),
75+
side_effect_expr_nondett(int_type, source_locationt{}),
76+
from_integer(0, int_type)),
7677
code_blockt({call, assign_x}));
7778

7879
a_body.add(std::move(if_block));

0 commit comments

Comments
 (0)