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. 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 |
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 35 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 30 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 121 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 97 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 207 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 183 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 42 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 70 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 253 of file dfcc_contract_clauses_codegen.cpp.
Member Data Documentation
◆ goto_model
|
protected |
Definition at line 77 of file dfcc_contract_clauses_codegen.h.
◆ library
|
protected |
Definition at line 80 of file dfcc_contract_clauses_codegen.h.
◆ log
|
protected |
Definition at line 79 of file dfcc_contract_clauses_codegen.h.
◆ message_handler
|
protected |
Definition at line 78 of file dfcc_contract_clauses_codegen.h.
◆ ns
|
protected |
Definition at line 81 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
