14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
A generic container class for the GOTO intermediate representation of one function.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Enum type representing the contract checking and replacement modes.
API to expression classes.