70 const auto function_name =
id2string(function_symbol.get_identifier());
72 R
"(.*org\.cprover\.CProver\.nondet)" 73 R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))"); 74 std::smatch match_results; 75 if(!std::regex_match(function_name, match_results, reg))
91 if(!(instr->is_function_call() && instr->code.id() == ID_code))
95 const auto &code =
to_code(instr->code);
96 if(code.get_statement() != ID_function_call)
110 return expr.
id() == ID_symbol &&
121 if(!(expr.
id() == ID_typecast && expr.
operands().size() == 1))
126 if(!(typecast.op().id() == ID_symbol && !typecast.op().has_operands()))
180 const auto next_instr = std::next(target);
182 instr_info.get_instruction_type() ==
190 const bool remove_returns_not_run =
194 if(remove_returns_not_run)
204 next_instr->is_assign(),
205 "the code_function_callt for a nondet-returning library function should " 206 "either have a variable for the return value in its lhs() or the next " 207 "instruction should be an assignment of the return value to a temporary " 209 const exprt &return_value_assignment =
214 !(return_value_assignment.id() == ID_symbol &&
215 !return_value_assignment.has_operands()))
228 auto assignment_instruction = std::find_if(
236 assignment_instruction != end,
237 "failed to find assignment of the temporary return variable into our " 241 const auto &code_assign =
to_code_assign(assignment_instruction->code);
242 const auto nondet_var = code_assign.lhs();
243 const auto source_loc = target->source_location;
246 const auto after_matching_assignment = std::next(assignment_instruction);
248 after_matching_assignment != end,
249 "goto_program missing END_FUNCTION instruction");
257 inserted->make_assignment();
260 instr_info.get_nullable_type() ==
262 inserted->code =
code_assignt(nondet_var, inserted_expr);
263 inserted->code.add_source_location() = source_loc;
264 inserted->source_location = source_loc;
268 return after_matching_assignment;
279 instruction_iterator != end;)
281 instruction_iterator =
void update()
Update all indices.
Holds information about any discovered nondet methods, with extreme type- safety. ...
const std::string & id2string(const irep_idt &d)
targett insert_before(const_targett target)
Insertion before the given target.
const irep_idt & get_identifier() const
static bool is_assignment_from(const goto_programt::instructiont &instr, const irep_idt &identifier)
Return whether the instruction is an assignment, and the rhs is a symbol or typecast expression with ...
function_mapt function_map
#define INVARIANT(CONDITION, REASON)
This class represents an instruction in the GOTO intermediate representation.
void set_nullable(bool nullable)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
instructionst::iterator targett
is_nondett get_instruction_type() const
instructionst instructions
The list of instructions in the goto program.
static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a symbol with the specified identifier.
instructionst::const_iterator const_targett
nondet_instruction_infot(is_nullablet is_nullable)
static goto_programt::targett check_and_replace_target(goto_programt &goto_program, const goto_programt::targett &target)
Given an iterator into a list of instructions, modify the list to replace 'nondet' library functions ...
A side effect that returns a non-deterministically chosen value.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Replace Java Nondet expressions.
static nondet_instruction_infot get_nondet_instruction_info(const goto_programt::const_targett &instr)
Check whether the instruction is a function call which matches one of the recognised nondet library m...
A generic container class for the GOTO intermediate representation of one function.
static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a typecast with the specified identifier.
Base class for all expressions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
nondet_instruction_infot()
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
static nondet_instruction_infot is_nondet_returning_object(const code_function_callt &function_call)
Checks whether the function call is one of our nondet library functions.
goto_programt & goto_program
const codet & to_code(const exprt &expr)
static void replace_java_nondet(goto_programt &goto_program)
Checks each instruction in the goto program to see whether it is a method returning nondet...
#define DATA_INVARIANT(CONDITION, REASON)
goto_functionst goto_functions
GOTO functions.
const code_function_callt & to_code_function_call(const codet &code)
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
is_nullablet get_nullable_type() const