cprover
c_typecheck_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-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 <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/std_types.h>
20 #include <util/prefix.h>
21 #include <util/cprover_prefix.h>
22 #include <util/simplify_expr.h>
23 #include <util/base_type.h>
24 #include <util/std_expr.h>
27 
28 #include "c_typecast.h"
29 #include "c_sizeof.h"
30 #include "c_qualifiers.h"
31 #include "string_constant.h"
32 #include "anonymous_member.h"
33 #include "padding.h"
34 
36 {
37  if(expr.id()==ID_already_typechecked)
38  {
39  assert(expr.operands().size()==1);
40  exprt tmp;
41  tmp.swap(expr.op0());
42  expr.swap(tmp);
43  return;
44  }
45 
46  // fist do sub-nodes
48 
49  // now do case-split
50  typecheck_expr_main(expr);
51 }
52 
54 {
55  for(auto &op : expr.operands())
57 
58  if(expr.id()==ID_div ||
59  expr.id()==ID_mult ||
60  expr.id()==ID_plus ||
61  expr.id()==ID_minus)
62  {
63  if(expr.type().id()==ID_floatbv &&
64  expr.operands().size()==2)
65  {
66  // The rounding mode to be used at compile time is non-obvious.
67  // We'll simply use round to even (0), which is suggested
68  // by Sec. F.7.2 Translation, ISO-9899:1999.
69  expr.operands().resize(3);
70 
71  if(expr.id()==ID_div)
72  expr.id(ID_floatbv_div);
73  else if(expr.id()==ID_mult)
74  expr.id(ID_floatbv_mult);
75  else if(expr.id()==ID_plus)
76  expr.id(ID_floatbv_plus);
77  else if(expr.id()==ID_minus)
78  expr.id(ID_floatbv_minus);
79  else
80  assert(false);
81 
82  expr.op2()=from_integer(0, unsigned_int_type());
83  }
84  }
85 }
86 
88  const typet &type1,
89  const typet &type2)
90 {
91  // read
92  // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
93 
94  if(type1.id()==ID_symbol)
95  return gcc_types_compatible_p(follow(type1), type2);
96  else if(type2.id()==ID_symbol)
97  return gcc_types_compatible_p(type1, follow(type2));
98 
99  // check qualifiers first
100  if(c_qualifierst(type1)!=c_qualifierst(type2))
101  return false;
102 
103  if(type1.id()==ID_c_enum_tag)
105  else if(type2.id()==ID_c_enum_tag)
107 
108  if(type1.id()==ID_c_enum)
109  {
110  if(type2.id()==ID_c_enum) // both are enums
111  return type1==type2; // compares the tag
112  else if(type2==type1.subtype())
113  return true;
114  }
115  else if(type2.id()==ID_c_enum)
116  {
117  if(type1==type2.subtype())
118  return true;
119  }
120  else if(type1.id()==ID_pointer &&
121  type2.id()==ID_pointer)
122  {
123  return gcc_types_compatible_p(type1.subtype(), type2.subtype());
124  }
125  else if(type1.id()==ID_array &&
126  type2.id()==ID_array)
127  {
128  return
129  gcc_types_compatible_p(type1.subtype(), type2.subtype()); // ignore size
130  }
131  else if(type1.id()==ID_code &&
132  type2.id()==ID_code)
133  {
134  const code_typet &c_type1=to_code_type(type1);
135  const code_typet &c_type2=to_code_type(type2);
136 
138  c_type1.return_type(),
139  c_type2.return_type()))
140  return false;
141 
142  if(c_type1.parameters().size()!=c_type2.parameters().size())
143  return false;
144 
145  for(std::size_t i=0; i<c_type1.parameters().size(); i++)
147  c_type1.parameters()[i].type(),
148  c_type2.parameters()[i].type()))
149  return false;
150 
151  return true;
152  }
153  else
154  {
155  if(type1==type2)
156  {
157  // Need to distinguish e.g. long int from int or
158  // long long int from long int.
159  // The rules appear to match those of C++.
160 
161  if(type1.get(ID_C_c_type)==type2.get(ID_C_c_type))
162  return true;
163  }
164  }
165 
166  return false;
167 }
168 
170 {
171  if(expr.id()==ID_side_effect)
173  else if(expr.id()==ID_constant)
175  else if(expr.id()==ID_infinity)
176  {
177  // ignore
178  }
179  else if(expr.id()==ID_symbol)
180  typecheck_expr_symbol(expr);
181  else if(expr.id()==ID_unary_plus ||
182  expr.id()==ID_unary_minus ||
183  expr.id()==ID_bitnot)
185  else if(expr.id()==ID_not)
187  else if(expr.id()==ID_and || expr.id()==ID_or || expr.id()==ID_implies)
189  else if(expr.id()==ID_address_of)
191  else if(expr.id()==ID_dereference)
193  else if(expr.id()==ID_member)
194  typecheck_expr_member(expr);
195  else if(expr.id()==ID_ptrmember)
197  else if(expr.id()==ID_equal ||
198  expr.id()==ID_notequal ||
199  expr.id()==ID_lt ||
200  expr.id()==ID_le ||
201  expr.id()==ID_gt ||
202  expr.id()==ID_ge)
204  else if(expr.id()==ID_index)
205  typecheck_expr_index(expr);
206  else if(expr.id()==ID_typecast)
208  else if(expr.id()==ID_sizeof)
209  typecheck_expr_sizeof(expr);
210  else if(expr.id()==ID_alignof)
212  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
213  expr.id()==ID_mult || expr.id()==ID_div ||
214  expr.id()==ID_mod ||
215  expr.id()==ID_bitand || expr.id()==ID_bitxor || expr.id()==ID_bitor)
217  else if(expr.id()==ID_shl || expr.id()==ID_shr)
219  else if(expr.id()==ID_comma)
220  typecheck_expr_comma(expr);
221  else if(expr.id()==ID_if)
223  else if(expr.id()==ID_code)
224  {
225  err_location(expr);
226  error() << "typecheck_expr_main got code: " << expr.pretty() << eom;
227  throw 0;
228  }
229  else if(expr.id()==ID_gcc_builtin_va_arg)
231  else if(expr.id()==ID_cw_va_arg_typeof)
233  else if(expr.id()==ID_gcc_builtin_types_compatible_p)
234  {
235  expr.type()=bool_typet();
236  typet::subtypest &subtypes=((typet &)(expr.add(ID_type_arg))).subtypes();
237  assert(subtypes.size()==2);
238  typecheck_type(subtypes[0]);
239  typecheck_type(subtypes[1]);
240  source_locationt source_location=expr.source_location();
241 
242  // ignores top-level qualifiers
243  subtypes[0].remove(ID_C_constant);
244  subtypes[0].remove(ID_C_volatile);
245  subtypes[0].remove(ID_C_restricted);
246  subtypes[1].remove(ID_C_constant);
247  subtypes[1].remove(ID_C_volatile);
248  subtypes[1].remove(ID_C_restricted);
249 
250  expr.make_bool(gcc_types_compatible_p(subtypes[0], subtypes[1]));
251  expr.add_source_location()=source_location;
252  }
253  else if(expr.id()==ID_clang_builtin_convertvector)
254  {
255  typecheck_type(expr.type());
256  }
257  else if(expr.id()==ID_builtin_offsetof)
259  else if(expr.id()==ID_string_constant)
260  {
261  // already fine -- mark as lvalue
262  expr.set(ID_C_lvalue, true);
263  }
264  else if(expr.id()==ID_arguments)
265  {
266  // already fine
267  }
268  else if(expr.id()==ID_designated_initializer)
269  {
270  exprt &designator=static_cast<exprt &>(expr.add(ID_designator));
271 
272  Forall_operands(it, designator)
273  {
274  if(it->id()==ID_index)
275  {
276  assert(it->operands().size()==1);
277  typecheck_expr(it->op0()); // still needs typechecking
278  }
279  }
280  }
281  else if(expr.id()==ID_initializer_list)
282  {
283  // already fine, just set some type
284  expr.type()=void_type();
285  }
286  else if(expr.id()==ID_forall ||
287  expr.id()==ID_exists)
288  {
289  // op0 is a declaration,
290  // op1 the bound expression
291  assert(expr.operands().size()==2);
292  expr.type()=bool_typet();
293 
294  if(expr.op0().get(ID_statement)!=ID_decl)
295  {
296  err_location(expr);
297  error() << "expected declaration as operand of quantifier" << eom;
298  throw 0;
299  }
300 
301  // replace declaration by symbol expression
302  symbol_exprt bound=to_symbol_expr(expr.op0().op0());
303  expr.op0().swap(bound);
304  }
305  else if(expr.id()==ID_label)
306  {
307  expr.type()=void_type();
308  }
309  else if(expr.id()==ID_array)
310  {
311  // these pop up as string constants, and are already typed
312  }
313  else if(expr.id()==ID_complex)
314  {
315  // these should only exist as constants,
316  // and should already be typed
317  }
318  else if(expr.id()==ID_complex_real ||
319  expr.id()==ID_complex_imag)
320  {
321  // get the subtype
322  assert(expr.operands().size()==1);
323  const typet &op_type=follow(expr.op0().type());
324  if(op_type.id()!=ID_complex)
325  {
326  if(!is_number(op_type))
327  {
328  err_location(expr.op0());
329  error() << "real/imag expect numerical operand, "
330  << "but got `" << to_string(op_type) << "'" << eom;
331  throw 0;
332  }
333 
334  // we could compile away, I suppose
335  expr.type()=op_type;
336  expr.op0().make_typecast(complex_typet(op_type));
337  }
338  else
339  {
340  expr.type()=op_type.subtype();
341 
342  // these are lvalues if the operand is one
343  if(expr.op0().get_bool(ID_C_lvalue))
344  expr.set(ID_C_lvalue, true);
345 
346  if(expr.op0().get_bool(ID_C_constant))
347  expr.set(ID_C_constant, true);
348  }
349  }
350  else if(expr.id()==ID_generic_selection)
351  {
352  // This is C11.
353  // The operand is already typechecked. Depending
354  // on its type, we return one of the generic associations.
355 
356  if(expr.operands().size()!=1)
357  {
358  err_location(expr);
359  error() << "_Generic expects one operand" << eom;
360  throw 0;
361  }
362 
363  // This is one of the few places where it's detectable
364  // that we are using "bool" for boolean operators instead
365  // of "int". We convert for this reason.
366  if(follow(expr.op0().type()).id()==ID_bool)
368 
369  irept::subt &generic_associations=
370  expr.add(ID_generic_associations).get_sub();
371 
372  // first typecheck all types
373  Forall_irep(it, generic_associations)
374  if(it->get(ID_type_arg)!=ID_default)
375  {
376  typet &type=static_cast<typet &>(it->add(ID_type_arg));
377  typecheck_type(type);
378  }
379 
380  // first try non-default match
381  exprt default_match=nil_exprt();
382  exprt assoc_match=nil_exprt();
383 
384  const typet &op_type=follow(expr.op0().type());
385 
386  forall_irep(it, generic_associations)
387  {
388  if(it->get(ID_type_arg)==ID_default)
389  default_match=static_cast<const exprt &>(it->find(ID_value));
390  else if(op_type==
391  follow(static_cast<const typet &>(it->find(ID_type_arg))))
392  assoc_match=static_cast<const exprt &>(it->find(ID_value));
393  }
394 
395  if(assoc_match.is_nil())
396  {
397  if(default_match.is_not_nil())
398  expr.swap(default_match);
399  else
400  {
401  err_location(expr);
402  error() << "unmatched generic selection: "
403  << to_string(expr.op0().type()) << eom;
404  throw 0;
405  }
406  }
407  else
408  expr.swap(assoc_match);
409 
410  // still need to typecheck the result
411  typecheck_expr(expr);
412  }
413  else if(expr.id()==ID_gcc_asm_input ||
414  expr.id()==ID_gcc_asm_output ||
415  expr.id()==ID_gcc_asm_clobbered_register)
416  {
417  }
418  else if(expr.id()==ID_lshr || expr.id()==ID_ashr ||
419  expr.id()==ID_assign_lshr || expr.id()==ID_assign_ashr)
420  {
421  // already type checked
422  }
423  else
424  {
425  err_location(expr);
426  error() << "unexpected expression: " << expr.pretty() << eom;
427  throw 0;
428  }
429 }
430 
432 {
433  if(expr.operands().size()!=2)
434  {
435  err_location(expr);
436  error() << "comma operator expects two operands" << eom;
437  throw 0;
438  }
439 
440  expr.type()=expr.op1().type();
441 
442  // make this an l-value if the last operand is one
443  if(expr.op1().get_bool(ID_C_lvalue))
444  expr.set(ID_C_lvalue, true);
445 }
446 
448 {
449  // The first parameter is the va_list, and the second
450  // is the type, which will need to be fixed and checked.
451  // The type is given by the parser as type of the expression.
452 
453  typet arg_type=expr.type();
454  typecheck_type(arg_type);
455 
456  code_typet new_type;
457  new_type.return_type().swap(arg_type);
458  new_type.parameters().resize(1);
459  new_type.parameters()[0].type()=pointer_type(void_type());
460 
461  assert(expr.operands().size()==1);
462  exprt arg=expr.op0();
463 
465 
466  // turn into function call
468  result.add_source_location()=expr.source_location();
469  result.function()=symbol_exprt(ID_gcc_builtin_va_arg);
470  result.function().add_source_location()=expr.source_location();
471  result.function().type()=new_type;
472  result.arguments().push_back(arg);
473  result.type()=new_type.return_type();
474 
475  expr.swap(result);
476 
477  // Make sure symbol exists, but we have it return void
478  // to avoid collisions of the same symbol with different
479  // types.
480 
481  code_typet symbol_type=new_type;
482  symbol_type.return_type()=void_type();
483 
484  symbolt symbol;
485  symbol.base_name=ID_gcc_builtin_va_arg;
486  symbol.name=ID_gcc_builtin_va_arg;
487  symbol.type=symbol_type;
488 
489  symbol_table.move(symbol);
490 }
491 
493 {
494  // used in Code Warrior via
495  //
496  // __va_arg( <Symbol>, _var_arg_typeof( <Typ> ) )
497  //
498  // where __va_arg is declared as
499  //
500  // extern void* __va_arg(void*, int);
501 
502  typet &type=static_cast<typet &>(expr.add(ID_type_arg));
503  typecheck_type(type);
504 
505  // these return an integer
506  expr.type()=signed_int_type();
507 }
508 
510 {
511  // these need not be constant, due to array indices!
512 
513  if(!expr.operands().empty())
514  {
515  err_location(expr);
516  error() << "builtin_offsetof expects no operands" << eom;
517  throw 0;
518  }
519 
520  typet &type=static_cast<typet &>(expr.add(ID_type_arg));
521  typecheck_type(type);
522 
523  exprt &member=static_cast<exprt &>(expr.add(ID_designator));
524 
526 
527  forall_operands(m_it, member)
528  {
529  if(type.id()==ID_symbol)
530  type=follow(type);
531 
532  if(m_it->id()==ID_member)
533  {
534  if(type.id()!=ID_union && type.id()!=ID_struct)
535  {
536  err_location(expr);
537  error() << "offsetof of member expects struct/union type, "
538  << "but got `" << to_string(type) << "'" << eom;
539  throw 0;
540  }
541 
542  bool found=false;
543  irep_idt component_name=m_it->get(ID_component_name);
544 
545  while(!found)
546  {
547  assert(type.id()==ID_union || type.id()==ID_struct);
548 
549  const struct_union_typet &struct_union_type=
550  to_struct_union_type(type);
551 
552  // direct member?
553  if(struct_union_type.has_component(component_name))
554  {
555  found=true;
556 
557  if(type.id()==ID_struct)
558  {
559  exprt o=c_offsetof(to_struct_type(type), component_name, *this);
560 
561  if(o.is_nil())
562  {
563  err_location(expr);
564  error() << "offsetof failed to determine offset of `"
565  << component_name << "'" << eom;
566  throw 0;
567  }
568 
569  if(o.type()!=size_type())
571 
573  }
574 
575  type=struct_union_type.get_component(component_name).type();
576  }
577  else
578  {
579  // maybe anonymous?
580 
581  const struct_union_typet::componentst &components=
582  struct_union_type.components();
583 
584  bool found2=false;
585 
586  for(struct_union_typet::componentst::const_iterator
587  c_it=components.begin();
588  c_it!=components.end();
589  c_it++)
590  {
591  if(c_it->get_anonymous() &&
592  (follow(c_it->type()).id()==ID_struct ||
593  follow(c_it->type()).id()==ID_union))
594  {
595  if(has_component_rec(c_it->type(), component_name, *this))
596  {
597  if(type.id()==ID_struct)
598  {
599  exprt o=
600  c_offsetof(to_struct_type(type), c_it->get_name(), *this);
601 
602  if(o.is_nil())
603  {
604  err_location(expr);
605  error() << "offsetof failed to determine offset of `"
606  << component_name << "'" << eom;
607  throw 0;
608  }
609 
610  if(o.type()!=size_type())
612 
614  }
615 
616  typet tmp=follow(c_it->type());
617  type=tmp;
618  assert(type.id()==ID_union || type.id()==ID_struct);
619  found2=true;
620  break; // we run into another iteration of the outer loop
621  }
622  }
623  }
624 
625  if(!found2)
626  {
627  err_location(expr);
628  error() << "offset-of of member failed to find component `"
629  << component_name << "' in `"
630  << to_string(type) << "'" << eom;
631  throw 0;
632  }
633  }
634  }
635  }
636  else if(m_it->id()==ID_index)
637  {
638  assert(m_it->operands().size()==1);
639 
640  if(type.id()!=ID_array)
641  {
642  err_location(expr);
643  error() << "offsetof of index expects array type" << eom;
644  throw 0;
645  }
646 
647  exprt index=m_it->op0();
648 
649  // still need to typecheck index
650  typecheck_expr(index);
651 
652  exprt sub_size=c_sizeof(type.subtype(), *this);
653  if(index.type()!=size_type())
654  index.make_typecast(size_type());
655  result=plus_exprt(result, mult_exprt(sub_size, index));
656 
657  typet tmp=type.subtype();
658  type=tmp;
659  }
660  }
661 
662  // We make an effort to produce a constant,
663  // but this may depend on variables
664  simplify(result, *this);
665  result.add_source_location()=expr.source_location();
666 
667  expr.swap(result);
668 }
669 
671 {
672  if(expr.id()==ID_side_effect &&
673  expr.get(ID_statement)==ID_function_call)
674  {
675  // don't do function operand
676  assert(expr.operands().size()==2);
677 
678  typecheck_expr(expr.op1()); // arguments
679  }
680  else if(expr.id()==ID_side_effect &&
681  expr.get(ID_statement)==ID_statement_expression)
682  {
683  typecheck_code(to_code(expr.op0()));
684  }
685  else if(expr.id()==ID_forall || expr.id()==ID_exists)
686  {
687  assert(expr.operands().size()==2);
688 
689  ansi_c_declarationt &declaration=
690  to_ansi_c_declaration(expr.op0());
691 
692  typecheck_declaration(declaration);
693 
694  if(declaration.declarators().size()!=1)
695  {
696  err_location(expr);
697  error() << "expected one declarator exactly" << eom;
698  throw 0;
699  }
700 
701  irep_idt identifier=
702  declaration.declarators().front().get_name();
703 
704  // look it up
705  symbol_tablet::symbolst::iterator s_it=
706  symbol_table.symbols.find(identifier);
707 
708  if(s_it==symbol_table.symbols.end())
709  {
710  err_location(expr);
711  error() << "failed to find decl symbol `" << identifier
712  << "' in symbol table" << eom;
713  throw 0;
714  }
715 
716  symbolt &symbol=s_it->second;
717 
718  if(symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
719  !is_complete_type(symbol.type) || symbol.type.id()==ID_code)
720  {
721  err_location(expr);
722  error() << "unexpected quantified symbol" << eom;
723  throw 0;
724  }
725 
726  code_declt decl;
727  decl.add_source_location()=declaration.source_location();
728  decl.symbol()=symbol.symbol_expr();
729 
730  expr.op0()=decl;
731 
732  typecheck_expr(expr.op1());
733  }
734  else
735  {
736  Forall_operands(it, expr)
737  typecheck_expr(*it);
738  }
739 }
740 
742 {
743  irep_idt identifier=to_symbol_expr(expr).get_identifier();
744 
745  // Is it a parameter? We do this while checking parameter lists.
746  id_type_mapt::const_iterator p_it=parameter_map.find(identifier);
747  if(p_it!=parameter_map.end())
748  {
749  // yes
750  expr.type()=p_it->second;
751  expr.set(ID_C_lvalue, true);
752  return;
753  }
754 
755  // renaming via GCC asm label
756  asm_label_mapt::const_iterator entry=
757  asm_label_map.find(identifier);
758  if(entry!=asm_label_map.end())
759  {
760  identifier=entry->second;
761  to_symbol_expr(expr).set_identifier(identifier);
762  }
763 
764  // look it up
765  const symbolt *symbol_ptr;
766  if(lookup(identifier, symbol_ptr))
767  {
768  err_location(expr);
769  error() << "failed to find symbol `"
770  << identifier << "'" << eom;
771  throw 0;
772  }
773 
774  const symbolt &symbol=*symbol_ptr;
775 
776  if(symbol.is_type)
777  {
778  err_location(expr);
779  error() << "did not expect a type symbol here, but got `"
780  << symbol.display_name() << "'" << eom;
781  throw 0;
782  }
783 
784  // save the source location
785  source_locationt source_location=expr.source_location();
786 
787  if(symbol.is_macro)
788  {
789  // preserve enum key
790  #if 0
791  irep_idt base_name=expr.get(ID_C_base_name);
792  #endif
793 
794  follow_macros(expr);
795 
796  #if 0
797  if(expr.id()==ID_constant &&
798  !base_name.empty())
799  expr.set(ID_C_cformat, base_name);
800  else
801  #endif
802  typecheck_expr(expr);
803 
804  // preserve location
805  expr.add_source_location()=source_location;
806  }
807  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "constant_infinity"))
808  {
809  expr=infinity_exprt(symbol.type);
810 
811  // put it back
812  expr.add_source_location()=source_location;
813  }
814  else if(identifier=="__func__" ||
815  identifier=="__FUNCTION__" ||
816  identifier=="__PRETTY_FUNCTION__")
817  {
818  // __func__ is an ANSI-C standard compliant hack to get the function name
819  // __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
820  string_constantt s(source_location.get_function());
821  s.add_source_location()=source_location;
822  s.set(ID_C_lvalue, true);
823  expr.swap(s);
824  }
825  else
826  {
827  expr=symbol.symbol_expr();
828 
829  // put it back
830  expr.add_source_location()=source_location;
831 
832  if(symbol.is_lvalue)
833  expr.set(ID_C_lvalue, true);
834 
835  if(expr.type().id()==ID_code) // function designator
836  { // special case: this is sugar for &f
837  address_of_exprt tmp(expr, pointer_type(expr.type()));
838  tmp.set("#implicit", true);
840  expr=tmp;
841  }
842  }
843 }
844 
846  side_effect_exprt &expr)
847 {
848  if(expr.operands().size()!=1)
849  {
850  err_location(expr);
851  error() << "statement expression expects one operand" << eom;
852  throw 0;
853  }
854 
855  codet &code=to_code(expr.op0());
856 
857  // the type is the type of the last statement in the
858  // block, but do worry about labels!
859 
861 
862  irep_idt last_statement=last.get_statement();
863 
864  if(last_statement==ID_expression)
865  {
866  assert(last.operands().size()==1);
867  exprt &op=last.op0();
868 
869  // arrays here turn into pointers (array decay)
870  if(op.type().id()==ID_array)
871  implicit_typecast(op, pointer_type(op.type().subtype()));
872 
873  expr.type()=op.type();
874  }
875  else if(last_statement==ID_function_call)
876  {
877  // this is suspected to be dead
878  assert(false);
879 
880  // make the last statement an expression
881 
883 
885 
886  sideeffect.function()=fc.function();
887  sideeffect.arguments()=fc.arguments();
888  sideeffect.add_source_location()=fc.source_location();
889 
890  sideeffect.type()=
891  static_cast<const typet &>(fc.function().type().find(ID_return_type));
892 
893  expr.type()=sideeffect.type();
894 
895  if(fc.lhs().is_nil())
896  {
897  codet code_expr(ID_expression);
898  code_expr.add_source_location() = fc.source_location();
899  code_expr.move_to_operands(sideeffect);
900  last.swap(code_expr);
901  }
902  else
903  {
904  codet code_expr(ID_expression);
905  code_expr.add_source_location() = fc.source_location();
906 
907  exprt assign(ID_side_effect);
908  assign.set(ID_statement, ID_assign);
909  assign.add_source_location()=fc.source_location();
910  assign.move_to_operands(fc.lhs(), sideeffect);
911  assign.type()=assign.op1().type();
912 
913  code_expr.move_to_operands(assign);
914  last.swap(code_expr);
915  }
916  }
917  else
918  expr.type()=typet(ID_empty);
919 }
920 
922 {
923  typet type;
924 
925  if(expr.operands().empty())
926  {
927  type.swap(static_cast<typet &>(expr.add(ID_type_arg)));
928  typecheck_type(type);
929  }
930  else if(expr.operands().size()==1)
931  {
932  type.swap(expr.op0().type());
933  }
934  else
935  {
936  err_location(expr);
937  error() << "sizeof operator expects zero or one operand, "
938  "but got " << expr.operands().size() << eom;
939  throw 0;
940  }
941 
942  if(type.id()==ID_c_bit_field)
943  {
944  err_location(expr);
945  error() << "sizeof cannot be applied to bit fields" << eom;
946  throw 0;
947  }
948 
949  exprt new_expr=c_sizeof(type, *this);
950 
951  if(new_expr.is_nil())
952  {
953  err_location(expr);
954  error() << "type has no size: " << to_string(type) << eom;
955  throw 0;
956  }
957 
958  new_expr.swap(expr);
959 
960  expr.add(ID_C_c_sizeof_type)=type;
961 
962  // The type may contain side-effects.
963  if(!clean_code.empty())
964  {
965  side_effect_exprt side_effect_expr(ID_statement_expression, void_type());
966  code_blockt decl_block(clean_code);
967  decl_block.set_statement(ID_decl_block);
968  side_effect_expr.copy_to_operands(decl_block);
969  clean_code.clear();
970 
971  // We merge the side-effect into the operand of the typecast,
972  // using a comma-expression.
973  // I.e., (type)e becomes (type)(side-effect, e)
974  // It is not obvious whether the type or 'e' should be evaluated
975  // first.
976 
977  exprt comma_expr(ID_comma, expr.type());
978  comma_expr.copy_to_operands(side_effect_expr, expr);
979  expr.swap(comma_expr);
980  }
981 }
982 
984 {
985  typet argument_type;
986 
987  if(expr.operands().size()==1)
988  argument_type=expr.op0().type();
989  else
990  {
991  typet &op_type=static_cast<typet &>(expr.add(ID_type_arg));
992  typecheck_type(op_type);
993  argument_type=op_type;
994  }
995 
996  // we only care about the type
997  mp_integer a=alignment(argument_type, *this);
998 
999  exprt tmp=from_integer(a, size_type());
1000  tmp.add_source_location()=expr.source_location();
1001 
1002  expr.swap(tmp);
1003 }
1004 
1006 {
1007  if(expr.operands().size()!=1)
1008  {
1009  err_location(expr);
1010  error() << "typecast operator expects one operand" << eom;
1011  throw 0;
1012  }
1013 
1014  exprt &op=expr.op0();
1015 
1016  typecheck_type(expr.type());
1017 
1018  // The type may contain side-effects.
1019  if(!clean_code.empty())
1020  {
1021  side_effect_exprt side_effect_expr(ID_statement_expression, void_type());
1022  code_blockt decl_block(clean_code);
1023  decl_block.set_statement(ID_decl_block);
1024  side_effect_expr.copy_to_operands(decl_block);
1025  clean_code.clear();
1026 
1027  // We merge the side-effect into the operand of the typecast,
1028  // using a comma-expression.
1029  // I.e., (type)e becomes (type)(side-effect, e)
1030  // It is not obvious whether the type or 'e' should be evaluated
1031  // first.
1032 
1033  exprt comma_expr(ID_comma, op.type());
1034  comma_expr.copy_to_operands(side_effect_expr, op);
1035  op.swap(comma_expr);
1036  }
1037 
1038  const typet expr_type=follow(expr.type());
1039 
1040  if(expr_type.id()==ID_union &&
1041  !base_type_eq(expr_type, op.type(), *this) &&
1042  op.id()!=ID_initializer_list)
1043  {
1044  // This is a GCC extension. It's either a 'temporary union',
1045  // where the argument is one of the member types.
1046 
1047  // This is one of the few places where it's detectable
1048  // that we are using "bool" for boolean operators instead
1049  // of "int". We convert for this reason.
1050  if(follow(op.type()).id()==ID_bool)
1052 
1053  // we need to find a member with the right type
1054  const union_typet &union_type=to_union_type(expr_type);
1055  const union_typet::componentst &components=union_type.components();
1056 
1057  for(union_typet::componentst::const_iterator
1058  it=components.begin();
1059  it!=components.end();
1060  it++)
1061  {
1062  if(base_type_eq(it->type(), op.type(), *this))
1063  {
1064  // found! build union constructor
1065  union_exprt union_expr(expr.type());
1066  union_expr.add_source_location()=expr.source_location();
1067  union_expr.op()=op;
1068  union_expr.set_component_name(it->get_name());
1069  expr=union_expr;
1070  expr.set(ID_C_lvalue, true);
1071  return;
1072  }
1073  }
1074 
1075  // not found, complain
1076  err_location(expr);
1077  error() << "type cast to union: type `"
1078  << to_string(op.type()) << "' not found in union" << eom;
1079  throw 0;
1080  }
1081 
1082  // We allow (TYPE){ initializer_list }
1083  // This is called "compound literal", and is syntactic
1084  // sugar for a (possibly local) declaration.
1085  if(op.id()==ID_initializer_list)
1086  {
1087  // just do a normal initialization
1088  do_initializer(op, expr.type(), false);
1089 
1090  // This produces a struct-expression,
1091  // union-expression, array-expression,
1092  // or an expression for a pointer or scalar.
1093  // We produce a compound_literal expression.
1094  exprt tmp(ID_compound_literal, expr.type());
1095  tmp.move_to_operands(op);
1096  expr=tmp;
1097  expr.set(ID_C_lvalue, true); // these are l-values
1098  return;
1099  }
1100 
1101  // a cast to void is always fine
1102  if(expr_type.id()==ID_empty)
1103  return;
1104 
1105  const typet op_type=follow(op.type());
1106 
1107  // cast to same type?
1108  if(base_type_eq(expr_type, op_type, *this))
1109  return; // it's ok
1110 
1111  // vectors?
1112 
1113  if(expr_type.id()==ID_vector)
1114  {
1115  // we are generous -- any vector to vector is fine
1116  if(op_type.id()==ID_vector)
1117  return;
1118  else if(op_type.id()==ID_signedbv ||
1119  op_type.id()==ID_unsignedbv)
1120  return;
1121  }
1122 
1123  if(!is_numeric_type(expr_type) && expr_type.id()!=ID_pointer)
1124  {
1125  err_location(expr);
1126  error() << "type cast to `"
1127  << to_string(expr_type) << "' is not permitted" << eom;
1128  throw 0;
1129  }
1130 
1131  if(is_numeric_type(op_type) || op_type.id()==ID_pointer)
1132  {
1133  }
1134  else if(op_type.id()==ID_array)
1135  {
1136  index_exprt index;
1137  index.array()=op;
1138  index.index()=from_integer(0, index_type());
1139  index.type()=op_type.subtype();
1140  op=address_of_exprt(index);
1141  }
1142  else if(op_type.id()==ID_empty)
1143  {
1144  if(expr_type.id()!=ID_empty)
1145  {
1146  err_location(expr);
1147  error() << "type cast from void only permitted to void, but got `"
1148  << to_string(expr.type()) << "'" << eom;
1149  throw 0;
1150  }
1151  }
1152  else if(op_type.id()==ID_vector)
1153  {
1154  const vector_typet &op_vector_type=
1155  to_vector_type(op_type);
1156 
1157  // gcc allows conversion of a vector of size 1 to
1158  // an integer/float of the same size
1159  if((expr_type.id()==ID_signedbv ||
1160  expr_type.id()==ID_unsignedbv) &&
1161  pointer_offset_bits(expr_type, *this)==
1162  pointer_offset_bits(op_vector_type, *this))
1163  {
1164  }
1165  else
1166  {
1167  err_location(expr);
1168  error() << "type cast from vector to `"
1169  << to_string(expr.type()) << "' not permitted" << eom;
1170  throw 0;
1171  }
1172  }
1173  else
1174  {
1175  err_location(expr);
1176  error() << "type cast from `"
1177  << to_string(op_type) << "' not permitted" << eom;
1178  throw 0;
1179  }
1180 
1181  // The new thing is an lvalue if the previous one is
1182  // an lvalue and it's just a pointer type cast.
1183  // This isn't really standard conformant!
1184  // Note that gcc says "warning: target of assignment not really an lvalue;
1185  // this will be a hard error in the future", i.e., we
1186  // can hope that the code below will one day simply go away.
1187 
1188  // Current versions of gcc in fact refuse to do this! Yay!
1189 
1190  if(expr.op0().get_bool(ID_C_lvalue))
1191  {
1192  if(expr_type.id()==ID_pointer)
1193  expr.set(ID_C_lvalue, true);
1194  }
1195 }
1196 
1198 {
1199  implicit_typecast(expr, index_type());
1200 }
1201 
1203 {
1204  if(expr.operands().size()!=2)
1205  {
1206  err_location(expr);
1207  error() << "operator `" << expr.id()
1208  << "' expects two operands" << eom;
1209  throw 0;
1210  }
1211 
1212  exprt &array_expr=expr.op0();
1213  exprt &index_expr=expr.op1();
1214 
1215  // we might have to swap them
1216 
1217  {
1218  const typet &array_full_type=follow(array_expr.type());
1219  const typet &index_full_type=follow(index_expr.type());
1220 
1221  if(array_full_type.id()!=ID_array &&
1222  array_full_type.id()!=ID_pointer &&
1223  array_full_type.id()!=ID_vector &&
1224  (index_full_type.id()==ID_array ||
1225  index_full_type.id()==ID_pointer ||
1226  index_full_type.id()==ID_vector))
1227  std::swap(array_expr, index_expr);
1228  }
1229 
1230  make_index_type(index_expr);
1231 
1232  const typet &final_array_type=follow(array_expr.type());
1233 
1234  if(final_array_type.id()==ID_array ||
1235  final_array_type.id()==ID_vector)
1236  {
1237  if(array_expr.get_bool(ID_C_lvalue))
1238  expr.set(ID_C_lvalue, true);
1239  }
1240  else if(final_array_type.id()==ID_pointer)
1241  {
1242  // p[i] is syntactic sugar for *(p+i)
1243 
1245  exprt addition(ID_plus, array_expr.type());
1246  addition.operands().swap(expr.operands());
1247  expr.move_to_operands(addition);
1248  expr.id(ID_dereference);
1249  expr.set(ID_C_lvalue, true);
1250  }
1251  else
1252  {
1253  err_location(expr);
1254  error() << "operator [] must take array/vector or pointer but got `"
1255  << to_string(array_expr.type()) << "'" << eom;
1256  throw 0;
1257  }
1258 
1259  expr.type()=final_array_type.subtype();
1260 }
1261 
1263 {
1264  // equality and disequality on float is not mathematical equality!
1265  assert(expr.operands().size()==2);
1266 
1267  if(follow(expr.op0().type()).id()==ID_floatbv)
1268  {
1269  if(expr.id()==ID_equal)
1270  expr.id(ID_ieee_float_equal);
1271  else if(expr.id()==ID_notequal)
1272  expr.id(ID_ieee_float_notequal);
1273  }
1274 }
1275 
1277  binary_relation_exprt &expr)
1278 {
1279  exprt &op0=expr.op0();
1280  exprt &op1=expr.op1();
1281 
1282  const typet o_type0=op0.type();
1283  const typet o_type1=op1.type();
1284 
1285  if(follow(o_type0).id()==ID_vector ||
1286  follow(o_type1).id()==ID_vector)
1287  {
1289  return;
1290  }
1291 
1292  expr.type()=bool_typet();
1293 
1294  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1295  {
1296  if(follow(o_type0)==follow(o_type1))
1297  {
1298  const typet &final_type=follow(o_type0);
1299  if(final_type.id()!=ID_array &&
1300  final_type.id()!=ID_incomplete_struct)
1301  {
1302  adjust_float_rel(expr);
1303  return; // no promotion necessary
1304  }
1305  }
1306  }
1307 
1308  implicit_typecast_arithmetic(op0, op1);
1309 
1310  const typet &type0=op0.type();
1311  const typet &type1=op1.type();
1312 
1313  if(type0==type1)
1314  {
1315  if(is_number(type0))
1316  {
1317  adjust_float_rel(expr);
1318  return;
1319  }
1320 
1321  if(type0.id()==ID_pointer)
1322  {
1323  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1324  return;
1325 
1326  if(expr.id()==ID_le || expr.id()==ID_lt ||
1327  expr.id()==ID_ge || expr.id()==ID_gt)
1328  return;
1329  }
1330 
1331  if(type0.id()==ID_string_constant)
1332  {
1333  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1334  return;
1335  }
1336  }
1337  else
1338  {
1339  // pointer and zero
1340  if(type0.id()==ID_pointer &&
1341  simplify_expr(op1, *this).is_zero())
1342  {
1343  op1=constant_exprt(ID_NULL, type0);
1344  return;
1345  }
1346 
1347  if(type1.id()==ID_pointer &&
1348  simplify_expr(op0, *this).is_zero())
1349  {
1350  op0=constant_exprt(ID_NULL, type1);
1351  return;
1352  }
1353 
1354  // pointer and integer
1355  if(type0.id()==ID_pointer && is_number(type1))
1356  {
1357  op1.make_typecast(type0);
1358  return;
1359  }
1360 
1361  if(type1.id()==ID_pointer && is_number(type0))
1362  {
1363  op0.make_typecast(type1);
1364  return;
1365  }
1366 
1367  if(type0.id()==ID_pointer && type1.id()==ID_pointer)
1368  {
1369  op1.make_typecast(type0);
1370  return;
1371  }
1372  }
1373 
1374  err_location(expr);
1375  error() << "operator `" << expr.id()
1376  << "' not defined for types `"
1377  << to_string(o_type0) << "' and `"
1378  << to_string(o_type1) << "'" << eom;
1379  throw 0;
1380 }
1381 
1383  binary_relation_exprt &expr)
1384 {
1385  exprt &op0=expr.op0();
1386  exprt &op1=expr.op1();
1387 
1388  const typet o_type0=follow(op0.type());
1389  const typet o_type1=follow(op1.type());
1390 
1391  if(o_type0.id()!=ID_vector ||
1392  o_type1.id()!=ID_vector ||
1393  follow(o_type0.subtype())!=follow(o_type1.subtype()))
1394  {
1395  err_location(expr);
1396  error() << "vector operator `" << expr.id()
1397  << "' not defined for types `"
1398  << to_string(o_type0) << "' and `"
1399  << to_string(o_type1) << "'" << eom;
1400  throw 0;
1401  }
1402 
1403  // Comparisons between vectors produce a vector
1404  // of integers with the same dimension.
1405  expr.type()=vector_typet(signed_int_type(), to_vector_type(o_type0).size());
1406 }
1407 
1409 {
1410  if(expr.operands().size()!=1)
1411  {
1412  err_location(expr);
1413  error() << "ptrmember operator expects one operand" << eom;
1414  throw 0;
1415  }
1416 
1417  const typet &final_op0_type=follow(expr.op0().type());
1418 
1419  if(final_op0_type.id()!=ID_pointer &&
1420  final_op0_type.id()!=ID_array)
1421  {
1422  err_location(expr);
1423  error() << "ptrmember operator requires pointer type "
1424  "on left hand side, but got `"
1425  << to_string(expr.op0().type()) << "'" << eom;
1426  throw 0;
1427  }
1428 
1429  // turn x->y into (*x).y
1430 
1431  exprt deref(ID_dereference);
1432  deref.move_to_operands(expr.op0());
1433  deref.add_source_location()=expr.source_location();
1434 
1436 
1437  expr.op0().swap(deref);
1438 
1439  expr.id(ID_member);
1440  typecheck_expr_member(expr);
1441 }
1442 
1444 {
1445  if(expr.operands().size()!=1)
1446  {
1447  err_location(expr);
1448  error() << "member operator expects one operand" << eom;
1449  throw 0;
1450  }
1451 
1452  exprt &op0=expr.op0();
1453  typet type=op0.type();
1454 
1455  follow_symbol(type);
1456 
1457  if(type.id()==ID_incomplete_struct)
1458  {
1459  err_location(expr);
1460  error() << "member operator got incomplete struct type "
1461  "on left hand side" << eom;
1462  throw 0;
1463  }
1464 
1465  if(type.id()==ID_incomplete_union)
1466  {
1467  err_location(expr);
1468  error() << "member operator got incomplete union type "
1469  "on left hand side" << eom;
1470  throw 0;
1471  }
1472 
1473  if(type.id()!=ID_struct &&
1474  type.id()!=ID_union)
1475  {
1476  err_location(expr);
1477  error() << "member operator requires structure type "
1478  "on left hand side but got `"
1479  << to_string(type) << "'" << eom;
1480  throw 0;
1481  }
1482 
1483  const struct_union_typet &struct_union_type=
1484  to_struct_union_type(type);
1485 
1486  const irep_idt &component_name=
1487  expr.get(ID_component_name);
1488 
1489  // first try to find directly
1491  struct_union_type.get_component(component_name);
1492 
1493  // if that fails, search the anonymous members
1494 
1495  if(component.is_nil())
1496  {
1497  exprt tmp=get_component_rec(op0, component_name, *this);
1498 
1499  if(tmp.is_nil())
1500  {
1501  // give up
1502  err_location(expr);
1503  error() << "member `" << component_name
1504  << "' not found in `"
1505  << to_string(type) << "'" << eom;
1506  throw 0;
1507  }
1508 
1509  // done!
1510  expr.swap(tmp);
1511  return;
1512  }
1513 
1514  expr.type()=component.type();
1515 
1516  if(op0.get_bool(ID_C_lvalue))
1517  expr.set(ID_C_lvalue, true);
1518 
1519  if(op0.get_bool(ID_C_constant) || type.get_bool(ID_C_constant))
1520  expr.set(ID_C_constant, true);
1521 
1522  // copy method identifier
1523  const irep_idt &identifier=component.get(ID_C_identifier);
1524 
1525  if(!identifier.empty())
1526  expr.set(ID_C_identifier, identifier);
1527 
1528  const irep_idt &access=component.get_access();
1529 
1530  if(access==ID_private)
1531  {
1532  err_location(expr);
1533  error() << "member `" << component_name
1534  << "' is " << access << eom;
1535  throw 0;
1536  }
1537 }
1538 
1540 {
1541  exprt::operandst &operands=expr.operands();
1542 
1543  assert(operands.size()==3);
1544 
1545  // copy (save) original types
1546  const typet o_type0=operands[0].type();
1547  const typet o_type1=operands[1].type();
1548  const typet o_type2=operands[2].type();
1549 
1550  implicit_typecast_bool(operands[0]);
1551  implicit_typecast_arithmetic(operands[1], operands[2]);
1552 
1553  if(operands[1].type().id()==ID_pointer &&
1554  operands[2].type().id()!=ID_pointer)
1555  implicit_typecast(operands[2], operands[1].type());
1556  else if(operands[2].type().id()==ID_pointer &&
1557  operands[1].type().id()!=ID_pointer)
1558  implicit_typecast(operands[1], operands[2].type());
1559 
1560  if(operands[1].type().id()==ID_pointer &&
1561  operands[2].type().id()==ID_pointer &&
1562  operands[1].type()!=operands[2].type())
1563  {
1564  exprt tmp1=simplify_expr(operands[1], *this);
1565  exprt tmp2=simplify_expr(operands[2], *this);
1566 
1567  // is one of them void * AND null? Convert that to the other.
1568  // (at least that's how GCC behaves)
1569  if(operands[1].type().subtype().id()==ID_empty &&
1570  tmp1.is_constant() &&
1571  to_constant_expr(tmp1).get_value()==ID_NULL)
1572  implicit_typecast(operands[1], operands[2].type());
1573  else if(operands[2].type().subtype().id()==ID_empty &&
1574  tmp2.is_constant() &&
1575  to_constant_expr(tmp2).get_value()==ID_NULL)
1576  implicit_typecast(operands[2], operands[1].type());
1577  else if(operands[1].type().subtype().id()!=ID_code ||
1578  operands[2].type().subtype().id()!=ID_code)
1579  {
1580  // Make it void *.
1581  // gcc and clang issue a warning for this.
1582  expr.type()=typet(ID_pointer);
1583  expr.type().subtype()=typet(ID_empty);
1584  implicit_typecast(operands[1], expr.type());
1585  implicit_typecast(operands[2], expr.type());
1586  }
1587  else
1588  {
1589  // maybe functions without parameter lists
1590  const code_typet &c_type1=to_code_type(operands[1].type().subtype());
1591  const code_typet &c_type2=to_code_type(operands[2].type().subtype());
1592 
1593  if(c_type1.return_type()==c_type2.return_type())
1594  {
1595  if(c_type1.parameters().empty() && c_type1.has_ellipsis())
1596  implicit_typecast(operands[1], operands[2].type());
1597  else if(c_type2.parameters().empty() && c_type2.has_ellipsis())
1598  implicit_typecast(operands[2], operands[1].type());
1599  }
1600  }
1601  }
1602 
1603  if(operands[1].type().id()==ID_empty ||
1604  operands[2].type().id()==ID_empty)
1605  {
1606  expr.type()=void_type();
1607  return;
1608  }
1609 
1610  if(follow(operands[1].type())==follow(operands[2].type()))
1611  {
1612  expr.type()=operands[1].type();
1613 
1614  // GCC says: "A conditional expression is a valid lvalue
1615  // if its type is not void and the true and false branches
1616  // are both valid lvalues."
1617 
1618  if(operands[1].get_bool(ID_C_lvalue) &&
1619  operands[2].get_bool(ID_C_lvalue))
1620  expr.set(ID_C_lvalue, true);
1621 
1622  return;
1623  }
1624 
1625  err_location(expr);
1626  error() << "operator ?: not defined for types `"
1627  << to_string(o_type1) << "' and `"
1628  << to_string(o_type2) << "'" << eom;
1629  throw 0;
1630 }
1631 
1633  side_effect_exprt &expr)
1634 {
1635  // x ? : y is almost the same as x ? x : y,
1636  // but not quite, as x is evaluated only once
1637 
1638  exprt::operandst &operands=expr.operands();
1639 
1640  if(operands.size()!=2)
1641  {
1642  err_location(expr);
1643  error() << "gcc conditional_expr expects two operands" << eom;
1644  throw 0;
1645  }
1646 
1647  // use typechecking code for "if"
1648 
1649  if_exprt if_expr;
1650  if_expr.cond()=operands[0];
1651  if_expr.true_case()=operands[0];
1652  if_expr.false_case()=operands[1];
1653  if_expr.add_source_location()=expr.source_location();
1654 
1655  typecheck_expr_trinary(if_expr);
1656 
1657  // copy the result
1658  expr.op0()=if_expr.op1();
1659  expr.op1()=if_expr.op2();
1660  expr.type()=if_expr.type();
1661 }
1662 
1664 {
1665  if(expr.operands().size()!=1)
1666  {
1667  err_location(expr);
1668  error() << "unary operator & expects one operand" << eom;
1669  throw 0;
1670  }
1671 
1672  exprt &op=expr.op0();
1673 
1674  if(op.type().id()==ID_c_bit_field)
1675  {
1676  err_location(expr);
1677  error() << "cannot take address of a bit field" << eom;
1678  throw 0;
1679  }
1680 
1681  // special case: address of label
1682  if(op.id()==ID_label)
1683  {
1684  expr.type()=pointer_type(void_type());
1685 
1686  // remember the label
1687  labels_used[op.get(ID_identifier)]=op.source_location();
1688  return;
1689  }
1690 
1691  // special case: address of function designator
1692  // ANSI-C 99 section 6.3.2.1 paragraph 4
1693 
1694  if(op.id()==ID_address_of &&
1695  op.get_bool(ID_C_implicit) &&
1696  op.operands().size()==1 &&
1697  op.op0().type().id()==ID_code)
1698  {
1699  // make the implicit address_of an explicit address_of
1700  exprt tmp;
1701  tmp.swap(op);
1702  tmp.set(ID_C_implicit, false);
1703  expr.swap(tmp);
1704  return;
1705  }
1706 
1707  if(op.id()==ID_struct ||
1708  op.id()==ID_union ||
1709  op.id()==ID_array ||
1710  op.id()==ID_string_constant)
1711  {
1712  // these are really objects
1713  }
1714  else if(op.get_bool(ID_C_lvalue))
1715  {
1716  // ok
1717  }
1718  else if(op.type().id()==ID_code)
1719  {
1720  // ok
1721  }
1722  else
1723  {
1724  err_location(expr);
1725  error() << "address_of error: `" << to_string(op)
1726  << "' not an lvalue" << eom;
1727  throw 0;
1728  }
1729 
1730  expr.type()=pointer_type(op.type());
1731 }
1732 
1734 {
1735  if(expr.operands().size()!=1)
1736  {
1737  err_location(expr);
1738  error() << "unary operator * expects one operand" << eom;
1739  throw 0;
1740  }
1741 
1742  exprt &op=expr.op0();
1743 
1744  const typet op_type=follow(op.type());
1745 
1746  if(op_type.id()==ID_array)
1747  {
1748  // *a is the same as a[0]
1749  expr.id(ID_index);
1750  expr.type()=op_type.subtype();
1752  assert(expr.operands().size()==2);
1753  }
1754  else if(op_type.id()==ID_pointer)
1755  {
1756  expr.type()=op_type.subtype();
1757  }
1758  else
1759  {
1760  err_location(expr);
1761  error() << "operand of unary * `" << to_string(op)
1762  << "' is not a pointer, but got `"
1763  << to_string(op_type) << "'" << eom;
1764  throw 0;
1765  }
1766 
1767  expr.set(ID_C_lvalue, true);
1768 
1769  // if you dereference a pointer pointing to
1770  // a function, you get a pointer again
1771  // allowing ******...*p
1772 
1774 }
1775 
1777 {
1778  if(expr.type().id()==ID_code)
1779  {
1780  address_of_exprt tmp(expr, pointer_type(expr.type()));
1781  tmp.set(ID_C_implicit, true);
1782  tmp.add_source_location()=expr.source_location();
1783  expr=tmp;
1784  }
1785 }
1786 
1788 {
1789  const irep_idt &statement=expr.get_statement();
1790 
1791  if(statement==ID_preincrement ||
1792  statement==ID_predecrement ||
1793  statement==ID_postincrement ||
1794  statement==ID_postdecrement)
1795  {
1796  if(expr.operands().size()!=1)
1797  {
1798  err_location(expr);
1799  error() << statement << "operator expects one operand" << eom;
1800  }
1801 
1802  const exprt &op0=expr.op0();
1803  const typet &type0=op0.type();
1804  const typet &final_type0=follow(type0);
1805 
1806  if(!op0.get_bool(ID_C_lvalue))
1807  {
1808  err_location(op0);
1809  error() << "prefix operator error: `" << to_string(op0)
1810  << "' not an lvalue" << eom;
1811  throw 0;
1812  }
1813 
1814  if(type0.get_bool(ID_C_constant))
1815  {
1816  err_location(op0);
1817  error() << "error: `" << to_string(op0)
1818  << "' is constant" << eom;
1819  throw 0;
1820  }
1821 
1822  if(final_type0.id()==ID_c_enum_tag)
1823  {
1824  if(follow_tag(to_c_enum_tag_type(final_type0)).id()==
1825  ID_incomplete_c_enum)
1826  {
1827  err_location(expr);
1828  error() << "operator `" << statement
1829  << "' given incomplete type `"
1830  << to_string(type0) << "'" << eom;
1831  throw 0;
1832  }
1833  else
1834  expr.type()=type0;
1835  }
1836  else if(final_type0.id()==ID_c_bit_field)
1837  {
1838  // promote to underlying type
1839  typet underlying_type=to_c_bit_field_type(final_type0).subtype();
1840  expr.op0().make_typecast(underlying_type);
1841  expr.type()=underlying_type;
1842  }
1843  else if(is_numeric_type(final_type0))
1844  {
1845  expr.type()=type0;
1846  }
1847  else if(final_type0.id()==ID_pointer)
1848  {
1849  expr.type()=type0;
1851  }
1852  else
1853  {
1854  err_location(expr);
1855  error() << "operator `" << statement
1856  << "' not defined for type `"
1857  << to_string(type0) << "'" << eom;
1858  throw 0;
1859  }
1860  }
1861  else if(has_prefix(id2string(statement), "assign"))
1863  else if(statement==ID_function_call)
1866  else if(statement==ID_statement_expression)
1868  else if(statement==ID_gcc_conditional_expression)
1870  else
1871  {
1872  err_location(expr);
1873  error() << "unknown side effect: " << statement << eom;
1874  throw 0;
1875  }
1876 }
1877 
1880 {
1881  if(expr.operands().size()!=2)
1882  {
1883  err_location(expr);
1884  error() << "function_call side effect expects two operands" << eom;
1885  throw 0;
1886  }
1887 
1888  exprt &f_op=expr.function();
1889 
1890  // f_op is not yet typechecked, in contrast to the other arguments.
1891  // This is a big special case!
1892 
1893  if(f_op.id()==ID_symbol)
1894  {
1895  irep_idt identifier=to_symbol_expr(f_op).get_identifier();
1896 
1897  asm_label_mapt::const_iterator entry=
1898  asm_label_map.find(identifier);
1899  if(entry!=asm_label_map.end())
1900  identifier=entry->second;
1901 
1902  if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
1903  {
1904  // This is an undeclared function. Let's just add it.
1905  // We do a bit of return-type guessing, but just a bit.
1907 
1908  // The following isn't really right and sound, but there
1909  // are too many idiots out there who use malloc and the like
1910  // without the right header file.
1911  if(identifier=="malloc" ||
1912  identifier=="realloc" ||
1913  identifier=="reallocf" ||
1914  identifier=="valloc")
1915  return_type=pointer_type(void_type()); // void *
1916 
1917  symbolt new_symbol;
1918 
1919  new_symbol.name=identifier;
1920  new_symbol.base_name=identifier;
1921  new_symbol.location=expr.source_location();
1922  new_symbol.type=code_typet();
1923  new_symbol.type.set(ID_C_incomplete, true);
1924  new_symbol.type.add(ID_return_type)=return_type;
1925 
1926  // TODO: should also guess some argument types
1927 
1928  symbolt *symbol_ptr;
1929  move_symbol(new_symbol, symbol_ptr);
1930 
1932  warning() << "function `" << identifier << "' is not declared" << eom;
1933  }
1934  }
1935 
1936  // typecheck it now
1937  typecheck_expr(f_op);
1938 
1939  const typet f_op_type=follow(f_op.type());
1940 
1941  if(f_op_type.id()!=ID_pointer)
1942  {
1943  err_location(f_op);
1944  error() << "expected function/function pointer as argument but got `"
1945  << to_string(f_op_type) << "'" << eom;
1946  throw 0;
1947  }
1948 
1949  // do implicit dereference
1950  if(f_op.id()==ID_address_of &&
1951  f_op.get_bool(ID_C_implicit) &&
1952  f_op.operands().size()==1)
1953  {
1954  exprt tmp;
1955  tmp.swap(f_op.op0());
1956  f_op.swap(tmp);
1957  }
1958  else
1959  {
1960  exprt tmp(ID_dereference, f_op_type.subtype());
1961  tmp.set(ID_C_implicit, true);
1962  tmp.add_source_location()=f_op.source_location();
1963  tmp.move_to_operands(f_op);
1964  f_op.swap(tmp);
1965  }
1966 
1967  if(f_op.type().id()!=ID_code)
1968  {
1969  err_location(f_op);
1970  error() << "expected code as argument" << eom;
1971  throw 0;
1972  }
1973 
1974  const code_typet &code_type=to_code_type(f_op.type());
1975 
1976  expr.type()=code_type.return_type();
1977 
1978  exprt tmp=do_special_functions(expr);
1979 
1980  if(tmp.is_not_nil())
1981  expr.swap(tmp);
1982  else
1984 }
1985 
1988 {
1989  const exprt &f_op=expr.function();
1990  const source_locationt &source_location=expr.source_location();
1991 
1992  // some built-in functions
1993  if(f_op.id()!=ID_symbol)
1994  return nil_exprt();
1995 
1996  const irep_idt &identifier=to_symbol_expr(f_op).get_identifier();
1997 
1998  if(identifier==CPROVER_PREFIX "same_object")
1999  {
2000  if(expr.arguments().size()!=2)
2001  {
2002  err_location(f_op);
2003  error() << "same_object expects two operands" << eom;
2004  throw 0;
2005  }
2006 
2007  exprt same_object_expr=
2008  same_object(expr.arguments()[0], expr.arguments()[1]);
2009  same_object_expr.add_source_location()=source_location;
2010 
2011  return same_object_expr;
2012  }
2013  else if(identifier==CPROVER_PREFIX "get_must")
2014  {
2015  if(expr.arguments().size()!=2)
2016  {
2017  err_location(f_op);
2018  error() << "get_must expects two operands" << eom;
2019  throw 0;
2020  }
2021 
2023 
2024  exprt get_must_expr=
2026  expr.arguments()[0], "get_must", expr.arguments()[1]);
2027  get_must_expr.add_source_location()=source_location;
2028 
2029  return get_must_expr;
2030  }
2031  else if(identifier==CPROVER_PREFIX "get_may")
2032  {
2033  if(expr.arguments().size()!=2)
2034  {
2035  err_location(f_op);
2036  error() << "get_may expects two operands" << eom;
2037  throw 0;
2038  }
2039 
2041 
2042  exprt get_may_expr=
2044  expr.arguments()[0], "get_may", expr.arguments()[1]);
2045  get_may_expr.add_source_location()=source_location;
2046 
2047  return get_may_expr;
2048  }
2049  else if(identifier==CPROVER_PREFIX "invalid_pointer")
2050  {
2051  if(expr.arguments().size()!=1)
2052  {
2053  err_location(f_op);
2054  error() << "invalid_pointer expects one operand" << eom;
2055  throw 0;
2056  }
2057 
2058  predicate_exprt same_object_expr(ID_invalid_pointer);
2059  same_object_expr.operands()=expr.arguments();
2060  same_object_expr.add_source_location()=source_location;
2061 
2062  return same_object_expr;
2063  }
2064  else if(identifier==CPROVER_PREFIX "buffer_size")
2065  {
2066  if(expr.arguments().size()!=1)
2067  {
2068  err_location(f_op);
2069  error() << "buffer_size expects one operand" << eom;
2070  throw 0;
2071  }
2072 
2073  exprt buffer_size_expr("buffer_size", size_type());
2074  buffer_size_expr.operands()=expr.arguments();
2075  buffer_size_expr.add_source_location()=source_location;
2076 
2077  return buffer_size_expr;
2078  }
2079  else if(identifier==CPROVER_PREFIX "is_zero_string")
2080  {
2081  if(expr.arguments().size()!=1)
2082  {
2083  err_location(f_op);
2084  error() << "is_zero_string expects one operand" << eom;
2085  throw 0;
2086  }
2087 
2088  predicate_exprt is_zero_string_expr("is_zero_string");
2089  is_zero_string_expr.operands()=expr.arguments();
2090  is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
2091  is_zero_string_expr.add_source_location()=source_location;
2092 
2093  return is_zero_string_expr;
2094  }
2095  else if(identifier==CPROVER_PREFIX "zero_string_length")
2096  {
2097  if(expr.arguments().size()!=1)
2098  {
2099  err_location(f_op);
2100  error() << "zero_string_length expects one operand" << eom;
2101  throw 0;
2102  }
2103 
2104  exprt zero_string_length_expr("zero_string_length", size_type());
2105  zero_string_length_expr.operands()=expr.arguments();
2106  zero_string_length_expr.set(ID_C_lvalue, true); // make it an lvalue
2107  zero_string_length_expr.add_source_location()=source_location;
2108 
2109  return zero_string_length_expr;
2110  }
2111  else if(identifier==CPROVER_PREFIX "DYNAMIC_OBJECT")
2112  {
2113  if(expr.arguments().size()!=1)
2114  {
2115  err_location(f_op);
2116  error() << "dynamic_object expects one argument" << eom;
2117  throw 0;
2118  }
2119 
2120  exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
2121  dynamic_object_expr.operands()=expr.arguments();
2122  dynamic_object_expr.add_source_location()=source_location;
2123 
2124  return dynamic_object_expr;
2125  }
2126  else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
2127  {
2128  if(expr.arguments().size()!=1)
2129  {
2130  err_location(f_op);
2131  error() << "pointer_offset expects one argument" << eom;
2132  throw 0;
2133  }
2134 
2135  exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
2136  pointer_offset_expr.add_source_location()=source_location;
2137 
2138  if(expr.type()!=pointer_offset_expr.type())
2139  pointer_offset_expr.make_typecast(expr.type());
2140 
2141  return pointer_offset_expr;
2142  }
2143  else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
2144  {
2145  if(expr.arguments().size()!=1)
2146  {
2147  err_location(f_op);
2148  error() << "pointer_object expects one argument" << eom;
2149  throw 0;
2150  }
2151 
2152  exprt pointer_object_expr=exprt(ID_pointer_object, expr.type());
2153  pointer_object_expr.operands()=expr.arguments();
2154  pointer_object_expr.add_source_location()=source_location;
2155 
2156  return pointer_object_expr;
2157  }
2158  else if(identifier=="__builtin_bswap16" ||
2159  identifier=="__builtin_bswap32" ||
2160  identifier=="__builtin_bswap64")
2161  {
2163 
2164  if(expr.arguments().size()!=1)
2165  {
2166  err_location(f_op);
2167  error() << identifier << " expects one operand" << eom;
2168  throw 0;
2169  }
2170 
2171  exprt bswap_expr(ID_bswap, expr.type());
2172  bswap_expr.operands()=expr.arguments();
2173  bswap_expr.add_source_location()=source_location;
2174 
2175  return bswap_expr;
2176  }
2177  else if(identifier==CPROVER_PREFIX "isnanf" ||
2178  identifier==CPROVER_PREFIX "isnand" ||
2179  identifier==CPROVER_PREFIX "isnanld" ||
2180  identifier=="__builtin_isnan")
2181  {
2182  if(expr.arguments().size()!=1)
2183  {
2184  err_location(f_op);
2185  error() << "isnan expects one operand" << eom;
2186  throw 0;
2187  }
2188 
2189  exprt isnan_expr(ID_isnan, bool_typet());
2190  isnan_expr.operands()=expr.arguments();
2191  isnan_expr.add_source_location()=source_location;
2192 
2193  return isnan_expr;
2194  }
2195  else if(identifier==CPROVER_PREFIX "isfinitef" ||
2196  identifier==CPROVER_PREFIX "isfinited" ||
2197  identifier==CPROVER_PREFIX "isfiniteld")
2198  {
2199  if(expr.arguments().size()!=1)
2200  {
2201  err_location(f_op);
2202  error() << "isfinite expects one operand" << eom;
2203  throw 0;
2204  }
2205 
2206  exprt isfinite_expr(ID_isfinite, bool_typet());
2207  isfinite_expr.operands()=expr.arguments();
2208  isfinite_expr.add_source_location()=source_location;
2209 
2210  return isfinite_expr;
2211  }
2212  else if(identifier==CPROVER_PREFIX "inf" ||
2213  identifier=="__builtin_inf")
2214  {
2215  constant_exprt inf_expr=
2218  inf_expr.add_source_location()=source_location;
2219 
2220  return inf_expr;
2221  }
2222  else if(identifier==CPROVER_PREFIX "inff")
2223  {
2224  constant_exprt inff_expr=
2227  inff_expr.add_source_location()=source_location;
2228 
2229  return inff_expr;
2230  }
2231  else if(identifier==CPROVER_PREFIX "infl")
2232  {
2234  constant_exprt infl_expr=
2236  infl_expr.add_source_location()=source_location;
2237 
2238  return infl_expr;
2239  }
2240  else if(identifier==CPROVER_PREFIX "abs" ||
2241  identifier==CPROVER_PREFIX "labs" ||
2242  identifier==CPROVER_PREFIX "llabs" ||
2243  identifier==CPROVER_PREFIX "fabs" ||
2244  identifier==CPROVER_PREFIX "fabsf" ||
2245  identifier==CPROVER_PREFIX "fabsl")
2246  {
2247  if(expr.arguments().size()!=1)
2248  {
2249  err_location(f_op);
2250  error() << "abs-functions expect one operand" << eom;
2251  throw 0;
2252  }
2253 
2254  exprt abs_expr(ID_abs, expr.type());
2255  abs_expr.operands()=expr.arguments();
2256  abs_expr.add_source_location()=source_location;
2257 
2258  return abs_expr;
2259  }
2260  else if(identifier==CPROVER_PREFIX "malloc")
2261  {
2262  if(expr.arguments().size()!=1)
2263  {
2264  err_location(f_op);
2265  error() << "malloc expects one operand" << eom;
2266  throw 0;
2267  }
2268 
2269  exprt malloc_expr=side_effect_exprt(ID_malloc);
2270  malloc_expr.type()=expr.type();
2271  malloc_expr.add_source_location()=source_location;
2272  malloc_expr.operands()=expr.arguments();
2273 
2274  return malloc_expr;
2275  }
2276  else if(identifier==CPROVER_PREFIX "isinff" ||
2277  identifier==CPROVER_PREFIX "isinfd" ||
2278  identifier==CPROVER_PREFIX "isinfld" ||
2279  identifier=="__builtin_isinf")
2280  {
2281  if(expr.arguments().size()!=1)
2282  {
2283  err_location(f_op);
2284  error() << "isinf expects one operand" << eom;
2285  throw 0;
2286  }
2287 
2288  exprt isinf_expr(ID_isinf, bool_typet());
2289  isinf_expr.operands()=expr.arguments();
2290  isinf_expr.add_source_location()=source_location;
2291 
2292  return isinf_expr;
2293  }
2294  else if(identifier==CPROVER_PREFIX "isnormalf" ||
2295  identifier==CPROVER_PREFIX "isnormald" ||
2296  identifier==CPROVER_PREFIX "isnormalld")
2297  {
2298  if(expr.arguments().size()!=1)
2299  {
2300  err_location(f_op);
2301  error() << "isnormal expects one operand" << eom;
2302  throw 0;
2303  }
2304 
2305  exprt isnormal_expr(ID_isnormal, bool_typet());
2306  isnormal_expr.operands()=expr.arguments();
2307  isnormal_expr.add_source_location()=source_location;
2308 
2309  return isnormal_expr;
2310  }
2311  else if(identifier==CPROVER_PREFIX "signf" ||
2312  identifier==CPROVER_PREFIX "signd" ||
2313  identifier==CPROVER_PREFIX "signld" ||
2314  identifier=="__builtin_signbit" ||
2315  identifier=="__builtin_signbitf" ||
2316  identifier=="__builtin_signbitl")
2317  {
2318  if(expr.arguments().size()!=1)
2319  {
2320  err_location(f_op);
2321  error() << "sign expects one operand" << eom;
2322  throw 0;
2323  }
2324 
2325  exprt sign_expr(ID_sign, bool_typet());
2326  sign_expr.operands()=expr.arguments();
2327  sign_expr.add_source_location()=source_location;
2328 
2329  return sign_expr;
2330  }
2331  else if(identifier=="__builtin_popcount" ||
2332  identifier=="__builtin_popcountl" ||
2333  identifier=="__builtin_popcountll" ||
2334  identifier=="__popcnt16" ||
2335  identifier=="__popcnt" ||
2336  identifier=="__popcnt64")
2337  {
2338  if(expr.arguments().size()!=1)
2339  {
2340  err_location(f_op);
2341  error() << identifier << " expects one operand" << eom;
2342  throw 0;
2343  }
2344 
2345  exprt popcount_expr(ID_popcount, expr.type());
2346  popcount_expr.operands()=expr.arguments();
2347  popcount_expr.add_source_location()=source_location;
2348 
2349  return popcount_expr;
2350  }
2351  else if(identifier==CPROVER_PREFIX "equal")
2352  {
2353  if(expr.arguments().size()!=2)
2354  {
2355  err_location(f_op);
2356  error() << "equal expects two operands" << eom;
2357  throw 0;
2358  }
2359 
2360  equal_exprt equality_expr;
2361  equality_expr.operands()=expr.arguments();
2362  equality_expr.add_source_location()=source_location;
2363 
2364  if(!base_type_eq(equality_expr.lhs().type(),
2365  equality_expr.rhs().type(), *this))
2366  {
2367  err_location(f_op);
2368  error() << "equal expects two operands of same type" << eom;
2369  throw 0;
2370  }
2371 
2372  return equality_expr;
2373  }
2374  else if(identifier=="__builtin_expect")
2375  {
2376  // This is a gcc extension to provide branch prediction.
2377  // We compile it away, but adding some IR instruction for
2378  // this would clearly be an option. Note that the type
2379  // of the return value is wired to "long", i.e.,
2380  // this may trigger a type conversion due to the signature
2381  // of this function.
2382  if(expr.arguments().size()!=2)
2383  {
2384  err_location(f_op);
2385  error() << "__builtin_expect expects two arguments" << eom;
2386  throw 0;
2387  }
2388 
2389  return typecast_exprt(expr.arguments()[0], expr.type());
2390  }
2391  else if(identifier=="__builtin_object_size")
2392  {
2393  // this is a gcc extension to provide information about
2394  // object sizes at compile time
2395  // http://gcc.gnu.org/onlinedocs/gcc/Object-Size-Checking.html
2396 
2397  if(expr.arguments().size()!=2)
2398  {
2399  err_location(f_op);
2400  error() << "__builtin_object_size expects two arguments" << eom;
2401  throw 0;
2402  }
2403 
2404  make_constant(expr.arguments()[1]);
2405 
2406  mp_integer arg1;
2407 
2408  if(expr.arguments()[1].is_true())
2409  arg1=1;
2410  else if(expr.arguments()[1].is_false())
2411  arg1=0;
2412  else if(to_integer(expr.arguments()[1], arg1))
2413  {
2414  err_location(f_op);
2415  error() << "__builtin_object_size expects constant as second argument, "
2416  << "but got " << to_string(expr.arguments()[1]) << eom;
2417  throw 0;
2418  }
2419 
2420  exprt tmp;
2421 
2422  // the following means "don't know"
2423  if(arg1==0 || arg1==1)
2424  {
2425  tmp=from_integer(-1, size_type());
2426  tmp.add_source_location()=f_op.source_location();
2427  }
2428  else
2429  {
2430  tmp=from_integer(0, size_type());
2431  tmp.add_source_location()=f_op.source_location();
2432  }
2433 
2434  return tmp;
2435  }
2436  else if(identifier=="__builtin_choose_expr")
2437  {
2438  // this is a gcc extension similar to ?:
2439  if(expr.arguments().size()!=3)
2440  {
2441  err_location(f_op);
2442  error() << "__builtin_choose_expr expects three arguments" << eom;
2443  throw 0;
2444  }
2445 
2446  expr.arguments()[0].make_typecast(bool_typet());
2447  make_constant(expr.arguments()[0]);
2448 
2449  if(expr.arguments()[0].is_true())
2450  return expr.arguments()[1];
2451  else
2452  return expr.arguments()[2];
2453  }
2454  else if(identifier=="__builtin_constant_p")
2455  {
2456  // this is a gcc extension to tell whether the argument
2457  // is known to be a compile-time constant
2458  if(expr.arguments().size()!=1)
2459  {
2460  err_location(f_op);
2461  error() << "__builtin_constant_p expects one argument" << eom;
2462  throw 0;
2463  }
2464 
2465  // try to produce constant
2466  exprt tmp1=expr.arguments().front();
2467  simplify(tmp1, *this);
2468 
2469  bool is_constant=false;
2470 
2471  // Need to do some special treatment for string literals,
2472  // which are (void *)&("lit"[0])
2473  if(tmp1.id()==ID_typecast &&
2474  tmp1.operands().size()==1 &&
2475  tmp1.op0().id()==ID_address_of &&
2476  tmp1.op0().operands().size()==1 &&
2477  tmp1.op0().op0().id()==ID_index &&
2478  tmp1.op0().op0().operands().size()==2 &&
2479  tmp1.op0().op0().op0().id()==ID_string_constant)
2480  {
2481  is_constant=true;
2482  }
2483  else
2484  is_constant=tmp1.is_constant();
2485 
2486  exprt tmp2=from_integer(is_constant, expr.type());
2487  tmp2.add_source_location()=source_location;
2488 
2489  return tmp2;
2490  }
2491  else if(identifier=="__builtin_classify_type")
2492  {
2493  // This is a gcc extension that produces an integer
2494  // constant for the type of the argument expression.
2495  if(expr.arguments().size()!=1)
2496  {
2497  err_location(f_op);
2498  error() << "__builtin_classify_type expects one argument" << eom;
2499  throw 0;
2500  }
2501 
2502  exprt object=expr.arguments()[0];
2503 
2504  // The value doesn't matter at all, we only care about the type.
2505  // Need to sync with typeclass.h.
2506  const typet &type=follow(object.type());
2507 
2508  unsigned type_number=
2509  type.id()==ID_empty?0:
2510  type.id()==ID_c_enum_tag?3:
2511  (type.id()==ID_bool || type.id()==ID_c_bool)?4:
2512  type.id()==ID_pointer?5:
2513  type.id()==ID_floatbv?8:
2514  (type.id()==ID_complex && type.subtype().id()==ID_floatbv)?9:
2515  type.id()==ID_struct?12:
2516  type.id()==ID_union?13:
2517  type.id()==ID_array?14:
2518  1; // int, short
2519 
2520  // clang returns 15 for the three 'char' types,
2521  // gcc treats these as 'int'
2522 
2523  exprt tmp=from_integer(type_number, expr.type());
2524  tmp.add_source_location()=source_location;
2525 
2526  return tmp;
2527  }
2528  else if(identifier==CPROVER_PREFIX "float_debug1" ||
2529  identifier==CPROVER_PREFIX "float_debug2")
2530  {
2531  if(expr.arguments().size()!=2)
2532  {
2533  err_location(f_op);
2534  error() << "float_debug expects two operands" << eom;
2535  throw 0;
2536  }
2537 
2538  const irep_idt &id=
2539  identifier==CPROVER_PREFIX "float_debug1"?
2540  "float_debug1":"float_debug2";
2541 
2542  exprt float_debug_expr(id, expr.type());
2543  float_debug_expr.operands()=expr.arguments();
2544  float_debug_expr.add_source_location()=source_location;
2545 
2546  return float_debug_expr;
2547  }
2548  else if(identifier=="__sync_fetch_and_add" ||
2549  identifier=="__sync_fetch_and_sub" ||
2550  identifier=="__sync_fetch_and_or" ||
2551  identifier=="__sync_fetch_and_and" ||
2552  identifier=="__sync_fetch_and_xor" ||
2553  identifier=="__sync_fetch_and_nand" ||
2554  identifier=="__sync_add_and_fetch" ||
2555  identifier=="__sync_sub_and_fetch" ||
2556  identifier=="__sync_or_and_fetch" ||
2557  identifier=="__sync_and_and_fetch" ||
2558  identifier=="__sync_xor_and_fetch" ||
2559  identifier=="__sync_nand_and_fetch" ||
2560  identifier=="__sync_val_compare_and_swap" ||
2561  identifier=="__sync_lock_test_and_set" ||
2562  identifier=="__sync_lock_release")
2563  {
2564  // These are polymorphic, see
2565  // http://gcc.gnu.org/onlinedocs/gcc-4.1.1/gcc/Atomic-Builtins.html
2566 
2567  // adjust return type of function to match pointer subtype
2568  if(expr.arguments().empty())
2569  {
2570  err_location(f_op);
2571  error() << "__sync_* primitives take as least one argument" << eom;
2572  throw 0;
2573  }
2574 
2575  exprt &ptr_arg=expr.arguments().front();
2576 
2577  if(ptr_arg.type().id()!=ID_pointer)
2578  {
2579  err_location(f_op);
2580  error() << "__sync_* primitives take pointer as first argument" << eom;
2581  throw 0;
2582  }
2583 
2584  expr.type()=expr.arguments().front().type().subtype();
2585 
2586  return expr;
2587  }
2588  else
2589  return nil_exprt();
2590 }
2591 
2596 {
2597  const exprt &f_op=expr.function();
2598  const code_typet &code_type=to_code_type(f_op.type());
2599  exprt::operandst &arguments=expr.arguments();
2600  const code_typet::parameterst &parameter_types=
2601  code_type.parameters();
2602 
2603  // no. of arguments test
2604 
2605  if(code_type.get_bool(ID_C_incomplete))
2606  {
2607  // can't check
2608  }
2609  else if(code_type.is_KnR())
2610  {
2611  // We are generous on KnR; any number is ok.
2612  // We will in missing ones with "NIL".
2613 
2614  while(parameter_types.size()>arguments.size())
2615  arguments.push_back(nil_exprt());
2616  }
2617  else if(code_type.has_ellipsis())
2618  {
2619  if(parameter_types.size()>arguments.size())
2620  {
2621  err_location(expr);
2622  error() << "not enough function arguments" << eom;
2623  throw 0;
2624  }
2625  }
2626  else if(parameter_types.size()!=arguments.size())
2627  {
2628  err_location(expr);
2629  error() << "wrong number of function arguments: "
2630  << "expected " << parameter_types.size()
2631  << ", but got " << arguments.size() << eom;
2632  throw 0;
2633  }
2634 
2635  for(unsigned i=0; i<arguments.size(); i++)
2636  {
2637  exprt &op=arguments[i];
2638 
2639  if(op.is_nil())
2640  {
2641  // ignore
2642  }
2643  else if(i<parameter_types.size())
2644  {
2645  const code_typet::parametert &parameter_type=
2646  parameter_types[i];
2647 
2648  const typet &op_type=parameter_type.type();
2649 
2650  if(op_type.id()==ID_bool &&
2651  op.id()==ID_side_effect &&
2652  op.get(ID_statement)==ID_assign &&
2653  op.type().id()!=ID_bool)
2654  {
2656  warning() << "assignment where Boolean argument is expected" << eom;
2657  }
2658 
2659  implicit_typecast(op, op_type);
2660  }
2661  else
2662  {
2663  // don't know type, just do standard conversion
2664 
2665  const typet &type=follow(op.type());
2666  if(type.id()==ID_array)
2667  {
2668  typet dest_type=pointer_type(void_type());
2669  dest_type.subtype().set(ID_C_constant, ID_1);
2670  implicit_typecast(op, dest_type);
2671  }
2672  }
2673  }
2674 }
2675 
2677 {
2678  // nothing to do
2679 }
2680 
2682 {
2683  if(expr.operands().size()!=1)
2684  {
2685  err_location(expr);
2686  error() << "operator `" << expr.id()
2687  << "' expects one operand" << eom;
2688  throw 0;
2689  }
2690 
2691  exprt &operand=expr.op0();
2692 
2693  const typet &o_type=follow(operand.type());
2694 
2695  if(o_type.id()==ID_vector)
2696  {
2697  if(is_number(follow(o_type.subtype())))
2698  {
2699  // Vector arithmetic.
2700  expr.type()=operand.type();
2701  return;
2702  }
2703  }
2704 
2706 
2707  if(is_number(operand.type()))
2708  {
2709  expr.type()=operand.type();
2710  return;
2711  }
2712 
2713  err_location(expr);
2714  error() << "operator `" << expr.id()
2715  << "' not defined for type `"
2716  << to_string(operand.type()) << "'" << eom;
2717  throw 0;
2718 }
2719 
2721 {
2722  if(expr.operands().size()!=1)
2723  {
2724  err_location(expr);
2725  error() << "operator `" << expr.id()
2726  << "' expects one operand" << eom;
2727  throw 0;
2728  }
2729 
2730  exprt &operand=expr.op0();
2731 
2732  implicit_typecast_bool(operand);
2733 
2734  // This is not quite accurate: the standard says the result
2735  // should be of type 'int'.
2736  // We do 'bool' anyway to get more compact formulae. Eventually,
2737  // this should be achieved by means of simplification, and not
2738  // in the frontend.
2739  expr.type()=bool_typet();
2740 }
2741 
2743  const vector_typet &type0,
2744  const vector_typet &type1)
2745 {
2746  // This is relatively restrictive!
2747 
2748  // compare dimension
2749  mp_integer s0, s1;
2750  if(to_integer(type0.size(), s0))
2751  return false;
2752  if(to_integer(type1.size(), s1))
2753  return false;
2754  if(s0!=s1)
2755  return false;
2756 
2757  // compare subtype
2758  if((type0.subtype().id()==ID_signedbv ||
2759  type0.subtype().id()==ID_unsignedbv) &&
2760  (type1.subtype().id()==ID_signedbv ||
2761  type1.subtype().id()==ID_unsignedbv) &&
2762  to_bitvector_type(type0.subtype()).get_width()==
2763  to_bitvector_type(type1.subtype()).get_width())
2764  return true;
2765 
2766  return type0.subtype()==type1.subtype();
2767 }
2768 
2770 {
2771  if(expr.operands().size()!=2)
2772  {
2773  err_location(expr);
2774  error() << "operator `" << expr.id()
2775  << "' expects two operands" << eom;
2776  throw 0;
2777  }
2778 
2779  exprt &op0=expr.op0();
2780  exprt &op1=expr.op1();
2781 
2782  const typet o_type0=follow(op0.type());
2783  const typet o_type1=follow(op1.type());
2784 
2785  if(o_type0.id()==ID_vector &&
2786  o_type1.id()==ID_vector)
2787  {
2789  to_vector_type(o_type0), to_vector_type(o_type1)) &&
2790  is_number(follow(o_type0.subtype())))
2791  {
2792  // Vector arithmetic has fairly strict typing rules, no promotion
2793  if(o_type0!=o_type1)
2794  op1.make_typecast(op0.type());
2795  expr.type()=op0.type();
2796  return;
2797  }
2798  }
2799 
2800  // promote!
2801 
2802  implicit_typecast_arithmetic(op0, op1);
2803 
2804  const typet &type0=follow(op0.type());
2805  const typet &type1=follow(op1.type());
2806 
2807  if(expr.id()==ID_plus || expr.id()==ID_minus ||
2808  expr.id()==ID_mult || expr.id()==ID_div)
2809  {
2810  if(type0.id()==ID_pointer || type1.id()==ID_pointer)
2811  {
2813  return;
2814  }
2815  else if(type0==type1)
2816  {
2817  if(is_number(type0))
2818  {
2819  expr.type()=type0;
2820  return;
2821  }
2822  }
2823  }
2824  else if(expr.id()==ID_mod)
2825  {
2826  if(type0==type1)
2827  {
2828  if(type0.id()==ID_signedbv || type0.id()==ID_unsignedbv)
2829  {
2830  expr.type()=type0;
2831  return;
2832  }
2833  }
2834  }
2835  else if(expr.id()==ID_bitand ||
2836  expr.id()==ID_bitxor ||
2837  expr.id()==ID_bitor)
2838  {
2839  if(type0==type1)
2840  {
2841  if(is_number(type0))
2842  {
2843  expr.type()=type0;
2844  return;
2845  }
2846  else if(type0.id()==ID_bool)
2847  {
2848  if(expr.id()==ID_bitand)
2849  expr.id(ID_and);
2850  else if(expr.id()==ID_bitor)
2851  expr.id(ID_or);
2852  else if(expr.id()==ID_bitxor)
2853  expr.id(ID_xor);
2854  else
2855  assert(false);
2856  expr.type()=type0;
2857  return;
2858  }
2859  }
2860  }
2861 
2862  err_location(expr);
2863  error() << "operator `" << expr.id()
2864  << "' not defined for types `"
2865  << to_string(o_type0) << "' and `"
2866  << to_string(o_type1) << "'" << eom;
2867  throw 0;
2868 }
2869 
2871 {
2872  assert(expr.id()==ID_shl || expr.id()==ID_shr);
2873 
2874  exprt &op0=expr.op0();
2875  exprt &op1=expr.op1();
2876 
2877  const typet o_type0=follow(op0.type());
2878  const typet o_type1=follow(op1.type());
2879 
2880  if(o_type0.id()==ID_vector &&
2881  o_type1.id()==ID_vector)
2882  {
2883  if(follow(o_type0.subtype())==follow(o_type1.subtype()) &&
2884  is_number(follow(o_type0.subtype())))
2885  {
2886  // {a0, a1, ..., an} >> {b0, b1, ..., bn} ==
2887  // {a0 >> b0, a1 >> b1, ..., an >> bn}
2888  // Fairly strict typing rules, no promotion
2889  expr.type()=op0.type();
2890  return;
2891  }
2892  }
2893 
2894  if(o_type0.id()==ID_vector &&
2895  is_number(follow(o_type0.subtype())) &&
2896  is_number(o_type1))
2897  {
2898  // {a0, a1, ..., an} >> b == {a0 >> b, a1 >> b, ..., an >> b}
2899  expr.type()=op0.type();
2900  return;
2901  }
2902 
2903  // must do the promotions _separately_!
2906 
2907  if(is_number(op0.type()) &&
2908  is_number(op1.type()))
2909  {
2910  expr.type()=op0.type();
2911 
2912  if(expr.id()==ID_shr) // shifting operation depends on types
2913  {
2914  const typet &op0_type=follow(op0.type());
2915 
2916  if(op0_type.id()==ID_unsignedbv)
2917  {
2918  expr.id(ID_lshr);
2919  return;
2920  }
2921  else if(op0_type.id()==ID_signedbv)
2922  {
2923  expr.id(ID_ashr);
2924  return;
2925  }
2926  }
2927 
2928  return;
2929  }
2930 
2931  err_location(expr);
2932  error() << "operator `" << expr.id()
2933  << "' not defined for types `"
2934  << to_string(o_type0) << "' and `"
2935  << to_string(o_type1) << "'" << eom;
2936  throw 0;
2937 }
2938 
2940 {
2941  const typet &type=expr.type();
2942  assert(type.id()==ID_pointer);
2943 
2944  typet subtype=type.subtype();
2945 
2946  if(subtype.id()==ID_symbol)
2947  subtype=follow(subtype);
2948 
2949  if(subtype.id()==ID_incomplete_struct)
2950  {
2951  err_location(expr);
2952  error() << "pointer arithmetic with unknown object size" << eom;
2953  throw 0;
2954  }
2955 }
2956 
2958 {
2959  assert(expr.operands().size()==2);
2960 
2961  exprt &op0=expr.op0();
2962  exprt &op1=expr.op1();
2963 
2964  const typet &type0=follow(op0.type());
2965  const typet &type1=follow(op1.type());
2966 
2967  if(expr.id()==ID_minus ||
2968  (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_minus))
2969  {
2970  if(type0.id()==ID_pointer &&
2971  type1.id()==ID_pointer)
2972  {
2973  // We should check the subtypes, and complain if
2974  // they are really different.
2975  expr.type()=pointer_diff_type();
2978  return;
2979  }
2980 
2981  if(type0.id()==ID_pointer &&
2982  (type1.id()==ID_bool ||
2983  type1.id()==ID_c_bool ||
2984  type1.id()==ID_unsignedbv ||
2985  type1.id()==ID_signedbv ||
2986  type1.id()==ID_c_bit_field ||
2987  type1.id()==ID_c_enum_tag))
2988  {
2990  make_index_type(op1);
2991  expr.type()=type0;
2992  return;
2993  }
2994  }
2995  else if(expr.id()==ID_plus ||
2996  (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_plus))
2997  {
2998  exprt *p_op, *int_op;
2999 
3000  if(type0.id()==ID_pointer)
3001  {
3002  p_op=&op0;
3003  int_op=&op1;
3004  }
3005  else if(type1.id()==ID_pointer)
3006  {
3007  p_op=&op1;
3008  int_op=&op0;
3009  }
3010  else
3011  {
3012  p_op=int_op=nullptr;
3013  assert(false);
3014  }
3015 
3016  const typet &int_op_type=follow(int_op->type());
3017 
3018  if(int_op_type.id()==ID_bool ||
3019  int_op_type.id()==ID_c_bool ||
3020  int_op_type.id()==ID_unsignedbv ||
3021  int_op_type.id()==ID_signedbv ||
3022  int_op_type.id()==ID_c_bit_field ||
3023  int_op_type.id()==ID_c_enum_tag)
3024  {
3026  make_index_type(*int_op);
3027  expr.type()=p_op->type();
3028  return;
3029  }
3030  }
3031 
3032  irep_idt op_name;
3033 
3034  if(expr.id()==ID_side_effect)
3035  op_name=to_side_effect_expr(expr).get_statement();
3036  else
3037  op_name=expr.id();
3038 
3039  err_location(expr);
3040  error() << "operator `" << op_name
3041  << "' not defined for types `"
3042  << to_string(type0) << "' and `"
3043  << to_string(type1) << "'" << eom;
3044  throw 0;
3045 }
3046 
3048 {
3049  if(expr.operands().size()!=2)
3050  {
3051  err_location(expr);
3052  error() << "operator `" << expr.id()
3053  << "' expects two operands" << eom;
3054  throw 0;
3055  }
3056 
3057  implicit_typecast_bool(expr.op0());
3058  implicit_typecast_bool(expr.op1());
3059 
3060  // This is not quite accurate: the standard says the result
3061  // should be of type 'int'.
3062  // We do 'bool' anyway to get more compact formulae. Eventually,
3063  // this should be achieved by means of simplification, and not
3064  // in the frontend.
3065  expr.type()=bool_typet();
3066 }
3067 
3069  side_effect_exprt &expr)
3070 {
3071  if(expr.operands().size()!=2)
3072  {
3073  err_location(expr);
3074  error() << "operator `" << expr.get_statement()
3075  << "' expects two operands" << eom;
3076  throw 0;
3077  }
3078 
3079  const irep_idt &statement=expr.get_statement();
3080 
3081  exprt &op0=expr.op0();
3082  exprt &op1=expr.op1();
3083 
3084  {
3085  const typet &type0=op0.type();
3086 
3087  if(type0.id()==ID_empty)
3088  {
3089  err_location(expr);
3090  error() << "cannot assign void" << eom;
3091  throw 0;
3092  }
3093 
3094  if(!op0.get_bool(ID_C_lvalue))
3095  {
3096  err_location(expr);
3097  error() << "assignment error: `" << to_string(op0)
3098  << "' not an lvalue" << eom;
3099  throw 0;
3100  }
3101 
3102  if(type0.get_bool(ID_C_constant))
3103  {
3104  err_location(expr);
3105  error() << "`" << to_string(op0)
3106  << "' is constant" << eom;
3107  throw 0;
3108  }
3109 
3110  // refuse to assign arrays
3111  if(type0.id()==ID_array ||
3112  type0.id()==ID_incomplete_array)
3113  {
3114  err_location(expr);
3115  error() << "direct assignments to arrays not permitted" << eom;
3116  throw 0;
3117  }
3118  }
3119 
3120  // Add a cast to the underlying type for bit fields.
3121  // In particular, sizeof(s.f=1) works for bit fields.
3122  if(op0.type().id()==ID_c_bit_field)
3123  op0.make_typecast(op0.type().subtype());
3124 
3125  const typet o_type0=op0.type();
3126  const typet o_type1=op1.type();
3127 
3128  expr.type()=o_type0;
3129 
3130  if(statement==ID_assign)
3131  {
3132  implicit_typecast(op1, o_type0);
3133  return;
3134  }
3135  else if(statement==ID_assign_shl ||
3136  statement==ID_assign_shr)
3137  {
3139 
3140  if(is_number(op1.type()))
3141  {
3142  if(statement==ID_assign_shl)
3143  {
3144  return;
3145  }
3146  else // assign_shr
3147  {
3148  // distinguish arithmetic from logical shifts by looking at type
3149 
3150  typet underlying_type=op0.type();
3151 
3152  if(underlying_type.id()==ID_c_enum_tag)
3153  {
3154  const typet &c_enum_type=
3155  follow_tag(to_c_enum_tag_type(underlying_type));
3156  underlying_type=c_enum_type.subtype();
3157  }
3158 
3159  if(underlying_type.id()==ID_unsignedbv ||
3160  underlying_type.id()==ID_c_bool)
3161  {
3162  expr.set(ID_statement, ID_assign_lshr);
3163  return;
3164  }
3165  else if(underlying_type.id()==ID_signedbv)
3166  {
3167  expr.set(ID_statement, ID_assign_ashr);
3168  return;
3169  }
3170  }
3171  }
3172  }
3173  else if(statement==ID_assign_bitxor ||
3174  statement==ID_assign_bitand ||
3175  statement==ID_assign_bitor)
3176  {
3177  // these are more restrictive
3178  if(o_type0.id()==ID_bool ||
3179  o_type0.id()==ID_c_bool)
3180  {
3182  if(op1.type().id()==ID_bool ||
3183  op1.type().id()==ID_c_bool ||
3184  op1.type().id()==ID_c_enum_tag ||
3185  op1.type().id()==ID_unsignedbv ||
3186  op1.type().id()==ID_signedbv)
3187  return;
3188  }
3189  else if(o_type0.id()==ID_c_enum_tag ||
3190  o_type0.id()==ID_unsignedbv ||
3191  o_type0.id()==ID_signedbv ||
3192  o_type0.id()==ID_c_bit_field)
3193  {
3194  implicit_typecast(op1, o_type0);
3195  return;
3196  }
3197  else if(o_type0.id()==ID_vector &&
3198  o_type1.id()==ID_vector)
3199  {
3200  // We are willing to do a modest amount of conversion
3202  to_vector_type(o_type0), to_vector_type(o_type1)))
3203  {
3204  if(o_type0!=o_type1)
3205  op1.make_typecast(o_type0);
3206  return;
3207  }
3208  }
3209  }
3210  else
3211  {
3212  if(o_type0.id()==ID_pointer &&
3213  (statement==ID_assign_minus || statement==ID_assign_plus))
3214  {
3216  return;
3217  }
3218  else if(o_type0.id()==ID_vector &&
3219  o_type1.id()==ID_vector)
3220  {
3221  // We are willing to do a modest amount of conversion
3223  to_vector_type(o_type0), to_vector_type(o_type1)))
3224  {
3225  if(o_type0!=o_type1)
3226  op1.make_typecast(o_type0);
3227  return;
3228  }
3229  }
3230  else if(o_type0.id()==ID_bool ||
3231  o_type0.id()==ID_c_bool)
3232  {
3234  if(op1.type().id()==ID_bool ||
3235  op1.type().id()==ID_c_bool ||
3236  op1.type().id()==ID_c_enum_tag ||
3237  op1.type().id()==ID_unsignedbv ||
3238  op1.type().id()==ID_signedbv)
3239  return;
3240  }
3241  else
3242  {
3243  implicit_typecast(op1, o_type0);
3244 
3245  if(is_number(op1.type()) ||
3246  op1.type().id()==ID_bool ||
3247  op1.type().id()==ID_c_bool ||
3248  op1.type().id()==ID_c_enum_tag)
3249  return;
3250  }
3251  }
3252 
3253  err_location(expr);
3254  error() << "assignment `" << statement
3255  << "' not defined for types `"
3256  << to_string(o_type0) << "' and `"
3257  << to_string(o_type1) << "'" << eom;
3258 
3259  throw 0;
3260 }
3261 
3263 {
3264  make_constant_rec(expr);
3265  simplify(expr, *this);
3266 
3267  if(!expr.is_constant() &&
3268  expr.id()!=ID_infinity)
3269  {
3271  error() << "expected constant expression, but got `"
3272  << to_string(expr) << "'" << eom;
3273  throw 0;
3274  }
3275 }
3276 
3278 {
3279  make_constant(expr);
3280  make_index_type(expr);
3281  simplify(expr, *this);
3282 
3283  if(!expr.is_constant() &&
3284  expr.id()!=ID_infinity)
3285  {
3287  error() << "conversion to integer constant failed" << eom;
3288  throw 0;
3289  }
3290 }
3291 
3293 {
3294 }
virtual void typecheck_expr_binary_boolean(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1083
The type of an expression.
Definition: type.h:20
mstreamt & warning()
Definition: message.h:228
irep_idt name
The unique identifier.
Definition: symbol.h:46
std::map< irep_idt, source_locationt > labels_used
mstreamt & result()
Definition: message.h:233
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
exprt & true_case()
Definition: std_expr.h:2805
typet void_type()
Definition: c_types.cpp:306
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
semantic type conversion
Definition: std_expr.h:1725
virtual void implicit_typecast_bool(exprt &expr)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
virtual bool is_complete_type(const typet &type) const
BigInt mp_integer
Definition: mp_arith.h:19
void typecheck_declaration(ansi_c_declarationt &)
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
asm_label_mapt asm_label_map
virtual void typecheck_expr_index(exprt &expr)
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
#define CPROVER_PREFIX
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
exprt simplify_expr(const exprt &src, const namespacet &ns)
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
std::vector< irept > subt
Definition: irep.h:91
virtual void make_constant(exprt &expr)
exprt & symbol()
Definition: std_code.h:205
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
bool has_ellipsis() const
Definition: std_types.h:803
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:43
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
const irep_idt & get_function() const
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const irep_idt & get_identifier() const
Definition: std_expr.h:120
std::vector< componentt > componentst
Definition: std_types.h:240
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2280
const irep_idt & get_value() const
Definition: std_expr.h:3702
std::vector< parametert > parameterst
Definition: std_types.h:829
const componentst & components() const
Definition: std_types.h:242
id_type_mapt parameter_map
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:60
unsignedbv_typet size_type()
Definition: c_types.cpp:57
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
A constant literal expression.
Definition: std_expr.h:3685
void make_bool(bool value)
Definition: expr.cpp:147
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:281
virtual std::string to_string(const exprt &expr)
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
bool is_static_lifetime
Definition: symbol.h:70
subt & get_sub()
Definition: irep.h:245
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
static ieee_float_spect double_precision()
Definition: ieee_float.h:69
symbol_tablet & symbol_table
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
equality
Definition: std_expr.h:1082
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
void follow_macros(exprt &expr) const
Definition: namespace.cpp:107
virtual void typecheck_expr_symbol(exprt &expr)
static bool is_numeric_type(const typet &src)
const irep_idt & id() const
Definition: irep.h:189
exprt c_sizeof(const typet &src, const namespacet &ns)
Definition: c_sizeof.cpp:303
An expression denoting infinity.
Definition: std_expr.h:3908
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
virtual void typecheck_expr_operands(exprt &expr)
ANSI-C Language Type Checking.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:717
ANSI-C Language Type Checking.
A declaration of a local variable.
Definition: std_code.h:192
virtual void typecheck_expr_member(exprt &expr)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
The NIL expression.
Definition: std_expr.h:3764
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
A constant-size array type.
Definition: std_types.h:1554
virtual void make_index_type(exprt &expr)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
union constructor from single element
Definition: std_expr.h:1389
API to expression classes.
exprt & op1()
Definition: expr.h:87
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
static ieee_float_spect single_precision()
Definition: ieee_float.h:63
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
const exprt & size() const
Definition: std_types.h:1568
exprt c_offsetof(const struct_typet &src, const irep_idt &component_name, const namespacet &ns)
Definition: c_sizeof.cpp:311
virtual void typecheck_expr(exprt &expr)
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:702
void err_location(const source_locationt &loc)
Definition: typecheck.h:27
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual void typecheck_expr_typecast(exprt &expr)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1319
bitvector_typet index_type()
Definition: c_types.cpp:15
#define Forall_irep(it, irep)
Definition: irep.h:66
std::list< codet > clean_code
codet & find_last_statement()
Definition: std_code.h:94
Operator to return the address of an object.
Definition: std_expr.h:2593
std::vector< typet > subtypest
Definition: type.h:54
exprt & false_case()
Definition: std_expr.h:2815
Various predicates over pointers in programs.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
virtual void typecheck_expr_function_identifier(exprt &expr)
bool is_constant() const
Definition: expr.cpp:128
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
binary multiplication
Definition: std_expr.h:806
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
Pointer Logic.
bitvector_typet long_double_type()
Definition: c_types.cpp:222
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
const irep_idt & display_name() const
Definition: symbol.h:60
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
A function call side effect.
Definition: std_code.h:1052
bool is_extern
Definition: symbol.h:71
Complex numbers made of pair of given subtype.
Definition: std_types.h:1606
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
virtual void typecheck_expr_sizeof(exprt &expr)
void follow_symbol(irept &irep) const
Definition: namespace.cpp:43
API to type classes.
bool is_KnR() const
Definition: std_types.h:814
const irep_idt & get_access() const
Definition: std_types.h:199
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
bool is_number(const typet &type)
Definition: type.cpp:24
exprt & index()
Definition: std_expr.h:1208
exprt & function()
Definition: std_code.h:677
void set_statement(const irep_idt &statement)
Definition: std_code.h:32
Base class for all expressions.
Definition: expr.h:46
The union type.
Definition: std_types.h:424
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
const parameterst & parameters() const
Definition: std_types.h:841
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
exprt pointer_offset(const exprt &pointer)
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
const source_locationt & source_location() const
Definition: expr.h:142
virtual void typecheck_expr_dereference(exprt &expr)
virtual void make_constant_index(exprt &expr)
irept & add(const irep_namet &name)
Definition: irep.cpp:306
exprt::operandst & arguments()
Definition: std_code.h:1071
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
mstreamt & error()
Definition: message.h:223
bool is_zero() const
Definition: expr.cpp:236
virtual bool gcc_types_compatible_p(const typet &, const typet &)
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
virtual void implicit_typecast_arithmetic(exprt &expr)
static void add_rounding_mode(exprt &)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:189
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
virtual void typecheck_type(typet &type)
int8_t s1
Definition: bytecode_info.h:59
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
Definition: std_expr.h:619
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
A statement in a programming language.
Definition: std_code.h:19
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:546
signedbv_typet signed_int_type()
Definition: c_types.cpp:29
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
void remove(const irep_namet &name)
Definition: irep.cpp:270
bool is_type
Definition: symbol.h:66
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
virtual void typecheck_expr_address_of(exprt &expr)
virtual void typecheck_expr_constant(exprt &expr)
virtual void make_constant_rec(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
An expression containing a side effect.
Definition: std_code.h:997
virtual void typecheck_expr_main(exprt &expr)
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
virtual void typecheck_expr_alignof(exprt &expr)
exprt same_object(const exprt &p1, const exprt &p2)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1589
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
A base class for shift operators.
Definition: std_expr.h:2227
const typet & return_type() const
Definition: std_types.h:831
bool is_macro
Definition: symbol.h:66
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
virtual void typecheck_expr_shifts(shift_exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
Definition: std_types.cpp:51
const irep_idt & get_statement() const
Definition: std_code.h:1012
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_code(codet &code)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
bool simplify(exprt &expr, const namespacet &ns)
A generic base class for expressions that are predicates, i.e., boolean-typed.
Definition: std_expr.h:400
bool is_lvalue
Definition: symbol.h:71
#define forall_irep(it, irep)
Definition: irep.h:62
array index operator
Definition: std_expr.h:1170
C Language Type Checking.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051
virtual void adjust_float_rel(exprt &expr)