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