Merge pull request diffblue#113 from diffblue/mariusmc92/bugfix/ignore-nondet-in-lvsa

Added NONDET handling in taint domain's init

Author: mariusmc92

src/taint-analysis/taint_summary.cpp

@@ -582,13 +582,33 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
         lvsa,
         it,
         *numbering);
+      if(asgn.rhs().id()==ID_side_effect)
+      {
+        const side_effect_exprt see=to_side_effect_expr(asgn.rhs());
+        if(see.get_statement()==ID_nondet)
+        {
+          const auto replace_it=
+            program->get_NONDET_retvals_replacements().find(it);
+          assert(replace_it!=program->get_NONDET_retvals_replacements().cend());
+          collect_lvsa_access_paths(
+            replace_it->second,
+            program->get_namespace(),
+            environment,
+            lvsa,
+            it,
+            *numbering);
+        }
+      }
+      else
+      {
       collect_lvsa_access_paths(
         asgn.rhs(),
         program->get_namespace(),
         environment,
         lvsa,
         it,
         *numbering);
+      }
     }
     else if(it->type == ASSERT)
     {