48 for(
const auto &expr : assigns_clause)
67 "loops in assigns clause specification functions must be unwound before "
68 "contracts instrumentation");
76 for(
const auto &expr : frees_clause)
94 "loops in assigns clause specification functions must be unwound before "
95 "contracts instrumentation");
108 std::list<irep_idt> new_vars;
110 new_vars = cleaner.
clean(condition, dest, language_mode);
116 for(
const auto &target : group.
targets())
120 goto_instruction->complete_goto(label_instruction);
137 auto &arguments = code_function_call.
arguments();
138 for(
auto &arg : funcall.arguments())
139 arguments.emplace_back(arg);
150 if(!size.has_value())
153 "no definite size for lvalue assigns clause target " +
162 auto &arguments = code_function_call.
arguments();
169 arguments.emplace_back(size.value());
181 "unsupported assigns clause target " +
197 std::list<irep_idt> new_vars;
199 new_vars = cleaner.
clean(condition, dest, language_mode);
205 for(
const auto &target : group.
targets())
209 goto_instruction->complete_goto(label_instruction);
230 auto &arguments = code_function_call.
arguments();
231 for(
auto &arg : funcall.arguments())
232 arguments.emplace_back(arg);
244 auto &arguments = code_function_call.
arguments();
245 arguments.emplace_back(target);
254 "unsupported frees clause target " +
263 std::set<irep_idt> no_body;
264 std::set<irep_idt> missing_function;
265 std::set<irep_idt> recursive_call;
266 std::set<irep_idt> not_enough_arguments;
274 not_enough_arguments,
278 for(
const auto &
id : no_body)
281 library.is_front_end_builtin(
id),
282 "no body for '" +
id2string(
id) +
"' when inlining goto program");
285 for(
auto it : missing_function)
288 library.is_front_end_builtin(it),
289 "missing function '" +
id2string(it) +
"' when inlining goto program");
293 recursive_call.empty(),
"recursive calls found when inlining goto program");
296 not_enough_arguments.empty(),
297 "not enough arguments when inlining goto program");
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
std::list< irep_idt > clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
goto_instruction_codet representation of a function call statement.
A class for an expression that represents a conditional target or a list of targets sharing a common ...
const exprt::operandst & targets() const
const exprt & condition() const
void encode_freeable_target_group(const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
Generates GOTO instructions to build the representation of the given conditional target group.
void encode_assignable_target(const irep_idt &language_mode, const exprt &target, goto_programt &dest)
Generates GOTO instructions to build the representation of the given assignable target.
void encode_assignable_target_group(const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
Generates GOTO instructions to build the representation of the given conditional target group.
void gen_spec_assigns_instructions(const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
Generates instructions encoding the assigns_clause targets and adds them to dest.
void encode_freeable_target(const irep_idt &language_mode, const exprt &target, goto_programt &dest)
Generates GOTO instructions to build the representation of the given freeable target.
message_handlert & message_handler
void gen_spec_frees_instructions(const irep_idt &language_mode, const exprt::operandst &frees_clause, goto_programt &dest)
Generates instructions encoding the frees_clause targets and adds them to dest.
void inline_and_check_warnings(goto_programt &goto_program)
Inlines all calls in the given program and checks that the only missing functions or functions withou...
dfcc_contract_clauses_codegent(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
Class interface to library types and functions defined in cprover_contracts.c.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
void update()
Update all indices.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Thrown when we can't handle something in an input source file.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a symbol (variable)
static exprt conditional_cast(const exprt &expr, const typet &type)
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Dynamic frame condition checking library loading.
Dynamic frame condition checking utility functions.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
const std::string & id2string(const irep_idt &d)
std::string from_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
API to expression classes for 'mathematical' expressions.
API to expression classes for Pointers.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static void inline_program(goto_modelt &goto_model, goto_programt &goto_program, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > ¬_enough_arguments, message_handlert &message_handler)
Inlines the given program, and returns function symbols that caused warnings.
bool is_loop_free(const goto_programt &goto_program, const namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.