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>
Collaboration diagram for dfcc_contract_clauses_codegent: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. | |
| 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. | |
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. | |
| 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_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_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. | |
| 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. | |
Protected Attributes | |
| goto_modelt & | goto_model |
| message_handlert & | message_handler |
| messaget | log |
| dfcc_libraryt & | library |
| namespacet | ns |
Detailed Description
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 28 of file dfcc_contract_clauses_codegen.h.
Constructor & Destructor Documentation
◆ dfcc_contract_clauses_codegent()
| dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent | ( | goto_modelt & | goto_model, |
| message_handlert & | message_handler, | ||
| dfcc_libraryt & | library | ||
| ) |
- Parameters
-
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.
Member Function Documentation
◆ encode_assignable_target()
|
protected |
Generates GOTO instructions to build the representation of the given assignable target.
Definition at line 125 of file dfcc_contract_clauses_codegen.cpp.
◆ encode_assignable_target_group()
|
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.
◆ encode_freeable_target()
|
protected |
Generates GOTO instructions to build the representation of the given freeable target.
Definition at line 214 of file dfcc_contract_clauses_codegen.cpp.
◆ encode_freeable_target_group()
|
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.
◆ gen_spec_assigns_instructions()
| 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).
- Parameters
-
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.
◆ gen_spec_frees_instructions()
| 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).
- Parameters
-
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.
◆ inline_and_check_warnings()
|
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.
Member Data Documentation
◆ goto_model
|
protected |
Definition at line 70 of file dfcc_contract_clauses_codegen.h.
◆ library
|
protected |
Definition at line 73 of file dfcc_contract_clauses_codegen.h.
◆ log
|
protected |
Definition at line 72 of file dfcc_contract_clauses_codegen.h.
◆ message_handler
|
protected |
Definition at line 71 of file dfcc_contract_clauses_codegen.h.
◆ ns
|
protected |
Definition at line 74 of file dfcc_contract_clauses_codegen.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h
- /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
