CBMC
Loading...
Searching...
No Matches
dfcc_utils.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: August 2022
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_UTILS_H
14#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_UTILS_H
15
16#include <util/std_expr.h>
17
18#include <set>
19
20class goto_modelt;
21class goto_programt;
24class symbolt;
25
27{
29 static bool
30 function_symbol_exists(const goto_modelt &, const irep_idt &function_id);
32 const goto_modelt &,
33 const irep_idt &function_id);
34
36 static symbolt &
37 get_function_symbol(symbol_table_baset &, const irep_idt &function_id);
38
46 const typet &type,
47 const irep_idt &function_id,
48 const std::string &base_name,
49 const source_locationt &source_location);
50
62 static const symbolt &create_static_symbol(
64 const typet &type,
65 const std::string &prefix,
66 const std::string &base_name,
67 const source_locationt &source_location,
68 const irep_idt &mode,
69 const irep_idt &module,
70 const exprt &initial_value,
71 const bool no_nondet_initialization = true);
72
74#if defined(__GNUC__) && __GNUC__ >= 14
76#endif
77 static const symbolt &
80 const irep_idt &function_id,
81 const std::string &base_name,
82 const typet &type);
83
87 static void add_parameter(
89 const symbolt &symbol,
90 const irep_idt &function_id);
91
94 static const symbolt &add_parameter(
96 const irep_idt &function_id,
97 const std::string &base_name,
98 const typet &type);
99
106#if defined(__GNUC__) && __GNUC__ >= 14
108#endif
109 static const symbolt &
111 goto_modelt &goto_model,
112 const irep_idt &function_id,
114 std::optional<typet> new_return_type);
115
144 static void wrap_function(
145 goto_modelt &goto_model,
146 const irep_idt &function_id,
148
150 static const exprt make_null_check_expr(const exprt &ptr);
151
153 static exprt make_sizeof_expr(const exprt &expr, const namespacet &);
154
157 static void inline_function(
158 goto_modelt &goto_model,
159 const irep_idt &function_id,
160 message_handlert &message_handler);
161
164 static void inline_function(
165 goto_modelt &goto_model,
166 const irep_idt &function_id,
167 std::set<irep_idt> &no_body,
168 std::set<irep_idt> &recursive_call,
169 std::set<irep_idt> &missing_function,
170 std::set<irep_idt> &not_enough_arguments,
171 message_handlert &message_handler);
172
175 static void inline_program(
176 goto_modelt &goto_model,
177 goto_programt &goto_program,
178 std::set<irep_idt> &no_body,
179 std::set<irep_idt> &recursive_call,
180 std::set<irep_idt> &missing_function,
181 std::set<irep_idt> &not_enough_arguments,
182 message_handlert &message_handler);
183};
184
185#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait()
Definition ai.h:565
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
A generic container class for the GOTO intermediate representation of one function.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
API to expression classes.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static void inline_function(goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
Inlines the given function, aborts on recursive calls during inlining.
static bool function_symbol_with_body_exists(const goto_modelt &, const irep_idt &function_id)
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
static bool function_symbol_exists(const goto_modelt &, const irep_idt &function_id)
Returns true iff the given symbol exists and satisfies requirements.
static exprt make_sizeof_expr(const exprt &expr, const namespacet &)
Returns the expression sizeof(expr).
static const symbolt & create_new_parameter_symbol(symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
Creates a new parameter symbol for the given function_id.
static void wrap_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id)
Given a function to wrap foo and a new name wrapped_foo
static const symbolt & create_static_symbol(symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol ...
static const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, std::optional< typet > new_return_type)
Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given ...
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
static void inline_program(goto_modelt &goto_model, goto_programt &goto_program, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > &not_enough_arguments, message_handlert &message_handler)
Inlines the given program, and returns function symbols that caused warnings.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...