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