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