69 const auto function_name =
id2string(function_symbol.get_identifier());
71 R
"(.*org\.cprover\.CProver\.nondet)"
72 R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))");
73 std::smatch match_results;
74 if(!std::regex_match(function_name, match_results, reg))
90 if(!(instr->is_function_call() && instr->get_code().id() == ID_code))
94 const auto &code = instr->get_code();
96 code.get_statement() == ID_function_call,
97 "function_call should have ID_function_call");
108 return expr.
id() == ID_symbol &&
119 if(!(expr.
id() == ID_typecast && expr.
operands().size() == 1))
124 if(!(typecast.op().id() == ID_symbol && !typecast.op().has_operands()))
130 return op_symbol.get_identifier() == identifier;
200 const auto next_instr = std::next(target);
202 instr_info.get_instruction_type() ==
210 const bool remove_returns_not_run = target->call_lhs().is_not_nil();
213 if(remove_returns_not_run)
221 next_instr->is_assign(),
222 "the code_function_callt for a nondet-returning library function should "
223 "either have a variable for the return value in its lhs() or the next "
224 "instruction should be an assignment of the return value to a temporary "
226 const exprt &return_value_assignment = next_instr->get_assign().lhs();
230 !(return_value_assignment.
id() == ID_symbol &&
244 auto target_instruction = std::find_if(
252 if(target_instruction == end)
254 target_instruction = std::find_if(
263 target_instruction != end,
264 "failed to find return of the temporary return variable or assignment of "
265 "the temporary return variable into a target variable");
272 if(target_instruction->is_set_return_value())
274 const auto &nondet_var = target_instruction->return_value();
277 nondet_var.type(), target_instruction->source_location);
279 instr_info.get_nullable_type() ==
281 target_instruction->code_nonconst() =
code_returnt(inserted_expr);
282 target_instruction->code_nonconst().add_source_location() =
283 target_instruction->source_location;
285 else if(target_instruction->is_assign())
288 const auto &nondet_var = target_instruction->get_assign().lhs();
291 nondet_var.type(), target_instruction->source_location);
293 instr_info.get_nullable_type() ==
295 target_instruction->code_nonconst() =
297 target_instruction->code_nonconst().add_source_location() =
298 target_instruction->source_location;
303 return std::next(target_instruction);
312 for(
auto instruction_iterator = goto_program.
instructions.begin(),
314 instruction_iterator != end;)
316 instruction_iterator =
A codet representing an assignment in the program.
codet representation of a function call statement.
codet representation of a "return from a function" statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool has_operands() const
Return true if there is at least one operand.
A collection of goto functions.
function_mapt function_map
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
bool is_set_return_value() const
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
instructionst::iterator targett
instructionst::const_iterator const_targett
const irep_idt & id() const
Holds information about any discovered nondet methods, with extreme type- safety.
nondet_instruction_infot()
is_nullablet get_nullable_type() const
is_nondett get_instruction_type() const
nondet_instruction_infot(is_nullablet is_nullable)
A side_effect_exprt that returns a non-deterministically chosen value.
void set_nullable(bool nullable)
const irep_idt & get_identifier() const
const std::string & id2string(const irep_idt &d)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
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.
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.
static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a symbol with the specified identifier.
static bool is_return_with_variable(const goto_programt::instructiont &instr, const irep_idt &identifier)
Return whether the instruction is a return, and the rhs is a symbol or typecast expression with the s...
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 ...
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...
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 ...
static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a typecast with the specified identifier.
Replace Java Nondet expressions.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const code_function_callt & to_code_function_call(const codet &code)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.