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>
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 36 of file dfcc_contract_clauses_codegen.h.
◆ dfcc_contract_clauses_codegent()
- Parameters
-
goto_model | GOTO model being transformed |
message_handler | Used debug/warning/error messages |
library | The contracts instrumentation library |
Definition at line 30 of file dfcc_contract_clauses_codegen.cpp.
◆ encode_assignable_target()
void dfcc_contract_clauses_codegent::encode_assignable_target |
( |
const irep_idt & | language_mode, |
|
|
const exprt & | target, |
|
|
goto_programt & | dest ) |
|
protected |
◆ encode_assignable_target_group()
◆ encode_freeable_target()
void dfcc_contract_clauses_codegent::encode_freeable_target |
( |
const irep_idt & | language_mode, |
|
|
const exprt & | target, |
|
|
goto_programt & | dest ) |
|
protected |
◆ encode_freeable_target_group()
◆ gen_spec_assigns_instructions()
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).
- Parameters
-
language_mode | Mode to use for fresh symbols |
assigns_clause | Sequence of targets to encode |
dest | Destination program |
Definition at line 42 of file dfcc_contract_clauses_codegen.cpp.
◆ gen_spec_frees_instructions()
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).
- Parameters
-
language_mode | Mode to use for fresh symbols |
frees_clause | Sequence of targets to encode |
dest | Destination program |
Definition at line 70 of file dfcc_contract_clauses_codegen.cpp.
◆ inline_and_check_warnings()
void dfcc_contract_clauses_codegent::inline_and_check_warnings |
( |
goto_programt & | goto_program | ) |
|
|
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 253 of file dfcc_contract_clauses_codegen.cpp.
◆ goto_model
goto_modelt& dfcc_contract_clauses_codegent::goto_model |
|
protected |
◆ library
◆ log
messaget dfcc_contract_clauses_codegent::log |
|
protected |
◆ message_handler
◆ ns
The documentation for this class was generated from the following files: