CBMC
|
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that build write sets or havoc write sets. More...
#include <dfcc_contract_clauses_codegen.h>
Public Member Functions | |
dfcc_contract_clauses_codegent (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library) | |
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 . More... | |
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 . More... | |
Protected Member Functions | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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 without bodies are built-in functions, and that no other warnings happened. More... | |
Protected Attributes | |
goto_modelt & | goto_model |
message_handlert & | message_handler |
messaget | log |
dfcc_libraryt & | library |
namespacet | ns |
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that build write sets or havoc write sets.
Definition at line 35 of file dfcc_contract_clauses_codegen.h.
dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
dfcc_libraryt & | library | ||
) |
goto_model | GOTO model being transformed |
message_handler | Used debug/warning/error messages |
library | The contracts instrumentation library |
Definition at line 31 of file dfcc_contract_clauses_codegen.cpp.
|
protected |
Generates GOTO instructions to build the representation of the given assignable target.
Definition at line 125 of file dfcc_contract_clauses_codegen.cpp.
|
protected |
Generates GOTO instructions to build the representation of the given conditional target group.
Definition at line 98 of file dfcc_contract_clauses_codegen.cpp.
|
protected |
Generates GOTO instructions to build the representation of the given freeable target.
Definition at line 214 of file dfcc_contract_clauses_codegen.cpp.
|
protected |
Generates GOTO instructions to build the representation of the given conditional target group.
Definition at line 187 of file dfcc_contract_clauses_codegen.cpp.
void dfcc_contract_clauses_codegent::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
.
Assumes that all targets in the clause are represented as plain expressions (i.e. an lambdas expressions introduced for function contract targets may are already instanciated).
language_mode | Mode to use for fresh symbols |
assigns_clause | Sequence of targets to encode |
dest | Destination program |
Definition at line 43 of file dfcc_contract_clauses_codegen.cpp.
void dfcc_contract_clauses_codegent::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
.
Assumes that all targets in the clause are represented as plain expressions (i.e. an lambdas expressions introduced for function contract targets may are already instanciated).
language_mode | Mode to use for fresh symbols |
frees_clause | Sequence of targets to encode |
dest | Destination program |
Definition at line 71 of file dfcc_contract_clauses_codegen.cpp.
|
protected |
Inlines all calls in the given program and checks that the only missing functions or functions without bodies are built-in functions, and that no other warnings happened.
Definition at line 260 of file dfcc_contract_clauses_codegen.cpp.
|
protected |
Definition at line 77 of file dfcc_contract_clauses_codegen.h.
|
protected |
Definition at line 80 of file dfcc_contract_clauses_codegen.h.
|
protected |
Definition at line 79 of file dfcc_contract_clauses_codegen.h.
|
protected |
Definition at line 78 of file dfcc_contract_clauses_codegen.h.
|
protected |
Definition at line 81 of file dfcc_contract_clauses_codegen.h.