cprover
ansi_c_entry_point.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "ansi_c_entry_point.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/c_types.h>
13 #include <util/config.h>
14 #include <util/pointer_expr.h>
15 #include <util/string_constant.h>
16 
18 
20 
22 #include "expr2c.h"
23 
25  const code_typet::parameterst &parameters,
26  code_blockt &init_code,
27  symbol_tablet &symbol_table,
28  const c_object_factory_parameterst &object_factory_parameters)
29 {
30  exprt::operandst main_arguments;
31  main_arguments.resize(parameters.size());
32 
33  for(std::size_t param_number=0;
34  param_number<parameters.size();
35  param_number++)
36  {
37  const code_typet::parametert &p=parameters[param_number];
38  const irep_idt base_name=p.get_base_name().empty()?
39  ("argument#"+std::to_string(param_number)):p.get_base_name();
40 
41  main_arguments[param_number] = c_nondet_symbol_factory(
42  init_code,
43  symbol_table,
44  base_name,
45  p.type(),
46  p.source_location(),
47  object_factory_parameters,
48  lifetimet::AUTOMATIC_LOCAL);
49  }
50 
51  return main_arguments;
52 }
53 
55  const symbolt &function,
56  code_blockt &init_code,
57  symbol_tablet &symbol_table)
58 {
59  bool has_return_value =
60  to_code_type(function.type).return_type() != void_type();
61 
62  if(has_return_value)
63  {
64  const symbolt &return_symbol = symbol_table.lookup_ref("return'");
65 
66  // record return value
67  init_code.add(code_outputt{
68  return_symbol.base_name, return_symbol.symbol_expr(), function.location});
69  }
70 
71  #if 0
72  std::size_t i=0;
73 
74  for(const auto &p : parameters)
75  {
76  if(p.get_identifier().empty())
77  continue;
78 
79  irep_idt identifier=p.get_identifier();
80 
81  const symbolt &symbol=symbol_table.lookup(identifier);
82 
83  if(symbol.type.id()==ID_pointer)
84  {
85  codet output(ID_output);
86  output.operands().resize(2);
87 
88  output.op0()=
92  from_integer(0, index_type())));
93  output.op1()=symbol.symbol_expr();
94  output.add_source_location()=p.source_location();
95 
96  init_code.add(std::move(output));
97  }
98 
99  i++;
100  }
101  #endif
102 }
103 
105  symbol_tablet &symbol_table,
106  message_handlert &message_handler,
107  const c_object_factory_parameterst &object_factory_parameters)
108 {
109  // check if entry point is already there
110  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
111  symbol_table.symbols.end())
112  return false; // silently ignore
113 
114  irep_idt main_symbol;
115 
116  // find main symbol, if any is given
117  if(config.main.has_value())
118  {
119  std::list<irep_idt> matches;
120 
122  it, symbol_table.symbol_base_map, config.main.value())
123  {
124  // look it up
125  symbol_tablet::symbolst::const_iterator s_it=
126  symbol_table.symbols.find(it->second);
127 
128  if(s_it==symbol_table.symbols.end())
129  continue;
130 
131  if(s_it->second.type.id()==ID_code)
132  matches.push_back(it->second);
133  }
134 
135  if(matches.empty())
136  {
137  messaget message(message_handler);
138  message.error() << "main symbol '" << config.main.value() << "' not found"
139  << messaget::eom;
140  return true; // give up
141  }
142 
143  if(matches.size()>=2)
144  {
145  messaget message(message_handler);
146  message.error() << "main symbol '" << config.main.value()
147  << "' is ambiguous" << messaget::eom;
148  return true;
149  }
150 
151  main_symbol=matches.front();
152  }
153  else
154  main_symbol=ID_main;
155 
156  // look it up
157  symbol_tablet::symbolst::const_iterator s_it=
158  symbol_table.symbols.find(main_symbol);
159 
160  if(s_it==symbol_table.symbols.end())
161  return false; // give up silently
162 
163  const symbolt &symbol=s_it->second;
164 
165  // check if it has a body
166  if(symbol.value.is_nil())
167  {
168  messaget message(message_handler);
169  message.error() << "main symbol '" << id2string(main_symbol)
170  << "' has no body" << messaget::eom;
171  return false; // give up
172  }
173 
174  static_lifetime_init(symbol_table, symbol.location);
175 
177  symbol, symbol_table, message_handler, object_factory_parameters);
178 }
179 
190  const symbolt &symbol,
191  symbol_tablet &symbol_table,
192  message_handlert &message_handler,
193  const c_object_factory_parameterst &object_factory_parameters)
194 {
195  PRECONDITION(!symbol.value.is_nil());
196  code_blockt init_code;
197 
198  // add 'HIDE' label
199  init_code.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
200 
201  // build call to initialization function
202 
203  {
204  symbol_tablet::symbolst::const_iterator init_it=
205  symbol_table.symbols.find(INITIALIZE_FUNCTION);
206 
207  if(init_it==symbol_table.symbols.end())
208  {
209  messaget message(message_handler);
210  message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
211  << messaget::eom;
212  return true;
213  }
214 
215  code_function_callt call_init(init_it->second.symbol_expr());
216  call_init.add_source_location()=symbol.location;
217 
218  init_code.add(std::move(call_init));
219  }
220 
221  // build call to main function
222 
223  code_function_callt call_main(symbol.symbol_expr());
224  call_main.add_source_location()=symbol.location;
225  call_main.function().add_source_location()=symbol.location;
226 
227  if(to_code_type(symbol.type).return_type() != void_type())
228  {
229  auxiliary_symbolt return_symbol;
230  return_symbol.mode=ID_C;
231  return_symbol.is_static_lifetime=false;
232  return_symbol.name="return'";
233  return_symbol.base_name = "return'";
234  return_symbol.type=to_code_type(symbol.type).return_type();
235 
236  symbol_table.add(return_symbol);
237  call_main.lhs()=return_symbol.symbol_expr();
238  }
239 
240  const code_typet::parameterst &parameters=
241  to_code_type(symbol.type).parameters();
242 
243  if(symbol.name==ID_main)
244  {
245  if(parameters.empty())
246  {
247  // ok
248  }
249  else if(parameters.size()==2 || parameters.size()==3)
250  {
251  namespacet ns(symbol_table);
252 
253  {
254  symbolt argc_symbol;
255 
256  argc_symbol.base_name = "argc'";
257  argc_symbol.name = "argc'";
258  argc_symbol.type = signed_int_type();
259  argc_symbol.is_static_lifetime = true;
260  argc_symbol.is_lvalue = true;
261  argc_symbol.mode = ID_C;
262 
263  auto r = symbol_table.insert(argc_symbol);
264  if(!r.second && r.first != argc_symbol)
265  {
266  messaget message(message_handler);
267  message.error() << "argc already exists but is not usable"
268  << messaget::eom;
269  return true;
270  }
271  }
272 
273  const symbolt &argc_symbol = ns.lookup("argc'");
274 
275  {
276  // we make the type of this thing an array of pointers
277  // need to add one to the size -- the array is terminated
278  // with NULL
279  const exprt one_expr = from_integer(1, argc_symbol.type);
280  const plus_exprt size_expr(argc_symbol.symbol_expr(), one_expr);
281  const array_typet argv_type(pointer_type(char_type()), size_expr);
282 
283  symbolt argv_symbol;
284 
285  argv_symbol.base_name = "argv'";
286  argv_symbol.name = "argv'";
287  argv_symbol.type = argv_type;
288  argv_symbol.is_static_lifetime = true;
289  argv_symbol.is_lvalue = true;
290  argv_symbol.mode = ID_C;
291 
292  auto r = symbol_table.insert(argv_symbol);
293  if(!r.second && r.first != argv_symbol)
294  {
295  messaget message(message_handler);
296  message.error() << "argv already exists but is not usable"
297  << messaget::eom;
298  return true;
299  }
300  }
301 
302  const symbolt &argv_symbol=ns.lookup("argv'");
303 
304  {
305  // assume argc is at least one
306  exprt one=from_integer(1, argc_symbol.type);
307 
309  argc_symbol.symbol_expr(), ID_ge, std::move(one));
310 
311  init_code.add(code_assumet(std::move(ge)));
312  }
313 
314  {
315  // assume argc is at most MAX/8-1
316  mp_integer upper_bound=
318 
319  exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
320 
322  argc_symbol.symbol_expr(), ID_le, std::move(bound_expr));
323 
324  init_code.add(code_assumet(std::move(le)));
325  }
326 
327  // record argc as an input
328  init_code.add(code_inputt{"argc", argc_symbol.symbol_expr()});
329 
330  if(parameters.size()==3)
331  {
332  {
333  symbolt envp_size_symbol;
334  envp_size_symbol.base_name = "envp_size'";
335  envp_size_symbol.name = "envp_size'";
336  envp_size_symbol.type = size_type();
337  envp_size_symbol.is_static_lifetime = true;
338  envp_size_symbol.mode = ID_C;
339 
340  if(!symbol_table.insert(std::move(envp_size_symbol)).second)
341  {
342  messaget message(message_handler);
343  message.error()
344  << "failed to insert envp_size symbol" << messaget::eom;
345  return true;
346  }
347  }
348 
349  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
350 
351  {
352  symbolt envp_symbol;
353  envp_symbol.base_name = "envp'";
354  envp_symbol.name = "envp'";
355  envp_symbol.type = array_typet(
356  pointer_type(char_type()), envp_size_symbol.symbol_expr());
357  envp_symbol.is_static_lifetime = true;
358  envp_symbol.mode = ID_C;
359 
360  if(!symbol_table.insert(std::move(envp_symbol)).second)
361  {
362  messaget message(message_handler);
363  message.error() << "failed to insert envp symbol" << messaget::eom;
364  return true;
365  }
366  }
367 
368  // assume envp_size is INTMAX-1
369  const mp_integer max =
370  to_integer_bitvector_type(envp_size_symbol.type).largest();
371 
372  exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
373 
375  envp_size_symbol.symbol_expr(), ID_le, std::move(max_minus_one));
376 
377  init_code.add(code_assumet(le));
378  }
379 
380  {
381  /* zero_string doesn't work yet */
382 
383  /*
384  exprt zero_string(ID_zero_string, array_typet());
385  zero_string.type().subtype()=char_type();
386  zero_string.type().set(ID_size, "infinity");
387  const index_exprt index(zero_string, from_integer(0, uint_type()));
388  exprt address_of =
389  typecast_exprt::conditional_cast(
390  address_of_exprt(index, pointer_type(char_type())),
391  argv_symbol.type.subtype());
392 
393  // assign argv[*] to the address of a string-object
394  array_of_exprt array_of(address_of, argv_symbol.type);
395 
396  init_code.copy_to_operands(
397  code_assignt(argv_symbol.symbol_expr(), array_of));
398  */
399  }
400 
401  {
402  // assign argv[argc] to NULL
403  const null_pointer_exprt null(
404  to_pointer_type(argv_symbol.type.subtype()));
405 
406  index_exprt index_expr(
407  argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
408 
409  // disable bounds check on that one
410  index_expr.set("bounds_check", false);
411 
412  init_code.add(code_assignt(index_expr, null));
413  }
414 
415  if(parameters.size()==3)
416  {
417  const symbolt &envp_symbol=ns.lookup("envp'");
418  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
419 
420  // assume envp[envp_size] is NULL
421  null_pointer_exprt null(to_pointer_type(envp_symbol.type.subtype()));
422 
423  index_exprt index_expr(
424  envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());
425  // disable bounds check on that one
426  index_expr.set("bounds_check", false);
427 
428  equal_exprt is_null(std::move(index_expr), std::move(null));
429 
430  init_code.add(code_assumet(is_null));
431  }
432 
433  {
434  exprt::operandst &operands=call_main.arguments();
435 
436  if(parameters.size()==3)
437  operands.resize(3);
438  else
439  operands.resize(2);
440 
441  exprt &op0=operands[0];
442  exprt &op1=operands[1];
443 
445  argc_symbol.symbol_expr(), parameters[0].type());
446 
447  {
448  index_exprt index_expr(
449  argv_symbol.symbol_expr(), from_integer(0, index_type()));
450 
451  // disable bounds check on that one
452  index_expr.set("bounds_check", false);
453 
454  const pointer_typet &pointer_type =
455  to_pointer_type(parameters[1].type());
456 
458  address_of_exprt(index_expr), pointer_type);
459  }
460 
461  // do we need envp?
462  if(parameters.size()==3)
463  {
464  const symbolt &envp_symbol=ns.lookup("envp'");
465 
466  index_exprt index_expr(
467  envp_symbol.symbol_expr(), from_integer(0, index_type()));
468 
469  const pointer_typet &pointer_type =
470  to_pointer_type(parameters[2].type());
471 
472  operands[2] = typecast_exprt::conditional_cast(
473  address_of_exprt(index_expr), pointer_type);
474  }
475  }
476  }
477  else
478  {
479  const namespacet ns{symbol_table};
480  const std::string main_signature = type2c(symbol.type, ns);
482  "'main' with signature '" + main_signature +
483  "' found,"
484  " but expecting one of:\n"
485  " int main(void)\n"
486  " int main(int argc, char *argv[])\n"
487  " int main(int argc, char *argv[], char *envp[])\n"
488  "If this is a non-standard main entry point please provide a custom\n"
489  "entry function and point to it via cbmc --function instead"};
490  }
491  }
492  else
493  {
494  // produce nondet arguments
496  parameters, init_code, symbol_table, object_factory_parameters);
497  }
498 
499  init_code.add(std::move(call_main));
500 
501  // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
502 
503  record_function_outputs(symbol, init_code, symbol_table);
504 
505  // add the entry point symbol
506  symbolt new_symbol;
507 
508  new_symbol.name=goto_functionst::entry_point();
509  new_symbol.type = code_typet({}, void_type());
510  new_symbol.value.swap(init_code);
511  new_symbol.mode=symbol.mode;
512 
513  if(!symbol_table.insert(std::move(new_symbol)).second)
514  {
515  messaget message(message_handler);
516  message.error() << "failed to insert main symbol" << messaget::eom;
517  return true;
518  }
519 
520  return false;
521 }
c_nondet_symbol_factory.h
C Nondet Symbol Factory.
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
symbol_table_baset::symbol_base_map
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
Definition: symbol_table_base.h:33
codet::op0
exprt & op0()
Definition: expr.h:103
ansi_c_entry_point.h
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:746
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
configt::main
optionalt< std::string > main
Definition: config.h:261
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:831
string_constant.h
c_nondet_symbol_factory
symbol_exprt c_nondet_symbol_factory(code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &loc, const c_object_factory_parameterst &object_factory_parameters, const lifetimet lifetime)
Creates a symbol and generates code so that it can vary over all possible values for its type.
Definition: c_nondet_symbol_factory.cpp:200
exprt
Base class for all expressions.
Definition: expr.h:54
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
build_function_environment
exprt::operandst build_function_environment(const code_typet::parameterst &parameters, code_blockt &init_code, symbol_tablet &symbol_table, const c_object_factory_parameterst &object_factory_parameters)
Definition: ansi_c_entry_point.cpp:24
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
configt::ansi_c
struct configt::ansi_ct ansi_c
string_constantt
Definition: string_constant.h:16
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1140
void_type
empty_typet void_type()
Definition: c_types.cpp:253
record_function_outputs
void record_function_outputs(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table)
Definition: ansi_c_entry_point.cpp:54
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
code_outputt
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:724
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
message
static const char * message(const statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:27
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
code_typet::parametert::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:800
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:15
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:2751
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
expr2c.h
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1407
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_integer_bitvector_type
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
Definition: std_types.h:1206
irept::swap
void swap(irept &irep)
Definition: irep.h:452
code_typet
Base type of functions.
Definition: std_types.h:744
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
generate_ansi_c_start_function
bool generate_ansi_c_start_function(const symbolt &symbol, symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Generate a _start function for a specific function.
Definition: ansi_c_entry_point.cpp:189
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
ansi_c_entry_point
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Definition: ansi_c_entry_point.cpp:104
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
config
configt config
Definition: config.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
array_typet
Arrays with given size.
Definition: std_types.h:968
code_skipt
A codet representing a skip statement.
Definition: std_code.h:270
is_null
static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
Expression which is true when the string is equal to the literal "null".
Definition: string_format_builtin_function.cpp:95
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
code_inputt
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:677
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
static_lifetime_init
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
Definition: static_lifetime_init.cpp:25
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
forall_symbol_base_map
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
code_typet::parametert
Definition: std_types.h:761
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_functions.h
Goto Programs with Functions.
config.h
integer_bitvector_typet::largest
mp_integer largest() const
Return the largest value that can be represented using this type.
Definition: std_types.cpp:185
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
exprt::operands
operandst & operands()
Definition: expr.h:96
r
static int8_t r
Definition: irep_hash.h:59
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
type2c
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3937
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
codet::op1
exprt & op1()
Definition: expr.h:106
index_exprt
Array index operator.
Definition: std_expr.h:1243
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:111
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35