Added check that resulting GOTO binaries do not contain 'x=NONDET(T*)'.

Updates requested in the review.

Author: marek-trtik

src/driver/sec_driver_parse_options.cpp

@@ -513,10 +513,7 @@ void sec_driver_parse_optionst::process_goto_function(
     replace_java_nondet(function);
 
     convert_nondet(
-      function,
-      get_message_handler(),
-      object_factory_params,
-      ID_java);
+      function, get_message_handler(), object_factory_params, ID_java);
 
     adjust_float_expressions(goto_function, namespacet(symbol_table));
 
@@ -642,7 +639,7 @@ bool sec_driver_parse_optionst::generate_function_body(
   if(body_available || !can_generate_function_body(function_name))
   {
     const symbolt *symbol = symbol_table.lookup(function_name);
-    if (symbol == nullptr || !symbol->type.get_bool(ID_C_abstract))
+    if(symbol == nullptr || !symbol->type.get_bool(ID_C_abstract))
       return false;
   }
 

src/taint-slicer/slicing_tasks_builder.cpp

@@ -326,6 +326,22 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
           I.function=fname_prog.first;
         }
 
+    // Check that the goto program to be saved does not contain any NONDET(T*)
+    // expressions. However, non-pointer NONDET expressions can be present.
+    class nondet_visitort : public const_expr_visitort
+    {
+    public:
+      void operator()(const exprt &expr) override
+      {
+        INVARIANT(
+          expr.id() != ID_nondet || expr.type().id() != ID_pointer,
+          "No pointer-typed NONDET allowed.");
+      }
+    } visitor;
+    for(auto &fname_prog : goto_functions.function_map)
+      for(const auto &I : fname_prog.second.body.instructions)
+        I.code.visit(visitor);
+
     // Finally save the constructed slicing task on the disc as GOTO program
     // binary.
     const bool fail=write_goto_binary(