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