CBMC
Loading...
Searching...
No Matches
dfcc_lift_memory_predicates.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: Remi Delmas, delmasrd@amazon.com
6Date: November 2022
7
8\*******************************************************************/
9
18
19#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H
20#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H
21
22#include <util/message.h>
23
25
26#include <map>
27#include <set>
28
29class dfcc_libraryt;
32class goto_modelt;
33class replace_symbolt;
34
36{
37public:
46 message_handlert &message_handler);
47
52 std::set<irep_idt>
54
57 void fix_calls(goto_programt &program);
58
62 void fix_calls(
63 goto_programt &program,
66
67protected:
72 // index of lifted parameters for lifted functions
73 std::map<irep_idt, std::set<std::size_t>> lifted_parameters;
74
78 const goto_programt &goto_program,
79 const std::set<irep_idt> &predicates);
80
81 void lift_predicate(
82 const irep_idt &function_id,
83 std::set<irep_idt> &discovered_function_pointer_contracts);
84
86 const irep_idt &function_id,
87 std::set<irep_idt> &discovered_function_pointer_contracts);
88
96 const irep_idt &function_id,
97 const std::size_t parameter_rank,
99
102 void collect_parameters_to_lift(const irep_idt &function_id);
103
105 bool is_lifted_function(const irep_idt &function_id);
106};
107
108#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
void fix_calls(goto_programt &program)
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to argume...
void collect_parameters_to_lift(const irep_idt &function_id)
Computes the subset of function parameters of function_id that are passed directly to core predicates...
void lift_predicate(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
void add_pointer_type(const irep_idt &function_id, const std::size_t parameter_rank, replace_symbolt &replace_lifted_param)
adds a pointer_type to the parameter of a function
std::map< irep_idt, std::set< std::size_t > > lifted_parameters
void lift_parameters_and_update_body(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
bool calls_memory_predicates(const goto_programt &goto_program, const std::set< irep_idt > &predicates)
Returns true iff goto_program calls core memory predicates.
bool is_lifted_function(const irep_idt &function_id)
True if a function at least had one of its parameters lifted.
std::set< irep_idt > lift_predicates(std::set< irep_idt > &discovered_function_pointer_contracts)
Collects and lifts all user-defined memory predicates.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
Replace a symbol expression by a given expression.
Concrete Goto Program.