Sanity check user specified havoc parameters

1: check the function actually takes that many parameters
2: check the parameter type is a pointer

Adds tests and extends the documentation.

Author: petr-bauch

doc/cprover-manual/goto-instrument.md

@@ -118,6 +118,11 @@ int main() {
 }
 ```
 
+Note that only parameters of pointer type can be havoc(ed) and CBMC will produce
+an error report if given a parameter number associated with a non-pointer
+parameter. Requesting to havoc a parameter with a number higher than the number
+of parameters a given function takes will also results in an error report.
+
 ### Loop Transformations
 
 ### Memory Model Instrumentations

regression/goto-instrument/generate-function-body-havoc-params-call-sites/main.c

@@ -6,14 +6,18 @@ struct S
   char *j;
 };
 
-void touches_parameter(int *param, int *const_param, struct S *struct_param);
+void touches_parameter(
+  int *param,
+  int *const_param,
+  struct S *struct_param,
+  int non_pointer_param);
 
 int main(void)
 {
   int parameter = 10;
   int unchanged_parameter = 10;
   struct S my_struct = {.i = 10, .j = "10"};
-  touches_parameter(&parameter, &unchanged_parameter, &my_struct);
+  touches_parameter(&parameter, &unchanged_parameter, &my_struct, 4);
   assert(parameter == 10);
   assert(unchanged_parameter == 10);
   assert(my_struct.i == 10);
@@ -23,7 +27,7 @@ int main(void)
   unchanged_parameter = 10;
   my_struct.i = 10;
   my_struct.j = "10";
-  touches_parameter(&parameter, &unchanged_parameter, &my_struct);
+  touches_parameter(&parameter, &unchanged_parameter, &my_struct, 4);
   assert(parameter == 10);
   assert(unchanged_parameter == 10);
   assert(my_struct.i == 10);

regression/goto-instrument/generate-function-body-havoc-params-call-sites/non_pointer_param.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-havocing-body 'touches_parameter,1,params:0;3,2,params:1'
+^EXIT=1$
+^SIGNAL=0$
+^Reason: argument number 3 of function touches_parameter.1 is not a pointer$
+--
+^warning: ignoring

regression/goto-instrument/generate-function-body-havoc-params-call-sites/too_high_param_number.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-havocing-body 'touches_parameter,1,params:0;5,2,params:1'
+^EXIT=1$
+^SIGNAL=0$
+^Reason: function touches_parameter.1 does not take 6 arguments$
+--
+^warning: ignoring

src/goto-instrument/generate_function_bodies.cpp

@@ -236,6 +236,33 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
     symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
+    const namespacet ns(symbol_table);
+    // some user input checking
+    if(param_numbers_to_havoc.has_value() && !param_numbers_to_havoc->empty())
+    {
+      auto max_param_number = std::max_element(
+        param_numbers_to_havoc->begin(), param_numbers_to_havoc->end());
+      if(*max_param_number >= function.parameter_identifiers.size())
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "function " + id2string(function_name) + " does not take " +
+            std::to_string(*max_param_number + 1) + " arguments",
+          "--generate-havocing-body"};
+      }
+      for(const auto number : *param_numbers_to_havoc)
+      {
+        const auto &parameter = function.parameter_identifiers[number];
+        const symbolt &parameter_symbol = ns.lookup(parameter);
+        if(parameter_symbol.type.id() != ID_pointer)
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "argument number " + std::to_string(number) + " of function " +
+              id2string(function_name) + " is not a pointer",
+            "--generate-havocing-body"};
+        }
+      }
+    }
+
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
     // NOLINTNEXTLINE
     auto add_instruction = [&](goto_programt::instructiont &&i) {
@@ -244,7 +271,6 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
       return instruction;
     };
 
-    const namespacet ns(symbol_table);
     for(std::size_t i = 0; i < function.parameter_identifiers.size(); ++i)
     {
       const auto &parameter = function.parameter_identifiers[i];