CBMC
Loading...
Searching...
No Matches
dfcc_swap_and_wrap.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
6
7\*******************************************************************/
8
15
16#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
17#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
18
19#include <util/message.h>
20#include <util/namespace.h>
21
23
24#include "dfcc_contract_mode.h"
25
26#include <map>
27#include <set>
28
32class dfcc_libraryt;
34class goto_modelt;
36class messaget;
37class symbolt;
38
40{
41public:
49
51 const loop_contract_configt &loop_contract_config,
52 const irep_idt &function_id,
53 const irep_idt &contract_id,
54 std::set<irep_idt> &function_pointer_contracts,
55 bool allow_recursive_calls)
56 {
59 loop_contract_config,
60 function_id,
62 function_pointer_contracts,
63 allow_recursive_calls);
64 }
65
67 const irep_idt &function_id,
68 const irep_idt &contract_id,
69 std::set<irep_idt> &function_pointer_contracts)
70 {
74 function_id,
76 function_pointer_contracts,
77 false);
78 }
79
81 void get_swapped_functions(std::set<irep_idt> &dest) const;
82
83protected:
92
94 static std::map<
96 std::pair<irep_idt, std::pair<dfcc_contract_modet, loop_contract_configt>>>
98
99 void swap_and_wrap(
100 const dfcc_contract_modet contract_mode,
101 const loop_contract_configt &loop_contract_config,
102 const irep_idt &function_id,
103 const irep_idt &contract_id,
104 std::set<irep_idt> &function_pointer_contracts,
105 bool allow_recursive_calls);
106
109 void check_contract(
110 const loop_contract_configt &loop_contract_config,
111 const irep_idt &function_id,
112 const irep_idt &contract_id,
113 std::set<irep_idt> &function_pointer_contracts,
114 bool allow_recursive_calls);
115
119 const irep_idt &function_id,
120 const irep_idt &contract_id,
121 std::set<irep_idt> &function_pointer_contracts);
122};
123#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:233
A contract is represented by a function declaration or definition with contract clauses attached to i...
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.
This class rewrites GOTO functions that use the built-ins:
void check_contract(const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
Swaps-and-wraps the given function_id in a wrapper function that checks the given contract_id.
message_handlert & message_handler
dfcc_spec_functionst & spec_functions
void swap_and_wrap_check(const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
dfcc_libraryt & library
void swap_and_wrap_replace(const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts)
void get_swapped_functions(std::set< irep_idt > &dest) const
Adds the set of swapped functions to dest.
static std::map< irep_idt, std::pair< irep_idt, std::pair< dfcc_contract_modet, loop_contract_configt > > > cache
remember all functions that were swapped/wrapped and in which mode
dfcc_instrumentt & instrument
dfcc_contract_handlert & contract_handler
void replace_with_contract(const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts)
Swaps-and-wraps the given function_id in a wrapper function that models the abstract behaviour of con...
void swap_and_wrap(const dfcc_contract_modet contract_mode, const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Symbol table entry.
Definition symbol.h:28
Enum type representing the contract checking and replacement modes.
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Config for loop contract.
Loop contract configurations.
dstringt irep_idt