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