diff --git a/regression/goto-harness/function_pointer_argument/test.c b/regression/goto-harness/function_pointer_argument/test.c new file mode 100644 index 00000000000..6b1fa95af7a --- /dev/null +++ b/regression/goto-harness/function_pointer_argument/test.c @@ -0,0 +1,20 @@ +#include + +typedef int (*fptr)(int a, int b); + +int max_normal(int first, int second) +{ + return first >= second ? first : second; +} + +int max_crazy(int first, int second) +{ + return first >= second ? second : first; +} + +void use_fptr(fptr max, int first, int second) +{ + int m = max(first, second); + assert(m == first || m == second); + assert(m >= first && m >= second); +} diff --git a/regression/goto-harness/function_pointer_argument/test.desc b/regression/goto-harness/function_pointer_argument/test.desc new file mode 100644 index 00000000000..5b596a989b7 --- /dev/null +++ b/regression/goto-harness/function_pointer_argument/test.desc @@ -0,0 +1,9 @@ +CORE +test.c +--harness-type call-function --harness-function-name harness --function use_fptr +^EXIT=10$ +^SIGNAL=0$ +\[use_fptr.assertion.1\] line \d+ assertion m == first \|\| m == second: SUCCESS +\[use_fptr.assertion.2\] line \d+ assertion m >= first && m >= second: FAILURE +-- +^warning: ignoring diff --git a/regression/goto-harness/function_pointer_nullable/test.c b/regression/goto-harness/function_pointer_nullable/test.c new file mode 100644 index 00000000000..13a0c3eec61 --- /dev/null +++ b/regression/goto-harness/function_pointer_nullable/test.c @@ -0,0 +1,18 @@ +#include +#include + +typedef int (*fptr_t)(void); + +void entry_point(fptr_t f, fptr_t f_but_may_be_null) +{ + assert(f != (void *)0); // expected to succeed + assert(f == (void *)0); // expected to fail + assert(f_but_may_be_null != (void *)0); // expected to fail + assert(f_but_may_be_null == (void *)0); // expected to fail + assert(f_but_may_be_null == (void *)0 || f() == f_but_may_be_null()); +} + +int f(void) +{ + return 42; +} diff --git a/regression/goto-harness/function_pointer_nullable/test.desc b/regression/goto-harness/function_pointer_nullable/test.desc new file mode 100644 index 00000000000..659a84a28c5 --- /dev/null +++ b/regression/goto-harness/function_pointer_nullable/test.desc @@ -0,0 +1,12 @@ +CORE +test.c +--harness-type call-function --function entry_point --function-pointer-can-be-null entry_point::f_but_may_be_null +^EXIT=10$ +^SIGNAL=0$ +\[entry_point.assertion.1\] line \d+ assertion f != \(void \*\)0: SUCCESS +\[entry_point.assertion.2\] line \d+ assertion f == \(void \*\)0: FAILURE +\[entry_point.assertion.3\] line \d+ assertion f_but_may_be_null != \(void \*\)0: FAILURE +\[entry_point.assertion.4\] line \d+ assertion f_but_may_be_null == \(void \*\)0: FAILURE +\[entry_point.assertion.5\] line \d+ assertion f_but_may_be_null == \(void \*\)0 || f\(\) == f_but_may_be_null\(\): SUCCESS +-- +^warning: ignoring diff --git a/regression/goto-harness/mixed-constructors/test.c b/regression/goto-harness/mixed-constructors/test.c new file mode 100644 index 00000000000..c820829edc6 --- /dev/null +++ b/regression/goto-harness/mixed-constructors/test.c @@ -0,0 +1,5 @@ +void entry_point(int *array_with_size, int size, int *array_without_size) +{ + assert(array_with_size != (void *)0); + assert(array_with_size != (void *)0); +} diff --git a/regression/goto-harness/mixed-constructors/test.desc b/regression/goto-harness/mixed-constructors/test.desc new file mode 100644 index 00000000000..4c21c51d75e --- /dev/null +++ b/regression/goto-harness/mixed-constructors/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--function entry_point --harness-type call-function --associated-array-size array_with_size:size +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +call to '\w+': not enough arguments, inserting non-deterministic value diff --git a/regression/goto-harness/parameter_and_global_variable_distinction/test.c b/regression/goto-harness/parameter_and_global_variable_distinction/test.c new file mode 100644 index 00000000000..687549bfcff --- /dev/null +++ b/regression/goto-harness/parameter_and_global_variable_distinction/test.c @@ -0,0 +1,18 @@ +#include + +typedef int (*fptr_t)(void); + +fptr_t f; + +int call_f() +{ + assert(f != ((void *)0)); + return f(); +} + +void function(fptr_t f) +{ + if(f != ((void *)0)) + assert(f() == call_f()); + assert(f != ((void *)0)); +} diff --git a/regression/goto-harness/parameter_and_global_variable_distinction/test.desc b/regression/goto-harness/parameter_and_global_variable_distinction/test.desc new file mode 100644 index 00000000000..f5e5c464a1d --- /dev/null +++ b/regression/goto-harness/parameter_and_global_variable_distinction/test.desc @@ -0,0 +1,10 @@ +CORE +test.c +--harness-type call-function --function function --function-pointer-can-be-null function::f +^EXIT=10$ +^SIGNAL=0$ +\[function.assertion.1\] line \d+ assertion f\(\) == call_f\(\): SUCCESS +\[function.assertion.2\] line \d+ assertion f != \(\(void \*\)0\): FAILURE +\[call_f.assertion.1\] line \d+ assertion f != \(\(void \*\)0\): SUCCESS +-- +^warning: ignoring diff --git a/src/goto-harness/common_harness_generator_options.h b/src/goto-harness/common_harness_generator_options.h index 844309f59b3..9a4c396133d 100644 --- a/src/goto-harness/common_harness_generator_options.h +++ b/src/goto-harness/common_harness_generator_options.h @@ -14,6 +14,8 @@ Author: Diffblue Ltd. "max-nondet-tree-depth" #define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size" #define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size" +#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ + "function-pointer-can-be-null" // clang-format off #define COMMON_HARNESS_GENERATOR_OPTIONS \ @@ -21,6 +23,7 @@ Author: Diffblue Ltd. "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):" \ "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):" \ "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \ + "(" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT "):" \ // COMMON_HARNESS_GENERATOR_OPTIONS // clang-format on @@ -39,6 +42,9 @@ Author: Diffblue Ltd. "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \ " N maximum size of dynamically created arrays\n" \ " (default: 2)\n" \ + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ + " , name of the function(s) pointer parameters\n" \ + " that can be NULL pointing." // COMMON_HARNESS_GENERATOR_HELP // clang-format on diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index b7f26a1d649..ff8728adcc1 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -12,6 +12,7 @@ Author: Diffblue Ltd. #include #include #include +#include #include #include #include @@ -72,14 +73,24 @@ 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, code_blockt &function_body); + /// For function parameters that are pointers to functions we want to + /// be able to specify whether or not they can be NULL. To disambiguate + /// this specification from that for a global variable of the same name, + /// we prepend the name of the function to the parameter name. However, + /// what is actually being initialised in the implementation is not the + /// parameter itself, but a corresponding function argument (local variable + /// of the harness function). We need a mapping from function parameter + /// name to function argument names, and this is what this function does. + std::unordered_set + map_function_parameters_to_function_argument_names(); }; function_call_harness_generatort::function_call_harness_generatort( @@ -173,6 +184,30 @@ void function_call_harness_generatort::handle_option( { p_impl->recursive_initialization_config.arguments_may_be_equal = true; } + else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT) + { + std::transform( + values.begin(), + values.end(), + std::inserter( + p_impl->recursive_initialization_config + .potential_null_function_pointers, + p_impl->recursive_initialization_config.potential_null_function_pointers + .end()), + [](const std::string &opt) -> irep_idt { return irep_idt{opt}; }); + } + else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT) + { + std::transform( + values.begin(), + values.end(), + std::inserter( + p_impl->recursive_initialization_config + .potential_null_function_pointers, + p_impl->recursive_initialization_config.potential_null_function_pointers + .end()), + [](const std::string &opt) -> irep_idt { return irep_idt{opt}; }); + } else { throw invalid_command_line_argument_exceptiont{ @@ -214,6 +249,8 @@ void function_call_harness_generatort::implt::generate( recursive_initialization_config.variables_that_hold_array_sizes.insert( pair.second); } + recursive_initialization_config.potential_null_function_pointers = + map_function_parameters_to_function_argument_names(); recursive_initialization_config.pointers_to_treat_as_cstrings = function_arguments_to_treat_as_cstrings; recursive_initialization = util_make_unique( @@ -269,7 +306,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}; @@ -283,8 +320,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 &equal_cluster : p_impl->function_parameters_to_treat_equal) { for(auto const &pointer_id : equal_cluster) @@ -325,6 +371,43 @@ void function_call_harness_generatort::validate_options( } } } + + const namespacet ns{goto_model.symbol_table}; + + // Make sure all function pointers that the user asks are nullable are + // present in the symbol table. + for(const auto &nullable : + p_impl->recursive_initialization_config.potential_null_function_pointers) + { + const auto &function_pointer_symbol_pointer = + goto_model.symbol_table.lookup(nullable); + + if(function_pointer_symbol_pointer == nullptr) + { + throw invalid_command_line_argument_exceptiont{ + "nullable function pointer `" + id2string(nullable) + + "' not found in symbol table", + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT}; + } + + const auto &function_pointer_type = + ns.follow(function_pointer_symbol_pointer->type); + + if(!can_cast_type(function_pointer_type)) + { + throw invalid_command_line_argument_exceptiont{ + "`" + id2string(nullable) + "' is not a pointer", + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT}; + } + + if(!can_cast_type( + to_pointer_type(function_pointer_type).subtype())) + { + throw invalid_command_line_argument_exceptiont{ + "`" + id2string(nullable) + "' is not pointing to a function", + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT}; + } + } } const symbolt & @@ -469,3 +552,25 @@ void function_call_harness_generatort::implt::call_function( function_body.add(std::move(function_call)); } + +std::unordered_set function_call_harness_generatort::implt:: + map_function_parameters_to_function_argument_names() +{ + std::unordered_set nullables; + for(const auto &nullable : + recursive_initialization_config.potential_null_function_pointers) + { + const auto &nullable_name = id2string(nullable); + const auto &function_prefix = id2string(function) + "::"; + if(has_prefix(nullable_name, function_prefix)) + { + nullables.insert( + "__goto_harness::" + nullable_name.substr(function_prefix.size())); + } + else + { + nullables.insert(nullable_name); + } + } + return nullables; +} diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 537ba8c8b4d..2ba446def5b 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -21,6 +21,7 @@ Author: Diffblue Ltd. #include #include +#include bool recursive_initialization_configt::handle_option( const std::string &option, @@ -74,6 +75,17 @@ bool recursive_initialization_configt::handle_option( COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values); return true; } + else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT) + { + std::transform( + values.begin(), + values.end(), + std::inserter( + potential_null_function_pointers, + potential_null_function_pointers.end()), + [](const std::string &opt) -> irep_idt { return irep_idt{opt}; }); + return true; + } return false; } @@ -185,9 +197,10 @@ 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 &size_symbol, - const optionalt &lhs_name) + const optionalt &lhs_name, + const bool is_nullable) { PRECONDITION(result_symbol.type().id() == ID_pointer); const typet &type = result_symbol.type().subtype(); @@ -197,6 +210,10 @@ code_blockt recursive_initializationt::build_constructor_body( } else if(type.id() == ID_pointer) { + if(type.subtype().id() == ID_code) + { + return build_function_pointer_constructor(result_symbol, is_nullable); + } if(lhs_name.has_value()) { if(should_be_treated_as_cstring(*lhs_name) && type == char_type()) @@ -220,7 +237,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: // @@ -231,15 +248,23 @@ const irep_idt &recursive_initializationt::build_constructor(const exprt &expr) // void type_constructor_T(int depth_T, T *result_T, int *size); optionalt size_var; optionalt expr_name; + bool is_nullable = false; + bool has_size_param = false; if(expr.id() == ID_symbol) { expr_name = to_symbol_expr(expr).get_identifier(); + is_nullable = initialization_config.potential_null_function_pointers.count( + expr_name.value()); if(should_be_treated_as_array(*expr_name)) + { size_var = get_associated_size_variable(*expr_name); + has_size_param = true; + } } const typet &type = expr.type(); - if(type_constructor_names.find(type) != type_constructor_names.end()) - return type_constructor_names[type]; + const constructor_keyt key{type, is_nullable, has_size_param}; + if(type_constructor_names.find(key) != type_constructor_names.end()) + return type_constructor_names[key]; const std::string &pretty_type = type2id(type); symbolt &depth_symbol = @@ -280,7 +305,7 @@ const irep_idt &recursive_initializationt::build_constructor(const exprt &expr) } const symbolt &function_symbol = get_fresh_fun_symbol( "type_constructor_" + pretty_type, code_typet{fun_params, empty_typet{}}); - type_constructor_names[type] = function_symbol.name; + type_constructor_names[key] = function_symbol.name; symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.name); // the body is specific for each type of expression @@ -290,11 +315,12 @@ const irep_idt &recursive_initializationt::build_constructor(const exprt &expr) size_symbol_expr, // the expression name may be needed to decide if expr should be treated as // a string - expr_name); + expr_name, + is_nullable); goto_model.goto_functions.function_map[function_symbol.name].type = to_code_type(function_symbol.type); - return type_constructor_names[type]; + return type_constructor_names.at(key); } symbol_exprt recursive_initializationt::get_malloc_function() @@ -554,7 +580,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(); @@ -639,7 +665,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(); @@ -668,7 +694,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(); @@ -690,7 +716,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(); @@ -705,8 +731,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{}; @@ -718,7 +744,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 &lhs_name) { @@ -820,7 +846,19 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor( bool recursive_initializationt::needs_freeing(const exprt &expr) const { - return expr.type().id() == ID_pointer && expr.type().id() != ID_code; + if(expr.type().id() != ID_pointer || expr.type().subtype().id() == ID_code) + return false; + for(auto const &common_arguments_origin : common_arguments_origins) + { + if(common_arguments_origin.has_value() && expr.id() == ID_symbol) + { + auto origin_name = + to_symbol_expr(*common_arguments_origin).get_identifier(); + auto expr_name = to_symbol_expr(expr).get_identifier(); + return origin_name == expr_name; + } + } + return true; } void recursive_initializationt::free_if_possible( @@ -863,3 +901,58 @@ void recursive_initializationt::free_cluster_origins(code_blockt &body) body.add(code_function_callt{get_free_function(), {*origin}}); } } + +code_blockt recursive_initializationt::build_function_pointer_constructor( + const symbol_exprt &result, + bool is_nullable) +{ + PRECONDITION(can_cast_type(result.type())); + const auto &result_type = to_pointer_type(result.type()); + PRECONDITION(can_cast_type(result_type.subtype())); + const auto &function_pointer_type = to_pointer_type(result_type.subtype()); + PRECONDITION(can_cast_type(function_pointer_type.subtype())); + const auto &function_type = to_code_type(function_pointer_type.subtype()); + + std::vector targets; + + for(const auto &sym : goto_model.get_symbol_table()) + { + if(sym.second.type == function_type) + { + targets.push_back(address_of_exprt{sym.second.symbol_expr()}); + } + } + + if(is_nullable) + targets.push_back(null_pointer_exprt{function_pointer_type}); + + code_blockt body{}; + + const auto function_pointer_selector = + get_fresh_local_symexpr("function_pointer_selector"); + body.add( + code_assignt{function_pointer_selector, + side_effect_expr_nondett{function_pointer_selector.type(), + source_locationt{}}}); + auto function_pointer_index = std::size_t{0}; + + for(const auto &target : targets) + { + auto const assign = code_assignt{dereference_exprt{result}, target}; + if(function_pointer_index != targets.size() - 1) + { + auto const condition = equal_exprt{ + function_pointer_selector, + from_integer(function_pointer_index, function_pointer_selector.type())}; + auto const then = code_blockt{{assign, code_returnt{}}}; + body.add(code_ifthenelset{condition, then}); + } + else + { + body.add(assign); + } + ++function_pointer_index; + } + + return body; +} diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index 5b0dfdac37d..725fec9efdf 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -27,6 +27,7 @@ struct recursive_initialization_configt std::size_t min_null_tree_depth = 1; std::size_t max_nondet_tree_depth = 2; irep_idt mode; + std::unordered_set potential_null_function_pointers; // array stuff std::size_t max_dynamic_array_size = 2; @@ -59,8 +60,30 @@ class recursive_initializationt { public: using recursion_sett = std::set; - using type_constructor_namest = std::map; using equal_cluster_idt = std::size_t; + struct constructor_keyt + { + typet constructor_type; + bool is_nullable; + bool has_size_parameter; + bool operator<(const constructor_keyt &other) const + { + return std::tie(constructor_type, is_nullable, has_size_parameter) < + std::tie( + other.constructor_type, + other.is_nullable, + other.has_size_parameter); + }; + bool operator==(const constructor_keyt &other) const + { + return std::tie(constructor_type, is_nullable, has_size_parameter) == + std::tie( + other.constructor_type, + other.is_nullable, + other.has_size_parameter); + }; + }; + using type_constructor_namest = std::map; recursive_initializationt( recursive_initialization_configt initialization_config, @@ -170,18 +193,28 @@ class recursive_initializationt /// \param result_symbol: the symbol for `result` parameter /// \param size_symbol: maybe the symbol for `size` parameter /// \param lhs_name: the name of the original symbol + /// \param is_nullable: flag for setting a function pointer nullable /// \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 &size_symbol, - const optionalt &lhs_name); + const optionalt &lhs_name, + const bool is_nullable); /// 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); + + /// Constructor for function pointers. + /// \param result: symbol of the result parameter + /// \param is_nullable: if the function pointer can be null + /// \return the body of the constructor + code_blockt build_function_pointer_constructor( + const symbol_exprt &result, + bool is_nullable); /// Generic constructor for all pointers: only builds one pointee (not an /// array) but may recourse in case the pointee contains more pointers, e.g. @@ -190,26 +223,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. @@ -220,14 +255,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 &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