Apply miscellaneous refactoring and fixes to goto-harness.

Add error checking (check that the entry function is in the symbol table
before the code generation, and make sure that it's present correctly)
make sure that doc comments are capitalised, change the signatures of
functions to make them stricter in the arguments they accept.

Author: NlightNFotis

src/goto-harness/function_call_harness_generator.cpp

@@ -72,10 +72,10 @@ struct function_call_harness_generatort::implt
   void ensure_harness_does_not_already_exist();
   /// Update the goto-model with the new harness function.
   void add_harness_function_to_goto_model(code_blockt function_body);
-  /// declare local variables for each of the parameters of the entry function
+  /// Declare local variables for each of the parameters of the entry function
   /// and return them
   code_function_callt::argumentst declare_arguments(code_blockt &function_body);
-  /// write initialisation code for each of the arguments into function_body,
+  /// Write initialisation code for each of the arguments into function_body,
   /// then insert a call to the entry function with the arguments
   void call_function(
     const code_function_callt::argumentst &arguments,
@@ -260,7 +260,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
 void function_call_harness_generatort::validate_options(
   const goto_modelt &goto_model)
 {
-  if(p_impl->function == ID_empty)
+  if(p_impl->function == ID_empty_string)
     throw invalid_command_line_argument_exceptiont{
       "required parameter entry function not set",
       "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
@@ -274,8 +274,17 @@ void function_call_harness_generatort::validate_options(
       " --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
   }
 
-  auto function_to_call = goto_model.symbol_table.lookup_ref(p_impl->function);
-  auto ftype = to_code_type(function_to_call.type);
+  const auto function_to_call_pointer =
+    goto_model.symbol_table.lookup(p_impl->function);
+  if(function_to_call_pointer == nullptr)
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "entry function `" + id2string(p_impl->function) +
+        "' does not exist in the symbol table",
+      "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
+  }
+  const auto &function_to_call = *function_to_call_pointer;
+  const auto &ftype = to_code_type(function_to_call.type);
   for(auto const &pointer_id : p_impl->function_parameters_to_treat_equal)
   {
     std::string decorated_pointer_id =

src/goto-harness/recursive_initialization.cpp

@@ -157,7 +157,7 @@ void recursive_initializationt::initialize(
 
 code_blockt recursive_initializationt::build_constructor_body(
   const exprt &depth_symbol,
-  const exprt &result_symbol,
+  const symbol_exprt &result_symbol,
   const optionalt<exprt> &size_symbol,
   const optionalt<irep_idt> &lhs_name)
 {
@@ -192,7 +192,7 @@ code_blockt recursive_initializationt::build_constructor_body(
   }
 }
 
-const irep_idt &recursive_initializationt::build_constructor(const exprt &expr)
+irep_idt recursive_initializationt::build_constructor(const exprt &expr)
 {
   // for `expr` of type T builds a declaration of a function:
   //
@@ -207,7 +207,9 @@ const irep_idt &recursive_initializationt::build_constructor(const exprt &expr)
   {
     expr_name = to_symbol_expr(expr).get_identifier();
     if(should_be_treated_as_array(*expr_name))
+    {
       size_var = get_associated_size_variable(*expr_name);
+    }
   }
   const typet &type = expr.type();
   if(type_constructor_names.find(type) != type_constructor_names.end())
@@ -520,7 +522,7 @@ symbol_exprt recursive_initializationt::get_free_function()
 
 code_blockt recursive_initializationt::build_pointer_constructor(
   const exprt &depth,
-  const exprt &result)
+  const symbol_exprt &result)
 {
   PRECONDITION(result.type().id() == ID_pointer);
   const typet &type = result.type().subtype();
@@ -605,7 +607,7 @@ code_blockt recursive_initializationt::build_pointer_constructor(
 }
 
 code_blockt recursive_initializationt::build_array_string_constructor(
-  const exprt &result) const
+  const symbol_exprt &result) const
 {
   PRECONDITION(result.type().id() == ID_pointer);
   const typet &type = result.type().subtype();
@@ -634,7 +636,7 @@ code_blockt recursive_initializationt::build_array_string_constructor(
 
 code_blockt recursive_initializationt::build_array_constructor(
   const exprt &depth,
-  const exprt &result)
+  const symbol_exprt &result)
 {
   PRECONDITION(result.type().id() == ID_pointer);
   const typet &type = result.type().subtype();
@@ -656,7 +658,7 @@ code_blockt recursive_initializationt::build_array_constructor(
 
 code_blockt recursive_initializationt::build_struct_constructor(
   const exprt &depth,
-  const exprt &result)
+  const symbol_exprt &result)
 {
   PRECONDITION(result.type().id() == ID_pointer);
   const typet &struct_type = result.type().subtype();
@@ -671,8 +673,8 @@ code_blockt recursive_initializationt::build_struct_constructor(
   return body;
 }
 
-code_blockt
-recursive_initializationt::build_nondet_constructor(const exprt &result) const
+code_blockt recursive_initializationt::build_nondet_constructor(
+  const symbol_exprt &result) const
 {
   PRECONDITION(result.type().id() == ID_pointer);
   code_blockt body{};
@@ -684,7 +686,7 @@ recursive_initializationt::build_nondet_constructor(const exprt &result) const
 
 code_blockt recursive_initializationt::build_dynamic_array_constructor(
   const exprt &depth,
-  const exprt &result,
+  const symbol_exprt &result,
   const exprt &size,
   const optionalt<irep_idt> &lhs_name)
 {
@@ -786,7 +788,7 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
 
 bool recursive_initializationt::needs_freeing(const exprt &expr) const
 {
-  if(expr.type().id() != ID_pointer)
+  if(expr.type().id() != ID_pointer || expr.type().subtype().id() == ID_code)
     return false;
   if(common_arguments_origin.has_value() && expr.id() == ID_symbol)
   {

src/goto-harness/recursive_initialization.h

@@ -168,15 +168,15 @@ class recursive_initializationt
   /// \return the body of the constructor
   code_blockt build_constructor_body(
     const exprt &depth_symbol,
-    const exprt &result_symbol,
+    const symbol_exprt &result_symbol,
     const optionalt<exprt> &size_symbol,
     const optionalt<irep_idt> &lhs_name);
 
   /// Check if a constructor for the type of \p expr already exists and create
   ///   it if not.
   /// \param expr: the expression to be constructed
   /// \return name of the constructor function
-  const irep_idt &build_constructor(const exprt &expr);
+  irep_idt build_constructor(const exprt &expr);
 
   /// Generic constructor for all pointers: only builds one pointee (not an
   ///   array) but may recourse in case the pointee contains more pointers, e.g.
@@ -185,26 +185,28 @@ class recursive_initializationt
   /// \param result: symbol of the result parameter
   /// \return the body of the constructor
   code_blockt
-  build_pointer_constructor(const exprt &depth, const exprt &result);
+  build_pointer_constructor(const exprt &depth, const symbol_exprt &result);
 
   /// Constructor for structures: simply iterates over members and initialise
   ///   each one.
   /// \param depth: symbol of the depth parameter
   /// \param result: symbol of the result parameter
   /// \return the body of the constructor
-  code_blockt build_struct_constructor(const exprt &depth, const exprt &result);
+  code_blockt
+  build_struct_constructor(const exprt &depth, const symbol_exprt &result);
 
   /// Default constructor: assigns non-deterministic value of the right type.
   /// \param result: symbol of the result parameter
   /// \return the body of the constructor
-  code_blockt build_nondet_constructor(const exprt &result) const;
+  code_blockt build_nondet_constructor(const symbol_exprt &result) const;
 
   /// Constructor for arrays: simply iterates over elements and initialise
   ///   each one.
   /// \param depth: symbol of the depth parameter
   /// \param result: symbol of the result parameter
   /// \return the body of the constructor
-  code_blockt build_array_constructor(const exprt &depth, const exprt &result);
+  code_blockt
+  build_array_constructor(const exprt &depth, const symbol_exprt &result);
 
   /// Constructor for dynamic arrays: allocate memory for `n` elements (`n` is
   ///   random but bounded) and initialise each one.
@@ -215,14 +217,14 @@ class recursive_initializationt
   /// \return the body of the constructor
   code_blockt build_dynamic_array_constructor(
     const exprt &depth,
-    const exprt &result,
+    const symbol_exprt &result,
     const exprt &size,
     const optionalt<irep_idt> &lhs_name);
 
   /// Constructor for strings: as array but the last element is zero.
   /// \param result: symbol of the result parameter
   /// \return the body of the constructor
-  code_blockt build_array_string_constructor(const exprt &result) const;
+  code_blockt build_array_string_constructor(const symbol_exprt &result) const;
 };
 
 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H