cprover
c_typecheck_code.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_typecheck_base.h"
13 
14 #include <util/c_types.h>
15 #include <util/config.h>
16 #include <util/range.h>
17 #include <util/string_constant.h>
18 
19 #include "ansi_c_declaration.h"
20 
22 {
24 }
25 
27 {
28  if(code.id()!=ID_code)
29  {
31  error() << "expected code, got " << code.pretty() << eom;
32  throw 0;
33  }
34 
35  code.type() = empty_typet();
36 
37  const irep_idt &statement=code.get_statement();
38 
39  if(statement==ID_expression)
41  else if(statement==ID_label)
43  else if(statement==ID_switch_case)
45  else if(statement==ID_gcc_switch_case_range)
47  else if(statement==ID_block)
49  else if(statement==ID_decl_block)
50  {
51  }
52  else if(statement==ID_ifthenelse)
54  else if(statement==ID_while)
56  else if(statement==ID_dowhile)
58  else if(statement==ID_for)
59  typecheck_for(code);
60  else if(statement==ID_switch)
61  typecheck_switch(code);
62  else if(statement==ID_break)
63  typecheck_break(code);
64  else if(statement==ID_goto)
66  else if(statement==ID_gcc_computed_goto)
68  else if(statement==ID_continue)
69  typecheck_continue(code);
70  else if(statement==ID_return)
72  else if(statement==ID_decl)
73  typecheck_decl(code);
74  else if(statement==ID_assign)
75  typecheck_assign(code);
76  else if(statement==ID_skip)
77  {
78  }
79  else if(statement==ID_asm)
81  else if(statement==ID_start_thread)
83  else if(statement==ID_gcc_local_label)
85  else if(statement==ID_msc_try_finally)
86  {
87  assert(code.operands().size()==2);
88  typecheck_code(to_code(code.op0()));
89  typecheck_code(to_code(code.op1()));
90  }
91  else if(statement==ID_msc_try_except)
92  {
93  assert(code.operands().size()==3);
94  typecheck_code(to_code(code.op0()));
95  typecheck_expr(code.op1());
96  typecheck_code(to_code(code.op2()));
97  }
98  else if(statement==ID_msc_leave)
99  {
100  // fine as is, but should check that we
101  // are in a 'try' block
102  }
103  else if(statement==ID_static_assert)
104  {
105  PRECONDITION(code.operands().size() == 2);
106 
107  typecheck_expr(code.op0());
108  typecheck_expr(code.op1());
109 
110  implicit_typecast_bool(code.op0());
111  make_constant(code.op0());
112 
113  if(code.op0().is_false())
114  {
115  // failed
117  error() << "static assertion failed";
118  if(code.op1().id() == ID_string_constant)
119  error() << ": " << to_string_constant(code.op1()).get_value();
120  error() << eom;
121  throw 0;
122  }
123  }
124  else if(statement==ID_CPROVER_try_catch ||
125  statement==ID_CPROVER_try_finally)
126  {
127  assert(code.operands().size()==2);
128  typecheck_code(to_code(code.op0()));
129  typecheck_code(to_code(code.op1()));
130  }
131  else if(statement==ID_CPROVER_throw)
132  {
133  assert(code.operands().empty());
134  }
135  else if(statement==ID_assume ||
136  statement==ID_assert)
137  {
138  // These are not generated by the C/C++ parsers,
139  // but we allow them for the benefit of other users
140  // of the typechecker.
141  assert(code.operands().size()==1);
142  typecheck_expr(code.op0());
143  }
144  else
145  {
147  error() << "unexpected statement: " << statement << eom;
148  throw 0;
149  }
150 }
151 
153 {
154  const irep_idt flavor = code.get_flavor();
155 
156  if(flavor==ID_gcc)
157  {
158  // These have 5 operands.
159  // The first operand is a string.
160  // Operands 1, 2, 3, 4 are lists of expressions.
161 
162  // Operand 1: OutputOperands
163  // Operand 2: InputOperands
164  // Operand 3: Clobbers
165  // Operand 4: GotoLabels
166 
167  auto &code_asm_gcc = to_code_asm_gcc(code);
168 
169  typecheck_expr(code_asm_gcc.asm_text());
170 
171  // the operands are lists of expressions
172  for(auto &op : ranget<exprt::operandst::iterator>(
173  code_asm_gcc.operands().begin() + 1, code_asm_gcc.operands().end()))
174  {
175  for(auto &expr : op.operands())
176  typecheck_expr(expr);
177  }
178  }
179  else if(flavor==ID_msc)
180  {
181  assert(code.operands().size()==1);
182  typecheck_expr(code.op0());
183  }
184 }
185 
187 {
188  if(code.operands().size()!=2)
189  {
191  error() << "assignment statement expected to have two operands"
192  << eom;
193  throw 0;
194  }
195 
196  typecheck_expr(code.op0());
197  typecheck_expr(code.op1());
198 
199  implicit_typecast(code.op1(), code.op0().type());
200 }
201 
203 {
204  for(auto &c : code.statements())
205  typecheck_code(c);
206 
207  // do decl-blocks
208 
209  code_blockt new_ops;
210  new_ops.statements().reserve(code.statements().size());
211 
212  for(auto &code_op : code.statements())
213  {
214  if(code_op.is_not_nil())
215  new_ops.add(std::move(code_op));
216  }
217 
218  code.statements().swap(new_ops.statements());
219 }
220 
222 {
223  if(!break_is_allowed)
224  {
226  error() << "break not allowed here" << eom;
227  throw 0;
228  }
229 }
230 
232 {
234  {
236  error() << "continue not allowed here" << eom;
237  throw 0;
238  }
239 }
240 
242 {
243  // this comes with 1 operand, which is a declaration
244  if(code.operands().size()!=1)
245  {
247  error() << "decl expected to have 1 operand" << eom;
248  throw 0;
249  }
250 
251  // op0 must be declaration
252  if(code.op0().id()!=ID_declaration)
253  {
255  error() << "decl statement expected to have declaration as operand"
256  << eom;
257  throw 0;
258  }
259 
260  ansi_c_declarationt declaration;
261  declaration.swap(code.op0());
262 
263  if(declaration.get_is_static_assert())
264  {
265  codet new_code(ID_static_assert);
266  new_code.add_source_location()=code.source_location();
267  new_code.operands().swap(declaration.operands());
268  code.swap(new_code);
269  typecheck_code(code);
270  return; // done
271  }
272 
273  typecheck_declaration(declaration);
274 
275  std::list<codet> new_code;
276 
277  // iterate over declarators
278 
279  for(const auto &d : declaration.declarators())
280  {
281  irep_idt identifier = d.get_name();
282 
283  // look it up
284  symbol_tablet::symbolst::const_iterator s_it=
285  symbol_table.symbols.find(identifier);
286 
287  if(s_it==symbol_table.symbols.end())
288  {
290  error() << "failed to find decl symbol '" << identifier
291  << "' in symbol table" << eom;
292  throw 0;
293  }
294 
295  const symbolt &symbol=s_it->second;
296 
297  // This must not be an incomplete type, unless it's 'extern'
298  // or a typedef.
299  if(!symbol.is_type &&
300  !symbol.is_extern &&
301  !is_complete_type(symbol.type))
302  {
303  error().source_location=symbol.location;
304  error() << "incomplete type not permitted here" << eom;
305  throw 0;
306  }
307 
308  // see if it's a typedef
309  // or a function
310  // or static
311  if(symbol.is_type ||
312  symbol.type.id()==ID_code ||
313  symbol.is_static_lifetime)
314  {
315  // we ignore
316  }
317  else
318  {
319  code_declt decl(symbol.symbol_expr());
320  decl.add_source_location() = symbol.location;
321  decl.symbol().add_source_location() = symbol.location;
322 
323  // add initializer, if any
324  if(symbol.value.is_not_nil())
325  {
326  decl.operands().resize(2);
327  decl.op1() = symbol.value;
328  }
329 
330  new_code.push_back(decl);
331  }
332  }
333 
334  // stash away any side-effects in the declaration
335  new_code.splice(new_code.begin(), clean_code);
336 
337  if(new_code.empty())
338  {
339  source_locationt source_location=code.source_location();
340  code=code_skipt();
341  code.add_source_location()=source_location;
342  }
343  else if(new_code.size()==1)
344  {
345  code.swap(new_code.front());
346  }
347  else
348  {
349  // build a decl-block
350  auto code_block=code_blockt::from_list(new_code);
351  code_block.set_statement(ID_decl_block);
352  code.swap(code_block);
353  }
354 }
355 
357 {
358  if(type.id() == ID_array)
359  {
360  if(to_array_type(type).size().is_nil())
361  return false;
362  return is_complete_type(type.subtype());
363  }
364  else if(type.id()==ID_struct || type.id()==ID_union)
365  {
366  const auto &struct_union_type = to_struct_union_type(type);
367 
368  if(struct_union_type.is_incomplete())
369  return false;
370 
371  for(const auto &c : struct_union_type.components())
372  if(!is_complete_type(c.type()))
373  return false;
374  }
375  else if(type.id()==ID_vector)
376  return is_complete_type(type.subtype());
377  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
378  {
379  return is_complete_type(follow(type));
380  }
381 
382  return true;
383 }
384 
386 {
387  if(code.operands().size()!=1)
388  {
390  error() << "expression statement expected to have one operand"
391  << eom;
392  throw 0;
393  }
394 
395  exprt &op=code.op0();
396  typecheck_expr(op);
397 }
398 
400 {
401  if(code.operands().size()!=4)
402  {
404  error() << "for expected to have four operands" << eom;
405  throw 0;
406  }
407 
408  // the "for" statement has an implicit block around it,
409  // since code.op0() may contain declarations
410  //
411  // we therefore transform
412  //
413  // for(a;b;c) d;
414  //
415  // to
416  //
417  // { a; for(;b;c) d; }
418  //
419  // if config.ansi_c.for_has_scope
420 
422  code.op0().is_nil())
423  {
424  if(code.op0().is_not_nil())
425  typecheck_code(to_code(code.op0()));
426 
427  if(code.op1().is_nil())
428  code.op1()=true_exprt();
429  else
430  {
431  typecheck_expr(code.op1());
432  implicit_typecast_bool(code.op1());
433  }
434 
435  if(code.op2().is_not_nil())
436  typecheck_expr(code.op2());
437 
438  if(code.op3().is_not_nil())
439  {
440  // save & set flags
441  bool old_break_is_allowed=break_is_allowed;
442  bool old_continue_is_allowed=continue_is_allowed;
443 
445 
446  // recursive call
447  if(to_code(code.op3()).get_statement()==ID_decl_block)
448  {
449  code_blockt code_block;
450  code_block.add_source_location()=code.op3().source_location();
451 
452  code_block.add(std::move(to_code(code.op3())));
453  code.op3().swap(code_block);
454  }
455  typecheck_code(to_code(code.op3()));
456 
457  // restore flags
458  break_is_allowed=old_break_is_allowed;
459  continue_is_allowed=old_continue_is_allowed;
460  }
461  }
462  else
463  {
464  code_blockt code_block;
465  code_block.add_source_location()=code.source_location();
466  if(to_code(code.op3()).get_statement()==ID_block)
467  {
468  code_block.set(
469  ID_C_end_location,
471  }
472  else
473  {
474  code_block.set(
475  ID_C_end_location,
476  code.op3().source_location());
477  }
478 
479  code_block.reserve_operands(2);
480  code_block.add(std::move(to_code(code.op0())));
481  code.op0().make_nil();
482  code_block.add(std::move(code));
483  code.swap(code_block);
484  typecheck_code(code); // recursive call
485  }
486 
489 }
490 
492 {
493  // record the label
495 
496  typecheck_code(code.code());
497 }
498 
500 {
501  if(code.operands().size()!=2)
502  {
504  error() << "switch_case expected to have two operands" << eom;
505  throw 0;
506  }
507 
508  typecheck_code(code.code());
509 
510  if(code.is_default())
511  {
512  if(!case_is_allowed)
513  {
515  error() << "did not expect default label here" << eom;
516  throw 0;
517  }
518  }
519  else
520  {
521  if(!case_is_allowed)
522  {
524  error() << "did not expect `case' here" << eom;
525  throw 0;
526  }
527 
528  exprt &case_expr=code.case_op();
529  typecheck_expr(case_expr);
530  implicit_typecast(case_expr, switch_op_type);
531  make_constant(case_expr);
532  }
533 }
534 
537 {
538  if(!case_is_allowed)
539  {
541  error() << "did not expect `case' here" << eom;
542  throw 0;
543  }
544 
545  typecheck_expr(code.lower());
546  typecheck_expr(code.upper());
549  make_constant(code.lower());
550  make_constant(code.upper());
551  typecheck_code(code.code());
552 }
553 
555 {
556  // these are just declarations, e.g.,
557  // __label__ here, there;
558 }
559 
561 {
562  // we record the label used
564 }
565 
567 {
568  if(code.operands().size()!=1)
569  {
571  error() << "computed-goto expected to have one operand" << eom;
572  throw 0;
573  }
574 
575  exprt &dest=code.op0();
576 
577  if(dest.id()!=ID_dereference)
578  {
580  error() << "computed-goto expected to have dereferencing operand"
581  << eom;
582  throw 0;
583  }
584 
585  typecheck_expr(to_unary_expr(dest).op());
586  dest.type() = void_type();
587 }
588 
590 {
591  if(code.operands().size()!=3)
592  {
594  error() << "ifthenelse expected to have three operands" << eom;
595  throw 0;
596  }
597 
598  exprt &cond=code.cond();
599 
600  typecheck_expr(cond);
601 
602  #if 0
603  if(cond.id()==ID_sideeffect &&
604  cond.get(ID_statement)==ID_assign)
605  {
606  warning("warning: assignment in if condition");
607  }
608  #endif
609 
611 
612  if(code.then_case().get_statement() == ID_decl_block)
613  {
614  code_blockt code_block({code.then_case()});
615  code_block.add_source_location()=code.then_case().source_location();
616  code.then_case() = code_block;
617  }
618 
619  typecheck_code(code.then_case());
620 
621  if(!code.else_case().is_nil())
622  {
623  if(code.else_case().get_statement() == ID_decl_block)
624  {
625  code_blockt code_block({code.else_case()});
626  code_block.add_source_location()=code.else_case().source_location();
627  code.else_case() = code_block;
628  }
629 
630  typecheck_code(code.else_case());
631  }
632 }
633 
635 {
636  if(code.operands().size()!=1)
637  {
639  error() << "start_thread expected to have one operand" << eom;
640  throw 0;
641  }
642 
643  typecheck_code(to_code(code.op0()));
644 }
645 
647 {
648  if(code.has_return_value())
649  {
651 
652  if(return_type.id() == ID_empty)
653  {
654  // gcc doesn't actually complain, it just warns!
655  if(code.return_value().type().id() != ID_empty)
656  {
658 
659  warning() << "function has return void ";
660  warning() << "but a return statement returning ";
661  warning() << to_string(code.return_value().type());
662  warning() << eom;
663 
665  }
666  }
667  else
669  }
670  else if(
671  return_type.id() != ID_empty && return_type.id() != ID_constructor &&
672  return_type.id() != ID_destructor)
673  {
674  // gcc doesn't actually complain, it just warns!
676  warning() << "non-void function should return a value" << eom;
677 
678  code.return_value() =
680  }
681 }
682 
684 {
685  // we expect a code_switcht, but might return either a code_switcht or a
686  // code_blockt, hence don't use code_switcht in the interface
687  code_switcht &code_switch = to_code_switch(code);
688 
689  typecheck_expr(code_switch.value());
690 
691  // this needs to be promoted
692  implicit_typecast_arithmetic(code_switch.value());
693 
694  // save & set flags
695 
696  bool old_case_is_allowed(case_is_allowed);
697  bool old_break_is_allowed(break_is_allowed);
698  typet old_switch_op_type(switch_op_type);
699 
700  switch_op_type = code_switch.value().type();
702 
703  typecheck_code(code_switch.body());
704 
705  if(code_switch.body().get_statement() == ID_block)
706  {
707  // Collect all declarations before the first case, if there is any case
708  // (including a default one).
709  code_blockt wrapping_block;
710 
711  code_blockt &body_block = to_code_block(code_switch.body());
712  for(auto &statement : body_block.statements())
713  {
714  if(statement.get_statement() == ID_switch_case)
715  break;
716  else if(statement.get_statement() == ID_decl)
717  {
718  if(statement.operands().size() == 1)
719  {
720  wrapping_block.add(code_skipt());
721  wrapping_block.statements().back().swap(statement);
722  }
723  else
724  {
725  PRECONDITION(statement.operands().size() == 2);
726  wrapping_block.add(statement);
727  wrapping_block.statements().back().operands().pop_back();
728  statement.set_statement(ID_assign);
729  }
730  }
731  }
732 
733  if(!wrapping_block.statements().empty())
734  {
735  wrapping_block.add(std::move(code));
736  code.swap(wrapping_block);
737  }
738  }
739 
740  // restore flags
741  case_is_allowed=old_case_is_allowed;
742  break_is_allowed=old_break_is_allowed;
743  switch_op_type=old_switch_op_type;
744 }
745 
747 {
748  if(code.operands().size()!=2)
749  {
751  error() << "while expected to have two operands" << eom;
752  throw 0;
753  }
754 
755  typecheck_expr(code.cond());
757 
758  // save & set flags
759  bool old_break_is_allowed(break_is_allowed);
760  bool old_continue_is_allowed(continue_is_allowed);
761 
763 
764  if(code.body().get_statement()==ID_decl_block)
765  {
766  code_blockt code_block({code.body()});
767  code_block.add_source_location()=code.body().source_location();
768  code.body() = code_block;
769  }
770  typecheck_code(code.body());
771 
772  // restore flags
773  break_is_allowed=old_break_is_allowed;
774  continue_is_allowed=old_continue_is_allowed;
775 
778 }
779 
781 {
782  if(code.operands().size()!=2)
783  {
785  error() << "do while expected to have two operands" << eom;
786  throw 0;
787  }
788 
789  typecheck_expr(code.cond());
791 
792  // save & set flags
793  bool old_break_is_allowed(break_is_allowed);
794  bool old_continue_is_allowed(continue_is_allowed);
795 
797 
798  if(code.body().get_statement()==ID_decl_block)
799  {
800  code_blockt code_block({code.body()});
801  code_block.add_source_location()=code.body().source_location();
802  code.body() = code_block;
803  }
804  typecheck_code(code.body());
805 
806  // restore flags
807  break_is_allowed=old_break_is_allowed;
808  continue_is_allowed=old_continue_is_allowed;
809 
812 }
813 
815 {
816  if(code.find(ID_C_spec_loop_invariant).is_not_nil())
817  {
818  for(auto &invariant :
819  (static_cast<exprt &>(code.add(ID_C_spec_loop_invariant)).operands()))
820  {
821  typecheck_expr(invariant);
822  implicit_typecast_bool(invariant);
824  invariant,
825  ID_old,
826  CPROVER_PREFIX "old is not allowed in loop invariants.");
827  }
828  }
829 }
830 
832 {
833  if(code.find(ID_C_spec_decreases).is_not_nil())
834  {
835  for(auto &decreases_clause_component :
836  (static_cast<exprt &>(code.add(ID_C_spec_decreases)).operands()))
837  {
838  typecheck_expr(decreases_clause_component);
839  implicit_typecast_arithmetic(decreases_clause_component);
840  }
841  }
842 }
ANSI-CC Language Type Checking.
ANSI-C Language Type Checking.
empty_typet void_type()
Definition: c_types.cpp:253
const declaratorst & declarators() const
bool get_is_static_assert() const
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_break(codet &code)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr(exprt &expr)
virtual void typecheck_return(code_returnt &code)
virtual void typecheck_block(code_blockt &code)
virtual void typecheck_code(codet &code)
virtual void typecheck_while(code_whilet &code)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
virtual void typecheck_decl(codet &code)
virtual void typecheck_spec_decreases(codet &code)
virtual void make_constant(exprt &expr)
virtual void typecheck_assign(codet &expr)
virtual void typecheck_continue(codet &code)
symbol_tablet & symbol_table
virtual void implicit_typecast_arithmetic(exprt &expr)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_gcc_local_label(codet &code)
virtual void start_typecheck_code()
virtual void typecheck_asm(code_asmt &code)
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_for(codet &code)
virtual void typecheck_switch(codet &code)
virtual void typecheck_expression(codet &code)
virtual bool is_complete_type(const typet &type) const
virtual void typecheck_start_thread(codet &code)
virtual void typecheck_switch_case(code_switch_caset &code)
virtual void typecheck_spec_loop_invariant(codet &code)
virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &)
virtual void implicit_typecast_bool(exprt &expr)
virtual void typecheck_dowhile(code_dowhilet &code)
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_label(code_labelt &code)
std::map< irep_idt, source_locationt > labels_defined
codet representation of an inline assembler statement.
Definition: std_code.h:1699
const irep_idt & get_flavor() const
Definition: std_code.h:1709
A codet representing sequential composition of program statements.
Definition: std_code.h:168
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:186
source_locationt end_location() const
Definition: std_code.h:225
void add(const codet &code)
Definition: std_code.h:206
code_operandst & statements()
Definition: std_code.h:176
A codet representing the declaration of a local variable.
Definition: std_code.h:400
symbol_exprt & symbol()
Definition: std_code.h:406
codet representation of a do while statement.
Definition: std_code.h:988
const exprt & cond() const
Definition: std_code.h:995
const codet & body() const
Definition: std_code.h:1005
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1543
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1577
const exprt & lower() const
lower bound of range
Definition: std_code.h:1553
const exprt & upper() const
upper bound of range
Definition: std_code.h:1565
codet representation of a goto statement.
Definition: std_code.h:1157
const irep_idt & get_destination() const
Definition: std_code.h:1169
codet representation of an if-then-else statement.
Definition: std_code.h:776
const codet & then_case() const
Definition: std_code.h:804
const exprt & cond() const
Definition: std_code.h:794
const codet & else_case() const
Definition: std_code.h:814
codet representation of a label for branch targets.
Definition: std_code.h:1405
const irep_idt & get_label() const
Definition: std_code.h:1413
codet & code()
Definition: std_code.h:1423
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
const exprt & return_value() const
Definition: std_code.h:1350
bool has_return_value() const
Definition: std_code.h:1360
A codet representing a skip statement.
Definition: std_code.h:268
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
codet & code()
Definition: std_code.h:1496
const exprt & case_op() const
Definition: std_code.h:1486
bool is_default() const
Definition: std_code.h:1476
codet representing a switch statement.
Definition: std_code.h:864
const exprt & value() const
Definition: std_code.h:871
const codet & body() const
Definition: std_code.h:881
codet representing a while statement.
Definition: std_code.h:926
const exprt & cond() const
Definition: std_code.h:933
const codet & body() const
Definition: std_code.h:943
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op3()
Definition: expr.h:108
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code.h:69
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
void reserve_operands(operandst::size_type n)
Definition: expr.h:124
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
irept & add(const irep_namet &name)
Definition: irep.cpp:116
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
void swap(irept &irep)
Definition: irep.h:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
bool is_nil() const
Definition: irep.h:387
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
const irep_idt & get_value() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
bool is_extern
Definition: symbol.h:66
bool is_static_lifetime
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
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
exprt value
Initial value of symbol.
Definition: symbol.h:34
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:846
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1389
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1191
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:970
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1523
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1450
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:1032
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:908
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:254
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition: std_code.h:1607
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition: std_code.h:1819
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1728
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const string_constantt & to_string_constant(const exprt &expr)
bool for_has_scope
Definition: config.h:124
A range is a pair of a begin and an end iterators.
Definition: range.h:396