#include <dfcc_lift_memory_predicates.h>
◆ dfcc_lift_memory_predicatest()
- Parameters
-
| goto_model | The goto model to process |
| library | The contracts instrumentation library |
| instrument | The DFCC instrumenter object |
| message_handler | Used for messages |
Definition at line 25 of file dfcc_lift_memory_predicates.cpp.
◆ add_pointer_type()
| void dfcc_lift_memory_predicatest::add_pointer_type |
( |
const irep_idt & |
function_id, |
|
|
const std::size_t |
parameter_rank, |
|
|
replace_symbolt & |
replace_lifted_param |
|
) |
| |
|
protected |
adds a pointer_type to the parameter of a function
- Parameters
-
| function_id | The function to update |
| parameter_rank | The parameter to update |
| replace_lifted_param | Symbol replacer (receives p ~> *p mappings) The parameter symbol gets updated in the symbol table and the function signature gets updated with the new type. |
Definition at line 276 of file dfcc_lift_memory_predicates.cpp.
◆ calls_memory_predicates()
| bool dfcc_lift_memory_predicatest::calls_memory_predicates |
( |
const goto_programt & |
goto_program, |
|
|
const std::set< irep_idt > & |
predicates |
|
) |
| |
|
protected |
Returns true iff goto_program calls core memory predicates.
or one of the functions found in predicates .
Definition at line 52 of file dfcc_lift_memory_predicates.cpp.
◆ collect_parameters_to_lift()
| void dfcc_lift_memory_predicatest::collect_parameters_to_lift |
( |
const irep_idt & |
function_id | ) |
|
|
protected |
Computes the subset of function parameters of function_id that are passed directly to core predicates and must be lifted.
Definition at line 212 of file dfcc_lift_memory_predicates.cpp.
◆ fix_calls() [1/2]
| void dfcc_lift_memory_predicatest::fix_calls |
( |
goto_programt & |
program | ) |
|
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position.
Definition at line 394 of file dfcc_lift_memory_predicates.cpp.
◆ fix_calls() [2/2]
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to arguments passed in lifted position, between first_instruction (included) and last_instruction (excluded).
Definition at line 399 of file dfcc_lift_memory_predicates.cpp.
◆ is_lifted_function()
| bool dfcc_lift_memory_predicatest::is_lifted_function |
( |
const irep_idt & |
function_id | ) |
|
|
protected |
True if a function at least had one of its parameters lifted.
True if a function had at least one of its parameters lifted.
Definition at line 38 of file dfcc_lift_memory_predicates.cpp.
◆ lift_parameters_and_update_body()
| void dfcc_lift_memory_predicatest::lift_parameters_and_update_body |
( |
const irep_idt & |
function_id, |
|
|
std::set< irep_idt > & |
discovered_function_pointer_contracts |
|
) |
| |
|
protected |
◆ lift_predicate()
| void dfcc_lift_memory_predicatest::lift_predicate |
( |
const irep_idt & |
function_id, |
|
|
std::set< irep_idt > & |
discovered_function_pointer_contracts |
|
) |
| |
|
protected |
◆ lift_predicates()
| std::set< irep_idt > dfcc_lift_memory_predicatest::lift_predicates |
( |
std::set< irep_idt > & |
discovered_function_pointer_contracts | ) |
|
Collects and lifts all user-defined memory predicates.
- Parameters
-
| [out] | discovered_function_pointer_contracts | Set of function pointer contracts discovered during instrumentation |
- Returns
- The set of predicates that were lifted
Definition at line 76 of file dfcc_lift_memory_predicates.cpp.
◆ goto_model
◆ instrument
◆ library
◆ lifted_parameters
| std::map<irep_idt, std::set<std::size_t> > dfcc_lift_memory_predicatest::lifted_parameters |
|
protected |
◆ log
| messaget dfcc_lift_memory_predicatest::log |
|
protected |
The documentation for this class was generated from the following files:
Collaboration diagram for dfcc_lift_memory_predicatest: