Merge pull request #3938 from tautschnig/deprecation-nondet

Construct side_effect_expr_nondett with a source location [blocks: #3800]

Author: tautschnig

src/goto-analyzer/taint_analysis.cpp

@@ -290,7 +290,8 @@ bool taint_analysist::operator()(
           t->make_function_call(call);
           calls.add_instruction()->make_goto(end.instructions.begin());
           goto_programt::targett g=gotos.add_instruction();
-          g->make_goto(t, side_effect_expr_nondett(bool_typet()));
+          g->make_goto(
+            t, side_effect_expr_nondett(bool_typet(), symbol.location));
         }
 
       goto_functionst::goto_functiont &entry=

src/util/nondet.cpp

@@ -54,8 +54,8 @@ symbol_exprt generate_nondet_int(
 
   // Assign the symbol any non deterministic integer value.
   //   int_type name_prefix::nondet_int = NONDET(int_type)
-  instructions.add(
-    code_assignt(nondet_symbol, side_effect_expr_nondett(int_type)));
+  instructions.add(code_assignt(
+    nondet_symbol, side_effect_expr_nondett(int_type, source_location)));
 
   // Constrain the non deterministic integer with a lower bound of `min_value`.
   //   ASSUME(name_prefix::nondet_int >= min_value)

unit/analyses/dependence_graph.cpp

@@ -72,7 +72,8 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]")
 
     code_ifthenelset if_block(
       equal_exprt(
-        side_effect_expr_nondett(int_type), from_integer(0, int_type)),
+        side_effect_expr_nondett(int_type, source_locationt{}),
+        from_integer(0, int_type)),
       code_blockt({call, assign_x}));
 
     a_body.add(std::move(if_block));