CBMC
dfcc_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: Remi Delmas, delmarsd@amazon.com
6 Date: August 2022
7 
8 \*******************************************************************/
9 
10 #include "dfcc_utils.h"
11 
12 #include <util/arith_tools.h>
13 #include <util/c_types.h>
14 #include <util/format_expr.h>
15 #include <util/fresh_symbol.h>
16 #include <util/message.h>
17 #include <util/pointer_expr.h>
19 #include <util/std_expr.h>
20 #include <util/std_types.h>
21 
24 
29 
30 #include <set>
31 
33 static bool symbol_exists(
34  const goto_modelt &goto_model,
35  const irep_idt &name,
36  const bool require_has_code_type,
37  const bool require_body_available)
38 {
39  const namespacet ns{goto_model.symbol_table};
40 
41  const symbolt *sym;
42  if(ns.lookup(name, sym))
43  return false;
44 
45  if(require_has_code_type && sym->type.id() != ID_code)
46  return false;
47 
48  if(require_body_available)
49  {
50  const auto found = goto_model.goto_functions.function_map.find(name);
51 
52  return found != goto_model.goto_functions.function_map.end() &&
53  found->second.body_available();
54  }
55  return true;
56 }
57 
59  const goto_modelt &goto_model,
60  const irep_idt &function_id)
61 {
62  return symbol_exists(goto_model, function_id, true, false);
63 }
64 
66  const goto_modelt &goto_model,
67  const irep_idt &function_id)
68 {
69  return symbol_exists(goto_model, function_id, true, true);
70 }
71 
73  symbol_table_baset &symbol_table,
74  const irep_idt &function_id)
75 {
76  symbolt &function_symbol = symbol_table.get_writeable_ref(function_id);
77  CHECK_RETURN(function_symbol.type.id() == ID_code);
78  return function_symbol;
79 }
80 
82  symbol_table_baset &symbol_table,
83  const typet &type,
84  const irep_idt &function_id,
85  const std::string &base_name,
86  const source_locationt &source_location)
87 {
88  const symbolt &function_symbol =
89  get_function_symbol(symbol_table, function_id);
90 
91  symbolt &symbol = get_fresh_aux_symbol(
92  type,
93  id2string(function_id),
94  base_name,
95  source_location,
96  function_symbol.mode,
97  symbol_table);
98  symbol.module = function_symbol.module;
99 
100  return symbol.symbol_expr();
101 }
102 
104  symbol_table_baset &symbol_table,
105  const typet &type,
106  const std::string &prefix,
107  const std::string &base_name,
108  const source_locationt &source_location,
109  const irep_idt &mode,
110  const irep_idt &module,
111  const exprt &initial_value,
112  const bool no_nondet_initialization)
113 {
114  symbolt &symbol = get_fresh_aux_symbol(
115  type, prefix, base_name, source_location, mode, symbol_table);
116  symbol.module = module;
117  symbol.is_static_lifetime = true;
118  symbol.value = initial_value;
119  symbol.value.set(ID_C_no_nondet_initialization, no_nondet_initialization);
120  symbol.is_parameter = false;
121  return symbol;
122 }
123 
125  symbol_table_baset &symbol_table,
126  const irep_idt &function_id,
127  const std::string &base_name,
128  const typet &type)
129 {
130  const symbolt &function_symbol =
131  get_function_symbol(symbol_table, function_id);
132 
133  symbolt &symbol = get_fresh_aux_symbol(
134  type,
135  id2string(function_id),
136  base_name,
137  function_symbol.location,
138  function_symbol.mode,
139  symbol_table);
140  symbol.is_parameter = true;
141  symbol.module = function_symbol.module;
142  return symbol;
143 }
144 
146 static void add_parameter(const symbolt &symbol, code_typet &code_type)
147 {
148  PRECONDITION(symbol.is_parameter);
149  code_typet::parametert parameter(symbol.type);
150  parameter.set_base_name(symbol.base_name);
151  parameter.set_identifier(symbol.name);
152  auto &parameters = code_type.parameters();
153  parameters.insert(parameters.end(), parameter);
154 }
155 
157  goto_modelt &goto_model,
158  const symbolt &symbol,
159  const irep_idt &function_id)
160 {
161  auto &function_symbol =
162  get_function_symbol(goto_model.symbol_table, function_id);
163  code_typet &code_type = to_code_type(function_symbol.type);
164  ::add_parameter(symbol, code_type);
165  auto found = goto_model.goto_functions.function_map.find(function_id);
166  if(found != goto_model.goto_functions.function_map.end())
167  found->second.set_parameter_identifiers(code_type);
168 }
169 
171  goto_modelt &goto_model,
172  const irep_idt &function_id,
173  const std::string &base_name,
174  const typet &type)
175 {
176  const symbolt &symbol = create_new_parameter_symbol(
177  goto_model.symbol_table, function_id, base_name, type);
178  add_parameter(goto_model, symbol, function_id);
179  return symbol;
180 }
181 
184 static void clone_parameters(
185  symbol_table_baset &symbol_table,
186  const code_typet::parameterst &old_params,
187  const irep_idt &mode,
188  const irep_idt &module,
189  const source_locationt &location,
190  std::function<const irep_idt(const irep_idt &)> &trans_param,
191  const irep_idt &new_function_id,
192  code_typet::parameterst &new_params)
193 {
194  // rename function parameters in the wrapper function's code_type
195  std::size_t anon_counter = 0;
196 
197  // build parameters and symbols
198  for(auto &old_param : old_params)
199  {
200  // new identifier for new_code_type
201  const irep_idt &old_base_name = old_param.get_base_name().empty()
202  ? "#anon" + std::to_string(anon_counter++)
203  : old_param.get_base_name();
204  const irep_idt &new_base_name = trans_param(old_base_name);
205 
206  irep_idt new_param_id =
207  id2string(new_function_id) + "::" + id2string(new_base_name);
208 
209  // build parameter
210  code_typet::parametert new_param(old_param.type());
211  new_param.set_base_name(new_base_name);
212  new_param.set_identifier(new_param_id);
213  new_params.push_back(new_param);
214 
215  // build symbol
216  parameter_symbolt new_param_symbol;
217  new_param_symbol.base_name = new_base_name;
218  new_param_symbol.name = new_param_id;
219  new_param_symbol.pretty_name = new_param_id;
220  new_param_symbol.type = old_param.type();
221  new_param_symbol.mode = mode;
222  new_param_symbol.module = module;
223  new_param_symbol.location = location;
224  bool add_failed = symbol_table.add(new_param_symbol);
225  INVARIANT(
226  !add_failed,
227  "DFCC: renamed parameter " + id2string(new_base_name) +
228  " already exists");
229  }
230 }
231 
250  goto_modelt &goto_model,
251  const irep_idt &function_id,
252  std::function<const irep_idt(const irep_idt &)> &trans_fun,
253  std::function<const irep_idt(const irep_idt &)> &trans_param,
254  std::function<const typet(const typet &)> &trans_ret_type,
255  std::function<const source_locationt(const source_locationt &)> &trans_loc)
256 {
257  const symbolt &old_function_symbol =
258  dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
259  code_typet old_code_type = to_code_type(old_function_symbol.type);
260 
261  irep_idt new_function_id = trans_fun(function_id);
262 
263  code_typet::parameterst new_params;
264  source_locationt new_location = trans_loc(old_function_symbol.location);
266  goto_model.symbol_table,
267  old_code_type.parameters(),
268  old_function_symbol.mode,
269  old_function_symbol.mode,
270  new_location,
271  trans_param,
272  new_function_id,
273  new_params);
274 
275  code_typet new_code_type(
276  new_params, trans_ret_type(old_code_type.return_type()));
277 
278  // create new goto_function
279  goto_functiont new_goto_function;
280  new_goto_function.set_parameter_identifiers(new_code_type);
281  goto_model.goto_functions.function_map[new_function_id].copy_from(
282  new_goto_function);
283 
284  // build new function symbol
285  symbolt new_function_symbol{
286  new_function_id, std::move(new_code_type), old_function_symbol.mode};
287  new_function_symbol.base_name = new_function_id;
288  new_function_symbol.pretty_name = new_function_id;
289  new_function_symbol.module = old_function_symbol.module;
290  new_function_symbol.location = trans_loc(old_function_symbol.location);
291  new_function_symbol.set_compiled();
292 
293  INVARIANT(
294  !goto_model.symbol_table.add(new_function_symbol),
295  "DFCC: renamed function " + id2string(new_function_id) + " already exists");
296 
297  return goto_model.symbol_table.lookup_ref(new_function_id);
298 }
299 
301  goto_modelt &goto_model,
302  const irep_idt &function_id,
303  const irep_idt &new_function_id,
304  std::optional<typet> new_return_type = {})
305 {
306  std::function<const irep_idt(const irep_idt &)> trans_fun =
307  [&](const irep_idt &old_name) { return new_function_id; };
308 
309  std::function<const irep_idt(const irep_idt &)> trans_param =
310  [&](const irep_idt &old_name) { return old_name; };
311 
312  std::function<const typet(const typet &)> trans_ret_type =
313  [&](const typet &old_type) {
314  return new_return_type.has_value() ? new_return_type.value() : old_type;
315  };
316 
317  std::function<const source_locationt(const source_locationt &)> trans_loc =
318  [&](const source_locationt &old_location) { return old_location; };
319 
321  goto_model, function_id, trans_fun, trans_param, trans_ret_type, trans_loc);
322 }
323 
325  goto_modelt &goto_model,
326  const irep_idt &function_id,
327  const irep_idt &wrapped_function_id)
328 {
329  auto &goto_functions = goto_model.goto_functions;
330  auto &symbol_table = goto_model.symbol_table;
331 
332  auto old_function = goto_functions.function_map.find(function_id);
333  INVARIANT(
334  old_function != goto_functions.function_map.end(),
335  "DFCC: function to wrap " + id2string(function_id) +
336  " must exist in the program");
337 
338  // Register the wrapped function under the new name
339  std::swap(
340  goto_functions.function_map[wrapped_function_id], old_function->second);
341 
342  // Remove previous entry
343  goto_functions.function_map.erase(old_function);
344 
345  // Add new symbol for the wrapped function in the symbol table
346  const symbolt *old_sym = symbol_table.lookup(function_id);
347  source_locationt sl(old_sym->location);
348  sl.set_file("wrapped functions for code contracts");
349  sl.set_line("0");
350  symbolt wrapped_sym = *old_sym;
351  wrapped_sym.name = wrapped_function_id;
352  wrapped_sym.base_name = wrapped_function_id;
353  wrapped_sym.location = sl;
354  const auto wrapped_found = symbol_table.insert(std::move(wrapped_sym));
355  INVARIANT(
356  wrapped_found.second,
357  "DFCC: wrapped function symbol " + id2string(wrapped_function_id) +
358  " already exists in the symbol table");
359 
360  // Re-insert a symbol for `function_id` which is now the wrapper function
361  symbolt wrapper_sym = *old_sym;
362 
363  std::function<const irep_idt(const irep_idt &)> trans_param =
364  [&](const irep_idt &old_param) {
365  return id2string(old_param) + "_wrapper";
366  };
367 
368  // create new code_type with renamed parameters for the wrapper
369  const auto &old_code_type = to_code_type(old_sym->type);
370  code_typet::parameterst new_params;
372  symbol_table,
373  old_code_type.parameters(),
374  wrapper_sym.mode,
375  wrapper_sym.module,
376  wrapper_sym.location,
377  // the naming scheme is `function_id::param` + `param_suffix`
378  trans_param,
379  function_id,
380  new_params);
381 
382  code_typet new_code_type(new_params, old_code_type.return_type());
383 
384  wrapper_sym.type = new_code_type;
385 
386  // Remove original symbol from the symbol_table
387  bool remove_failed = goto_model.symbol_table.remove(function_id);
388  INVARIANT(
389  !remove_failed,
390  "DFCC: could not remove wrapped function '" + id2string(function_id) +
391  "' from the symbol table");
392 
393  // Insert update symbol in the symbol_table
394  const auto wrapper_sym_found = symbol_table.insert(std::move(wrapper_sym));
395  INVARIANT(
396  wrapper_sym_found.second,
397  "DFCC: could not insert wrapper symbol '" + id2string(function_id) +
398  "' in the symbol table");
399 
400  // Insert wrapper function in the function_map
401  goto_functiont &wrapper_fun = goto_functions.function_map[function_id];
402  wrapper_fun.set_parameter_identifiers(new_code_type);
403  wrapper_fun.body.add(goto_programt::make_end_function(sl));
404 }
405 
407 {
408  return equal_exprt(ptr, null_pointer_exprt(to_pointer_type(ptr.type())));
409 }
410 
412 {
413  const auto &size = size_of_expr(expr.type(), ns);
414 
415  if(!size.has_value())
416  {
418  "DFCC: no definite size for lvalue target" + format_to_string(expr),
419  expr.source_location());
420  }
421  return size.value();
422 }
423 
425  goto_modelt &goto_model,
426  const irep_idt &function_id,
427  message_handlert &message_handler)
428 {
429  auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
430 
432  goto_function.body_available(),
433  "dfcc_utilst::inline_function: '" + id2string(function_id) +
434  "' must have a body");
435 
436  const namespacet ns{goto_model.symbol_table};
437  inlining_decoratort decorated(message_handler);
438  goto_function_inline(goto_model.goto_functions, function_id, ns, decorated);
439 
440  return decorated;
441 }
442 
444  goto_modelt &goto_model,
445  const irep_idt &function_id,
446  message_handlert &message_handler)
447 {
448  inlining_decoratort decorated =
449  ::inline_function(goto_model, function_id, message_handler);
450 
451  messaget log{message_handler};
452  decorated.throw_on_recursive_calls(log, 0);
453  decorated.throw_on_no_body(log, 0);
454  decorated.throw_on_missing_function(log, 0);
455  decorated.throw_on_not_enough_arguments(log, 0);
456 
457  goto_model.goto_functions.update();
458 }
459 
461  goto_modelt &goto_model,
462  const irep_idt &function_id,
463  std::set<irep_idt> &no_body,
464  std::set<irep_idt> &recursive_call,
465  std::set<irep_idt> &missing_function,
466  std::set<irep_idt> &not_enough_arguments,
467  message_handlert &message_handler)
468 {
469  inlining_decoratort decorated =
470  ::inline_function(goto_model, function_id, message_handler);
471 
472  no_body.insert(
473  decorated.get_no_body_set().begin(), decorated.get_no_body_set().end());
474  recursive_call.insert(
475  decorated.get_recursive_call_set().begin(),
476  decorated.get_recursive_call_set().end());
477  missing_function.insert(
478  decorated.get_missing_function_set().begin(),
479  decorated.get_missing_function_set().end());
480  not_enough_arguments.insert(
481  decorated.get_not_enough_arguments_set().begin(),
482  decorated.get_not_enough_arguments_set().end());
483 
484  goto_model.goto_functions.update();
485 }
486 
488  goto_modelt &goto_model,
489  goto_programt &goto_program,
490  std::set<irep_idt> &no_body,
491  std::set<irep_idt> &recursive_call,
492  std::set<irep_idt> &missing_function,
493  std::set<irep_idt> &not_enough_arguments,
494  message_handlert &message_handler)
495 {
496  const namespacet ns{goto_model.symbol_table};
497  inlining_decoratort decorated(message_handler);
498  goto_program_inline(goto_model.goto_functions, goto_program, ns, decorated);
499  no_body.insert(
500  decorated.get_no_body_set().begin(), decorated.get_no_body_set().end());
501  recursive_call.insert(
502  decorated.get_recursive_call_set().begin(),
503  decorated.get_recursive_call_set().end());
504  missing_function.insert(
505  decorated.get_missing_function_set().begin(),
506  decorated.get_missing_function_set().end());
507  not_enough_arguments.insert(
508  decorated.get_not_enough_arguments_set().begin(),
509  decorated.get_not_enough_arguments_set().end());
510  goto_model.goto_functions.update();
511 }
void set_base_name(const irep_idt &name)
Definition: std_types.h:629
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:624
Base type of functions.
Definition: std_types.h:583
std::vector< parametert > parameterst
Definition: std_types.h:585
const typet & return_type() const
Definition: std_types.h:689
const parameterst & parameters() const
Definition: std_types.h:699
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
void set_parameter_identifiers(const code_typet &code_type)
Definition: goto_function.h:40
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
Decorator for a message_handlert used during function inlining that collect names of GOTO functions c...
const std::set< irep_idt > & get_no_body_set() const
void throw_on_recursive_calls(messaget &log, const int error_code)
Throws the given error code if recursive call warnings happend during inlining.
const std::set< irep_idt > & get_missing_function_set() const
void throw_on_missing_function(messaget &log, const int error_code)
Throws the given error code if missing function warnings happend during inlining.
void throw_on_no_body(messaget &log, const int error_code)
Throws the given error code if no body for function warnings happend during inlining.
const std::set< irep_idt > & get_not_enough_arguments_set() const
void throw_on_not_enough_arguments(messaget &log, const int error_code)
Throws the given error code if not enough arguments warnings happend during inlining.
const std::set< irep_idt > & get_recursive_call_set() const
Thrown when we can't handle something in an input source file.
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
const irep_idt & id() const
Definition: irep.h:388
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:94
The null pointer constant.
Definition: pointer_expr.h:909
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:179
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table base class interface.
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:70
bool is_parameter
Definition: symbol.h:76
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
static void clone_parameters(symbol_table_baset &symbol_table, const code_typet::parameterst &old_params, const irep_idt &mode, const irep_idt &module, const source_locationt &location, std::function< const irep_idt(const irep_idt &)> &trans_param, const irep_idt &new_function_id, code_typet::parameterst &new_params)
Clones the old_params into the new_params list, applying the trans_param function to generate the nam...
Definition: dfcc_utils.cpp:184
static const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, std::function< const irep_idt(const irep_idt &)> &trans_fun, std::function< const irep_idt(const irep_idt &)> &trans_param, std::function< const typet(const typet &)> &trans_ret_type, std::function< const source_locationt(const source_locationt &)> &trans_loc)
Creates a new symbol in the symbol_table by cloning the given function_id function and transforming t...
Definition: dfcc_utils.cpp:249
static inlining_decoratort inline_function(goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
Definition: dfcc_utils.cpp:424
static bool symbol_exists(const goto_modelt &goto_model, const irep_idt &name, const bool require_has_code_type, const bool require_body_available)
Returns true iff the given symbol exists and satisfies requirements.
Definition: dfcc_utils.cpp:33
static void add_parameter(const symbolt &symbol, code_typet &code_type)
Adds the given symbol as parameter to the given code_typet.
Definition: dfcc_utils.cpp:146
Dynamic frame condition checking utility functions.
std::string format_to_string(const T &o)
Definition: format.h:43
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Goto Programs with Functions.
void goto_program_inline(goto_functionst &goto_functions, goto_programt &goto_program, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls found in a particular program.
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
double log(double x)
Definition: math.c:2776
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
Definition: dfcc_utils.cpp:72
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.
Definition: dfcc_utils.cpp:443
static bool function_symbol_with_body_exists(const goto_modelt &, const irep_idt &function_id)
Definition: dfcc_utils.cpp:65
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
Definition: dfcc_utils.cpp:406
static bool function_symbol_exists(const goto_modelt &, const irep_idt &function_id)
Returns true iff the given symbol exists and satisfies requirements.
Definition: dfcc_utils.cpp:58
static exprt make_sizeof_expr(const exprt &expr, const namespacet &)
Returns the expression sizeof(expr).
Definition: dfcc_utils.cpp:411
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.
Definition: dfcc_utils.cpp:124
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
Definition: dfcc_utils.cpp:324
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 ...
Definition: dfcc_utils.cpp:103
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 ...
Definition: dfcc_utils.cpp:300
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.
Definition: dfcc_utils.cpp:156
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.
Definition: dfcc_utils.cpp:487
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...
Definition: dfcc_utils.cpp:81
dstringt irep_idt