cprover
Loading...
Searching...
No Matches
c_typecheck_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Language Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include <util/arith_tools.h>
13#include <util/bitvector_expr.h>
14#include <util/c_types.h>
15#include <util/config.h>
16#include <util/cprover_prefix.h>
17#include <util/expr_util.h>
18#include <util/floatbv_expr.h>
19#include <util/ieee_float.h>
22#include <util/pointer_expr.h>
25#include <util/prefix.h>
26#include <util/range.h>
27#include <util/simplify_expr.h>
29#include <util/suffix.h>
31
33
34#include "anonymous_member.h"
35#include "ansi_c_declaration.h"
36#include "builtin_factory.h"
37#include "c_expr.h"
38#include "c_qualifiers.h"
39#include "c_typecast.h"
40#include "c_typecheck_base.h"
41#include "expr2c.h"
42#include "padding.h"
43#include "type2name.h"
44
45#include <sstream>
46
48{
49 if(expr.id()==ID_already_typechecked)
50 {
51 expr.swap(to_already_typechecked_expr(expr).get_expr());
52 return;
53 }
54
55 // first do sub-nodes
57
58 // now do case-split
60}
61
63{
64 for(auto &op : expr.operands())
66
67 if(expr.id()==ID_div ||
68 expr.id()==ID_mult ||
69 expr.id()==ID_plus ||
70 expr.id()==ID_minus)
71 {
72 if(expr.type().id()==ID_floatbv &&
73 expr.operands().size()==2)
74 {
75 // The rounding mode to be used at compile time is non-obvious.
76 // We'll simply use round to even (0), which is suggested
77 // by Sec. F.7.2 Translation, ISO-9899:1999.
78 expr.operands().resize(3);
79
80 if(expr.id()==ID_div)
81 expr.id(ID_floatbv_div);
82 else if(expr.id()==ID_mult)
83 expr.id(ID_floatbv_mult);
84 else if(expr.id()==ID_plus)
85 expr.id(ID_floatbv_plus);
86 else if(expr.id()==ID_minus)
87 expr.id(ID_floatbv_minus);
88 else
90
91 to_ieee_float_op_expr(expr).rounding_mode() =
93 }
94 }
95}
96
98 const typet &type1,
99 const typet &type2)
100{
101 // read
102 // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
103
104 // check qualifiers first
106 return false;
107
108 if(type1.id()==ID_c_enum_tag)
110 else if(type2.id()==ID_c_enum_tag)
112
113 if(type1.id()==ID_c_enum)
114 {
115 if(type2.id()==ID_c_enum) // both are enums
116 return type1==type2; // compares the tag
117 else if(type2 == to_c_enum_type(type1).underlying_type())
118 return true;
119 }
120 else if(type2.id()==ID_c_enum)
121 {
122 if(type1 == to_c_enum_type(type2).underlying_type())
123 return true;
124 }
125 else if(type1.id()==ID_pointer &&
126 type2.id()==ID_pointer)
127 {
129 to_pointer_type(type1).base_type(), to_pointer_type(type2).base_type());
130 }
131 else if(type1.id()==ID_array &&
132 type2.id()==ID_array)
133 {
135 to_array_type(type1).element_type(),
136 to_array_type(type2).element_type()); // ignore size
137 }
138 else if(type1.id()==ID_code &&
139 type2.id()==ID_code)
140 {
143
145 c_type1.return_type(),
146 c_type2.return_type()))
147 return false;
148
149 if(c_type1.parameters().size()!=c_type2.parameters().size())
150 return false;
151
152 for(std::size_t i=0; i<c_type1.parameters().size(); i++)
154 c_type1.parameters()[i].type(),
155 c_type2.parameters()[i].type()))
156 return false;
157
158 return true;
159 }
160 else
161 {
162 if(type1==type2)
163 {
164 // Need to distinguish e.g. long int from int or
165 // long long int from long int.
166 // The rules appear to match those of C++.
167
168 if(type1.get(ID_C_c_type)==type2.get(ID_C_c_type))
169 return true;
170 }
171 }
172
173 return false;
174}
175
177{
178 if(expr.id()==ID_side_effect)
180 else if(expr.is_constant())
182 else if(expr.id()==ID_infinity)
183 {
184 // ignore
185 }
186 else if(expr.id()==ID_symbol)
188 else if(expr.id()==ID_unary_plus ||
189 expr.id()==ID_unary_minus ||
190 expr.id()==ID_bitnot)
192 else if(expr.id()==ID_not)
194 else if(
195 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies ||
196 expr.id() == ID_xor)
198 else if(expr.id()==ID_address_of)
200 else if(expr.id()==ID_dereference)
202 else if(expr.id()==ID_member)
204 else if(expr.id()==ID_ptrmember)
206 else if(expr.id()==ID_equal ||
207 expr.id()==ID_notequal ||
208 expr.id()==ID_lt ||
209 expr.id()==ID_le ||
210 expr.id()==ID_gt ||
211 expr.id()==ID_ge)
213 else if(expr.id()==ID_index)
215 else if(expr.id()==ID_typecast)
217 else if(expr.id()==ID_sizeof)
219 else if(expr.id()==ID_alignof)
221 else if(
222 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
223 expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitand ||
224 expr.id() == ID_bitxor || expr.id() == ID_bitor || expr.id() == ID_bitnand)
225 {
227 }
228 else if(expr.id()==ID_shl || expr.id()==ID_shr)
230 else if(expr.id()==ID_comma)
232 else if(expr.id()==ID_if)
234 else if(expr.id()==ID_code)
235 {
237 error() << "typecheck_expr_main got code: " << expr.pretty() << eom;
238 throw 0;
239 }
240 else if(expr.id()==ID_gcc_builtin_va_arg)
242 else if(expr.id()==ID_cw_va_arg_typeof)
245 {
246 expr.type()=bool_typet();
247 auto &subtypes =
248 (static_cast<type_with_subtypest &>(expr.add(ID_type_arg))).subtypes();
249 PRECONDITION(subtypes.size() == 2);
250 typecheck_type(subtypes[0]);
251 typecheck_type(subtypes[1]);
252 source_locationt source_location=expr.source_location();
253
254 // ignores top-level qualifiers
255 subtypes[0].remove(ID_C_constant);
256 subtypes[0].remove(ID_C_volatile);
257 subtypes[0].remove(ID_C_restricted);
258 subtypes[1].remove(ID_C_constant);
259 subtypes[1].remove(ID_C_volatile);
260 subtypes[1].remove(ID_C_restricted);
261
262 expr = make_boolean_expr(gcc_types_compatible_p(subtypes[0], subtypes[1]));
263 expr.add_source_location()=source_location;
264 }
265 else if(expr.id()==ID_clang_builtin_convertvector)
266 {
267 // This has one operand and a type, and acts like a typecast
268 DATA_INVARIANT(expr.operands().size()==1, "clang_builtin_convertvector has one operand");
269 typecheck_type(expr.type());
270 typecast_exprt tmp(to_unary_expr(expr).op(), expr.type());
271 tmp.add_source_location()=expr.source_location();
272 expr.swap(tmp);
273 }
274 else if(expr.id()==ID_builtin_offsetof)
276 else if(expr.id()==ID_string_constant)
277 {
278 // already fine -- mark as lvalue
279 expr.set(ID_C_lvalue, true);
280 }
281 else if(expr.id()==ID_arguments)
282 {
283 // already fine
284 }
285 else if(expr.id()==ID_designated_initializer)
286 {
287 exprt &designator=static_cast<exprt &>(expr.add(ID_designator));
288
289 Forall_operands(it, designator)
290 {
291 if(it->id()==ID_index)
292 typecheck_expr(to_unary_expr(*it).op()); // still needs typechecking
293 }
294 }
295 else if(expr.id()==ID_initializer_list)
296 {
297 // already fine, just set some type
298 expr.type()=void_type();
299 }
300 else if(
301 expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda)
302 {
303 // These have two operands.
304 // op0 is a tuple with declarations,
305 // op1 is the bound expression
306 auto &binary_expr = to_binary_expr(expr);
307 auto &bindings = binary_expr.op0().operands();
308 auto &where = binary_expr.op1();
309
310 for(const auto &binding : bindings)
311 {
312 if(binding.get(ID_statement) != ID_decl)
313 {
315 error() << "expected declaration as operand of quantifier" << eom;
316 throw 0;
317 }
318 }
319
320 if(has_subexpr(where, ID_side_effect))
321 {
323 error() << "quantifier must not contain side effects" << eom;
324 throw 0;
325 }
326
327 // replace declarations by symbol expressions
328 for(auto &binding : bindings)
329 binding = to_code_frontend_decl(to_code(binding)).symbol();
330
331 if(expr.id() == ID_lambda)
332 {
334
335 for(auto &binding : bindings)
336 domain.push_back(binding.type());
337
338 expr.type() = mathematical_function_typet(domain, where.type());
339 }
340 else
341 {
342 expr.type() = bool_typet();
344 }
345 }
346 else if(expr.id()==ID_label)
347 {
348 expr.type()=void_type();
349 }
350 else if(expr.id()==ID_array)
351 {
352 // these pop up as string constants, and are already typed
353 }
354 else if(expr.id()==ID_complex)
355 {
356 // these should only exist as constants,
357 // and should already be typed
358 }
359 else if(expr.id() == ID_complex_real)
360 {
361 const exprt &op = to_unary_expr(expr).op();
362
363 if(op.type().id() != ID_complex)
364 {
365 if(!is_number(op.type()))
366 {
368 error() << "real part retrieval expects numerical operand, "
369 << "but got '" << to_string(op.type()) << "'" << eom;
370 throw 0;
371 }
372
375
377 }
378 else
379 {
381
382 // these are lvalues if the operand is one
383 if(op.get_bool(ID_C_lvalue))
385
386 if(op.type().get_bool(ID_C_constant))
387 complex_real_expr.type().set(ID_C_constant, true);
388
390 }
391 }
392 else if(expr.id() == ID_complex_imag)
393 {
394 const exprt &op = to_unary_expr(expr).op();
395
396 if(op.type().id() != ID_complex)
397 {
398 if(!is_number(op.type()))
399 {
401 error() << "real part retrieval expects numerical operand, "
402 << "but got '" << to_string(op.type()) << "'" << eom;
403 throw 0;
404 }
405
408
410 }
411 else
412 {
414
415 // these are lvalues if the operand is one
416 if(op.get_bool(ID_C_lvalue))
418
419 if(op.type().get_bool(ID_C_constant))
420 complex_imag_expr.type().set(ID_C_constant, true);
421
423 }
424 }
425 else if(expr.id()==ID_generic_selection)
426 {
427 // This is C11.
428 // The operand is already typechecked. Depending
429 // on its type, we return one of the generic associations.
430 auto &op = to_unary_expr(expr).op();
431
432 // This is one of the few places where it's detectable
433 // that we are using "bool" for boolean operators instead
434 // of "int". We convert for this reason.
435 if(op.is_boolean())
437
440
441 // first typecheck all types
442 for(auto &irep : generic_associations)
443 {
444 if(irep.get(ID_type_arg) != ID_default)
445 {
446 typet &type = static_cast<typet &>(irep.add(ID_type_arg));
447 typecheck_type(type);
448 }
449 }
450
451 // first try non-default match
454
455 const typet &op_type = follow(op.type());
456
457 for(const auto &irep : generic_associations)
458 {
459 if(irep.get(ID_type_arg) == ID_default)
460 default_match = static_cast<const exprt &>(irep.find(ID_value));
461 else if(
462 op_type == follow(static_cast<const typet &>(irep.find(ID_type_arg))))
463 {
464 assoc_match = static_cast<const exprt &>(irep.find(ID_value));
465 }
466 }
467
468 if(assoc_match.is_nil())
469 {
470 if(default_match.is_not_nil())
471 expr.swap(default_match);
472 else
473 {
475 error() << "unmatched generic selection: " << to_string(op.type())
476 << eom;
477 throw 0;
478 }
479 }
480 else
481 expr.swap(assoc_match);
482
483 // still need to typecheck the result
484 typecheck_expr(expr);
485 }
486 else if(expr.id()==ID_gcc_asm_input ||
487 expr.id()==ID_gcc_asm_output ||
489 {
490 }
491 else if(expr.id()==ID_lshr || expr.id()==ID_ashr ||
492 expr.id()==ID_assign_lshr || expr.id()==ID_assign_ashr)
493 {
494 // already type checked
495 }
496 else if(
497 expr.id() == ID_C_spec_assigns || expr.id() == ID_C_spec_frees ||
498 expr.id() == ID_target_list)
499 {
500 // already type checked
501 }
502 else
503 {
505 error() << "unexpected expression: " << expr.pretty() << eom;
506 throw 0;
507 }
508}
509
511{
512 expr.type() = to_binary_expr(expr).op1().type();
513
514 // make this an l-value if the last operand is one
515 if(to_binary_expr(expr).op1().get_bool(ID_C_lvalue))
516 expr.set(ID_C_lvalue, true);
517}
518
520{
521 // The first parameter is the va_list, and the second
522 // is the type, which will need to be fixed and checked.
523 // The type is given by the parser as type of the expression.
524
525 typet arg_type=expr.type();
527
528 const code_typet new_type(
530
531 exprt arg = to_unary_expr(expr).op();
532
534
536 function.add_source_location() = expr.source_location();
537
538 // turn into function call
540 function, {arg}, new_type.return_type(), expr.source_location());
541
542 expr.swap(result);
543
544 // Make sure symbol exists, but we have it return void
545 // to avoid collisions of the same symbol with different
546 // types.
547
549 symbol_type.return_type()=void_type();
550
552 symbol.base_name=ID_gcc_builtin_va_arg;
553
554 symbol_table.insert(std::move(symbol));
555}
556
558{
559 // used in Code Warrior via
560 //
561 // __va_arg( <Symbol>, _var_arg_typeof( <Typ> ) )
562 //
563 // where __va_arg is declared as
564 //
565 // extern void* __va_arg(void*, int);
566
567 typet &type=static_cast<typet &>(expr.add(ID_type_arg));
568 typecheck_type(type);
569
570 // these return an integer
571 expr.type()=signed_int_type();
572}
573
575{
576 // these need not be constant, due to array indices!
577
578 if(!expr.operands().empty())
579 {
581 error() << "builtin_offsetof expects no operands" << eom;
582 throw 0;
583 }
584
585 typet &type=static_cast<typet &>(expr.add(ID_type_arg));
586 typecheck_type(type);
587
588 const exprt &member = static_cast<const exprt &>(expr.add(ID_designator));
589
591
592 for(const auto &op : member.operands())
593 {
594 type = follow(type);
595
596 if(op.id() == ID_member)
597 {
598 if(type.id()!=ID_union && type.id()!=ID_struct)
599 {
601 error() << "offsetof of member expects struct/union type, "
602 << "but got '" << to_string(type) << "'" << eom;
603 throw 0;
604 }
605
606 bool found=false;
607 irep_idt component_name = op.get(ID_component_name);
608
609 while(!found)
610 {
611 PRECONDITION(type.id() == ID_union || type.id() == ID_struct);
612
615
616 // direct member?
617 if(struct_union_type.has_component(component_name))
618 {
619 found=true;
620
621 if(type.id()==ID_struct)
622 {
623 auto o_opt =
624 member_offset_expr(to_struct_type(type), component_name, *this);
625
626 if(!o_opt.has_value())
627 {
629 error() << "offsetof failed to determine offset of '"
630 << component_name << "'" << eom;
631 throw 0;
632 }
633
635 result,
637 }
638
639 type=struct_union_type.get_component(component_name).type();
640 }
641 else
642 {
643 // maybe anonymous?
644 bool found2=false;
645
646 for(const auto &c : struct_union_type.components())
647 {
648 if(
649 c.get_anonymous() &&
650 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
651 {
652 if(has_component_rec(c.type(), component_name, *this))
653 {
654 if(type.id()==ID_struct)
655 {
657 to_struct_type(type), c.get_name(), *this);
658
659 if(!o_opt.has_value())
660 {
662 error() << "offsetof failed to determine offset of '"
663 << component_name << "'" << eom;
664 throw 0;
665 }
666
668 result,
670 o_opt.value(), size_type()));
671 }
672
673 typet tmp = follow(c.type());
674 type=tmp;
675 CHECK_RETURN(type.id() == ID_union || type.id() == ID_struct);
676 found2=true;
677 break; // we run into another iteration of the outer loop
678 }
679 }
680 }
681
682 if(!found2)
683 {
685 error() << "offset-of of member failed to find component '"
686 << component_name << "' in '" << to_string(type) << "'"
687 << eom;
688 throw 0;
689 }
690 }
691 }
692 }
693 else if(op.id() == ID_index)
694 {
695 if(type.id()!=ID_array)
696 {
698 error() << "offsetof of index expects array type" << eom;
699 throw 0;
700 }
701
702 exprt index = to_unary_expr(op).op();
703
704 // still need to typecheck index
705 typecheck_expr(index);
706
707 auto element_size_opt =
708 size_of_expr(to_array_type(type).element_type(), *this);
709
710 if(!element_size_opt.has_value())
711 {
713 error() << "offsetof failed to determine array element size" << eom;
714 throw 0;
715 }
716
718
720
721 typet tmp = to_array_type(type).element_type();
722 type=tmp;
723 }
724 }
725
726 // We make an effort to produce a constant,
727 // but this may depend on variables
728 simplify(result, *this);
729 result.add_source_location()=expr.source_location();
730
731 expr.swap(result);
732}
733
735{
736 if(expr.id()==ID_side_effect &&
738 {
739 // don't do function operand
740 typecheck_expr(to_binary_expr(expr).op1()); // arguments
741 }
742 else if(expr.id()==ID_side_effect &&
744 {
746 }
747 else if(
748 expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda)
749 {
750 // These introduce new symbols, which need to be added to the symbol table
751 // before the second operand is typechecked.
752
753 auto &binary_expr = to_binary_expr(expr);
754 auto &bindings = binary_expr.op0().operands();
755
756 for(auto &binding : bindings)
757 {
758 ansi_c_declarationt &declaration = to_ansi_c_declaration(binding);
759
760 typecheck_declaration(declaration);
761
762 if(declaration.declarators().size() != 1)
763 {
765 error() << "forall/exists expects one declarator exactly" << eom;
766 throw 0;
767 }
768
769 irep_idt identifier = declaration.declarators().front().get_name();
770
771 // look it up
772 symbol_table_baset::symbolst::const_iterator s_it =
773 symbol_table.symbols.find(identifier);
774
775 if(s_it == symbol_table.symbols.end())
776 {
778 error() << "failed to find bound symbol `" << identifier
779 << "' in symbol table" << eom;
780 throw 0;
781 }
782
783 const symbolt &symbol = s_it->second;
784
785 if(
786 symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
787 !is_complete_type(symbol.type) || symbol.type.id() == ID_code)
788 {
790 error() << "unexpected quantified symbol" << eom;
791 throw 0;
792 }
793
794 code_frontend_declt decl(symbol.symbol_expr());
795 decl.add_source_location() = declaration.source_location();
796
797 binding = decl;
798 }
799
801 }
802 else
803 {
804 Forall_operands(it, expr)
805 typecheck_expr(*it);
806 }
807}
808
810{
811 irep_idt identifier=to_symbol_expr(expr).get_identifier();
812
813 // Is it a parameter? We do this while checking parameter lists.
814 id_type_mapt::const_iterator p_it=parameter_map.find(identifier);
815 if(p_it!=parameter_map.end())
816 {
817 // yes
818 expr.type()=p_it->second;
819 expr.set(ID_C_lvalue, true);
820 return;
821 }
822
823 // renaming via GCC asm label
824 asm_label_mapt::const_iterator entry=
825 asm_label_map.find(identifier);
826 if(entry!=asm_label_map.end())
827 {
828 identifier=entry->second;
829 to_symbol_expr(expr).set_identifier(identifier);
830 }
831
832 // look it up
833 const symbolt *symbol_ptr;
834 if(lookup(identifier, symbol_ptr))
835 {
837 error() << "failed to find symbol '" << identifier << "'" << eom;
838 throw 0;
839 }
840
841 const symbolt &symbol=*symbol_ptr;
842
843 if(symbol.is_type)
844 {
846 error() << "did not expect a type symbol here, but got '"
847 << symbol.display_name() << "'" << eom;
848 throw 0;
849 }
850
851 // save the source location
852 source_locationt source_location=expr.source_location();
853
854 if(symbol.is_macro)
855 {
856 // preserve enum key
857 #if 0
858 irep_idt base_name=expr.get(ID_C_base_name);
859 #endif
860
861 follow_macros(expr);
862
863 #if 0
864 if(expr.is_constant() && !base_name.empty())
865 expr.set(ID_C_cformat, base_name);
866 else
867 #endif
868 typecheck_expr(expr);
869
870 // preserve location
871 expr.add_source_location()=source_location;
872 }
873 else if(has_prefix(id2string(identifier), CPROVER_PREFIX "constant_infinity"))
874 {
875 expr=infinity_exprt(symbol.type);
876
877 // put it back
878 expr.add_source_location()=source_location;
879 }
880 else if(identifier=="__func__" ||
881 identifier=="__FUNCTION__" ||
882 identifier=="__PRETTY_FUNCTION__")
883 {
884 // __func__ is an ANSI-C standard compliant hack to get the function name
885 // __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
886 string_constantt s(source_location.get_function());
887 s.add_source_location()=source_location;
888 s.set(ID_C_lvalue, true);
889 expr.swap(s);
890 }
891 else
892 {
893 expr=symbol.symbol_expr();
894
895 // put it back
896 expr.add_source_location()=source_location;
897
898 if(symbol.is_lvalue)
899 expr.set(ID_C_lvalue, true);
900
901 if(expr.type().id()==ID_code) // function designator
902 { // special case: this is sugar for &f
903 address_of_exprt tmp(expr, pointer_type(expr.type()));
904 tmp.set(ID_C_implicit, true);
905 tmp.add_source_location()=expr.source_location();
906 expr=tmp;
907 }
908 }
909}
910
912 side_effect_exprt &expr)
913{
914 codet &code = to_code(to_unary_expr(expr).op());
915
916 // the type is the type of the last statement in the
917 // block, but do worry about labels!
918
919 codet &last=to_code_block(code).find_last_statement();
920
921 irep_idt last_statement=last.get_statement();
922
923 if(last_statement==ID_expression)
924 {
925 PRECONDITION(last.operands().size() == 1);
926 exprt &op=last.op0();
927
928 // arrays here turn into pointers (array decay)
929 if(op.type().id()==ID_array)
931 op, pointer_type(to_array_type(op.type()).element_type()));
932
933 expr.type()=op.type();
934 }
935 else
936 {
937 // we used to do this, but don't expect it any longer
938 PRECONDITION(last_statement != ID_function_call);
939
940 expr.type()=typet(ID_empty);
941 }
942}
943
945{
946 typet type;
947
948 // these come in two flavors: with zero operands, for a type,
949 // and with one operand, for an expression.
950 PRECONDITION(expr.operands().size() <= 1);
951
952 if(expr.operands().empty())
953 {
954 type.swap(static_cast<typet &>(expr.add(ID_type_arg)));
955 typecheck_type(type);
956 }
957 else
958 {
959 const exprt &op = to_unary_expr(as_const(expr)).op();
960 // This is one of the few places where it's detectable
961 // that we are using "bool" for boolean operators instead
962 // of "int". We convert for this reason.
963 if(op.is_boolean())
964 type = signed_int_type();
965 else
966 type = op.type();
967 }
968
970
971 if(type.id()==ID_c_bit_field)
972 {
974 error() << "sizeof cannot be applied to bit fields" << eom;
975 throw 0;
976 }
977 else if(type.id() == ID_bool)
978 {
980 error() << "sizeof cannot be applied to single bits" << eom;
981 throw 0;
982 }
983 else if(type.id() == ID_empty)
984 {
985 // This is a gcc extension.
986 // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
988 }
989 else
990 {
991 if(
992 (type.id() == ID_struct_tag &&
993 follow_tag(to_struct_tag_type(type)).is_incomplete()) ||
994 (type.id() == ID_union_tag &&
995 follow_tag(to_union_tag_type(type)).is_incomplete()) ||
996 (type.id() == ID_c_enum_tag &&
997 follow_tag(to_c_enum_tag_type(type)).is_incomplete()) ||
998 (type.id() == ID_array && to_array_type(type).is_incomplete()))
999 {
1001 error() << "invalid application of \'sizeof\' to an incomplete type\n\t\'"
1002 << to_string(type) << "\'" << eom;
1003 throw 0;
1004 }
1005
1006 auto size_of_opt = size_of_expr(type, *this);
1007
1008 if(!size_of_opt.has_value())
1009 {
1011 error() << "type has no size: " << to_string(type) << eom;
1012 throw 0;
1013 }
1014
1015 new_expr = size_of_opt.value();
1016 }
1017
1018 new_expr.swap(expr);
1019
1020 expr.add(ID_C_c_sizeof_type)=type;
1021
1022 // The type may contain side-effects.
1023 if(!clean_code.empty())
1024 {
1028 decl_block.set_statement(ID_decl_block);
1029 side_effect_expr.copy_to_operands(decl_block);
1030 clean_code.clear();
1031
1032 // We merge the side-effect into the operand of the typecast,
1033 // using a comma-expression.
1034 // I.e., (type)e becomes (type)(side-effect, e)
1035 // It is not obvious whether the type or 'e' should be evaluated
1036 // first.
1037
1039 std::move(side_effect_expr), ID_comma, expr, expr.type()};
1040 expr.swap(comma_expr);
1041 }
1042}
1043
1045{
1047
1048 if(expr.operands().size()==1)
1049 argument_type = to_unary_expr(expr).op().type();
1050 else
1051 {
1052 typet &op_type=static_cast<typet &>(expr.add(ID_type_arg));
1055 }
1056
1057 // we only care about the type
1059
1061 tmp.add_source_location()=expr.source_location();
1062
1063 expr.swap(tmp);
1064}
1065
1067{
1068 exprt &op = to_unary_expr(expr).op();
1069
1070 typecheck_type(expr.type());
1071
1072 // The type may contain side-effects.
1073 if(!clean_code.empty())
1074 {
1078 decl_block.set_statement(ID_decl_block);
1079 side_effect_expr.copy_to_operands(decl_block);
1080 clean_code.clear();
1081
1082 // We merge the side-effect into the operand of the typecast,
1083 // using a comma-expression.
1084 // I.e., (type)e becomes (type)(side-effect, e)
1085 // It is not obvious whether the type or 'e' should be evaluated
1086 // first.
1087
1089 std::move(side_effect_expr), ID_comma, op, op.type()};
1090 op.swap(comma_expr);
1091 }
1092
1093 const typet expr_type = expr.type();
1094
1095 if(
1096 expr_type.id() == ID_union_tag && expr_type != op.type() &&
1097 op.id() != ID_initializer_list)
1098 {
1099 // This is a GCC extension. It's either a 'temporary union',
1100 // where the argument is one of the member types.
1101
1102 // This is one of the few places where it's detectable
1103 // that we are using "bool" for boolean operators instead
1104 // of "int". We convert for this reason.
1105 if(op.is_boolean())
1106 op = typecast_exprt(op, signed_int_type());
1107
1108 // we need to find a member with the right type
1110 for(const auto &c : union_type.components())
1111 {
1112 if(c.type() == op.type())
1113 {
1114 // found! build union constructor
1115 union_exprt union_expr(c.get_name(), op, expr.type());
1116 union_expr.add_source_location()=expr.source_location();
1117 expr=union_expr;
1118 expr.set(ID_C_lvalue, true);
1119 return;
1120 }
1121 }
1122
1123 // not found, complain
1125 error() << "type cast to union: type '" << to_string(op.type())
1126 << "' not found in union" << eom;
1127 throw 0;
1128 }
1129
1130 // We allow (TYPE){ initializer_list }
1131 // This is called "compound literal", and is syntactic
1132 // sugar for a (possibly local) declaration.
1133 if(op.id()==ID_initializer_list)
1134 {
1135 // just do a normal initialization
1136 do_initializer(op, expr.type(), false);
1137
1138 // This produces a struct-expression,
1139 // union-expression, array-expression,
1140 // or an expression for a pointer or scalar.
1141 // We produce a compound_literal expression.
1143 tmp.copy_to_operands(op);
1144
1145 // handle the case of TYPE being an array with unspecified size
1146 if(op.id()==ID_array &&
1147 expr.type().id()==ID_array &&
1148 to_array_type(expr.type()).size().is_nil())
1149 tmp.type()=op.type();
1150
1151 expr=tmp;
1152 expr.set(ID_C_lvalue, true); // these are l-values
1153 return;
1154 }
1155
1156 // a cast to void is always fine
1157 if(expr_type.id()==ID_empty)
1158 return;
1159
1160 const typet op_type = op.type();
1161
1162 // cast to same type?
1163 if(expr_type == op_type)
1164 return; // it's ok
1165
1166 // vectors?
1167
1168 if(expr_type.id()==ID_vector)
1169 {
1170 // we are generous -- any vector to vector is fine
1171 if(op_type.id()==ID_vector)
1172 return;
1173 else if(op_type.id()==ID_signedbv ||
1174 op_type.id()==ID_unsignedbv)
1175 return;
1176 }
1177
1179 {
1181 error() << "type cast to '" << to_string(expr_type) << "' is not permitted"
1182 << eom;
1183 throw 0;
1184 }
1185
1187 {
1188 }
1189 else if(op_type.id()==ID_array)
1190 {
1191 // This is the promotion from an array
1192 // to a pointer to the first element.
1194 if(error_opt.has_value())
1196
1197 index_exprt index(op, from_integer(0, c_index_type()));
1198 op=address_of_exprt(index);
1199 }
1200 else if(op_type.id()==ID_empty)
1201 {
1202 if(expr_type.id()!=ID_empty)
1203 {
1205 error() << "type cast from void only permitted to void, but got '"
1206 << to_string(expr.type()) << "'" << eom;
1207 throw 0;
1208 }
1209 }
1210 else if(op_type.id()==ID_vector)
1211 {
1214
1215 // gcc allows conversion of a vector of size 1 to
1216 // an integer/float of the same size
1217 if((expr_type.id()==ID_signedbv ||
1218 expr_type.id()==ID_unsignedbv) &&
1221 {
1222 }
1223 else
1224 {
1226 error() << "type cast from vector to '" << to_string(expr.type())
1227 << "' not permitted" << eom;
1228 throw 0;
1229 }
1230 }
1231 else
1232 {
1234 error() << "type cast from '" << to_string(op_type) << "' not permitted"
1235 << eom;
1236 throw 0;
1237 }
1238
1239 // The new thing is an lvalue if the previous one is
1240 // an lvalue and it's just a pointer type cast.
1241 // This isn't really standard conformant!
1242 // Note that gcc says "warning: target of assignment not really an lvalue;
1243 // this will be a hard error in the future", i.e., we
1244 // can hope that the code below will one day simply go away.
1245
1246 // Current versions of gcc in fact refuse to do this! Yay!
1247
1248 if(op.get_bool(ID_C_lvalue))
1249 {
1250 if(expr_type.id()==ID_pointer)
1251 expr.set(ID_C_lvalue, true);
1252 }
1253}
1254
1259
1261{
1262 exprt &array_expr = to_binary_expr(expr).op0();
1263 exprt &index_expr = to_binary_expr(expr).op1();
1264
1265 // we might have to swap them
1266
1267 {
1268 const typet &array_type = array_expr.type();
1269 const typet &index_type = index_expr.type();
1270
1271 if(
1272 array_type.id() != ID_array && array_type.id() != ID_pointer &&
1273 array_type.id() != ID_vector &&
1274 (index_type.id() == ID_array || index_type.id() == ID_pointer ||
1275 index_type.id() == ID_vector))
1276 std::swap(array_expr, index_expr);
1277 }
1278
1280
1281 // array_expr is a reference to one of expr.operands(), when that vector is
1282 // swapped below the reference is no longer valid. final_array_type exists
1283 // beyond that point so can't be a reference
1284 const typet final_array_type = array_expr.type();
1285
1286 if(final_array_type.id()==ID_array ||
1288 {
1289 expr.type() = to_type_with_subtype(final_array_type).subtype();
1290
1291 if(array_expr.get_bool(ID_C_lvalue))
1292 expr.set(ID_C_lvalue, true);
1293
1294 if(final_array_type.get_bool(ID_C_constant))
1295 expr.type().set(ID_C_constant, true);
1296 }
1297 else if(final_array_type.id()==ID_pointer)
1298 {
1299 // p[i] is syntactic sugar for *(p+i)
1300
1303 std::swap(summands, expr.operands());
1304 expr.add_to_operands(plus_exprt(std::move(summands), array_expr.type()));
1305 expr.id(ID_dereference);
1306 expr.set(ID_C_lvalue, true);
1307 expr.type() = to_pointer_type(final_array_type).base_type();
1308 }
1309 else
1310 {
1312 error() << "operator [] must take array/vector or pointer but got '"
1313 << to_string(array_expr.type()) << "'" << eom;
1314 throw 0;
1315 }
1316}
1317
1319{
1320 // equality and disequality on float is not mathematical equality!
1321 if(expr.op0().type().id() == ID_floatbv)
1322 {
1323 if(expr.id()==ID_equal)
1324 expr.id(ID_ieee_float_equal);
1325 else if(expr.id()==ID_notequal)
1327 }
1328}
1329
1332{
1333 exprt &op0=expr.op0();
1334 exprt &op1=expr.op1();
1335
1336 const typet o_type0=op0.type();
1337 const typet o_type1=op1.type();
1338
1339 if(o_type0.id() == ID_vector || o_type1.id() == ID_vector)
1340 {
1342 return;
1343 }
1344
1345 expr.type()=bool_typet();
1346
1347 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1348 {
1350 {
1351 if(o_type0.id() != ID_array)
1352 {
1353 adjust_float_rel(expr);
1354 return; // no promotion necessary
1355 }
1356 }
1357 }
1358
1360
1361 const typet &type0=op0.type();
1362 const typet &type1=op1.type();
1363
1364 if(type0==type1)
1365 {
1366 if(is_number(type0))
1367 {
1368 adjust_float_rel(expr);
1369 return;
1370 }
1371
1372 if(type0.id()==ID_pointer)
1373 {
1374 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1375 return;
1376
1377 if(expr.id()==ID_le || expr.id()==ID_lt ||
1378 expr.id()==ID_ge || expr.id()==ID_gt)
1379 return;
1380 }
1381
1382 if(type0.id()==ID_string_constant)
1383 {
1384 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1385 return;
1386 }
1387 }
1388 else
1389 {
1390 // pointer and zero
1391 if(type0.id()==ID_pointer &&
1392 simplify_expr(op1, *this).is_zero())
1393 {
1395 return;
1396 }
1397
1398 if(type1.id()==ID_pointer &&
1399 simplify_expr(op0, *this).is_zero())
1400 {
1402 return;
1403 }
1404
1405 // pointer and integer
1406 if(type0.id()==ID_pointer && is_number(type1))
1407 {
1408 op1 = typecast_exprt(op1, type0);
1409 return;
1410 }
1411
1412 if(type1.id()==ID_pointer && is_number(type0))
1413 {
1414 op0 = typecast_exprt(op0, type1);
1415 return;
1416 }
1417
1418 if(type0.id()==ID_pointer && type1.id()==ID_pointer)
1419 {
1420 op1 = typecast_exprt(op1, type0);
1421 return;
1422 }
1423 }
1424
1426 error() << "operator '" << expr.id() << "' not defined for types '"
1427 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
1428 << eom;
1429 throw 0;
1430}
1431
1433{
1434 const typet &o_type0 = as_const(expr).op0().type();
1435 const typet &o_type1 = as_const(expr).op1().type();
1436
1437 if(o_type0.id() != ID_vector || o_type0 != o_type1)
1438 {
1440 error() << "vector operator '" << expr.id() << "' not defined for types '"
1441 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
1442 << eom;
1443 throw 0;
1444 }
1445
1446 // Comparisons between vectors produce a vector of integers of the same width
1447 // with the same dimension.
1448 auto subtype_width =
1449 to_bitvector_type(to_vector_type(o_type0).element_type()).get_width();
1450 expr.type() = vector_typet{
1451 to_vector_type(o_type0).index_type(),
1453 to_vector_type(o_type0).size()};
1454
1455 // Replace the id as the semantics of these are point-wise application (and
1456 // the result is not of bool type).
1457 if(expr.id() == ID_notequal)
1458 expr.id(ID_vector_notequal);
1459 else
1460 expr.id("vector-" + id2string(expr.id()));
1461}
1462
1464{
1465 auto &op = to_unary_expr(expr).op();
1466 const typet &op0_type = op.type();
1467
1468 if(op0_type.id() == ID_array)
1469 {
1470 // a->f is the same as a[0].f
1471 exprt zero = from_integer(0, c_index_type());
1472 index_exprt index_expr(op, zero, to_array_type(op0_type).element_type());
1473 index_expr.set(ID_C_lvalue, true);
1474 op.swap(index_expr);
1475 }
1476 else if(op0_type.id() == ID_pointer)
1477 {
1478 // turn x->y into (*x).y
1482 op.swap(deref_expr);
1483 }
1484 else
1485 {
1487 error() << "ptrmember operator requires pointer or array type "
1488 "on left hand side, but got '"
1489 << to_string(op0_type) << "'" << eom;
1490 throw 0;
1491 }
1492
1493 expr.id(ID_member);
1495}
1496
1498{
1499 exprt &op0 = to_unary_expr(expr).op();
1500 typet type=op0.type();
1501
1502 type = follow(type);
1503
1504 if(type.id()!=ID_struct &&
1505 type.id()!=ID_union)
1506 {
1508 error() << "member operator requires structure type "
1509 "on left hand side but got '"
1510 << to_string(type) << "'" << eom;
1511 throw 0;
1512 }
1513
1516
1517 if(struct_union_type.is_incomplete())
1518 {
1520 error() << "member operator got incomplete " << type.id()
1521 << " type on left hand side" << eom;
1522 throw 0;
1523 }
1524
1525 const irep_idt &component_name=
1526 expr.get(ID_component_name);
1527
1528 // first try to find directly
1530 struct_union_type.get_component(component_name);
1531
1532 // if that fails, search the anonymous members
1533
1534 if(component.is_nil())
1535 {
1536 exprt tmp=get_component_rec(op0, component_name, *this);
1537
1538 if(tmp.is_nil())
1539 {
1540 // give up
1542 error() << "member '" << component_name << "' not found in '"
1543 << to_string(type) << "'" << eom;
1544 throw 0;
1545 }
1546
1547 // done!
1548 expr.swap(tmp);
1549 return;
1550 }
1551
1552 expr.type()=component.type();
1553
1554 if(op0.get_bool(ID_C_lvalue))
1555 expr.set(ID_C_lvalue, true);
1556
1558 expr.type().set(ID_C_constant, true);
1559
1560 // copy method identifier
1561 const irep_idt &identifier=component.get(ID_C_identifier);
1562
1563 if(!identifier.empty())
1564 expr.set(ID_C_identifier, identifier);
1565
1566 const irep_idt &access=component.get_access();
1567
1568 if(access==ID_private)
1569 {
1571 error() << "member '" << component_name << "' is " << access << eom;
1572 throw 0;
1573 }
1574}
1575
1577{
1578 exprt::operandst &operands=expr.operands();
1579
1580 PRECONDITION(operands.size() == 3);
1581
1582 // copy (save) original types
1583 const typet o_type0=operands[0].type();
1584 const typet o_type1=operands[1].type();
1585 const typet o_type2=operands[2].type();
1586
1587 implicit_typecast_bool(operands[0]);
1588
1589 if(o_type1.id() == ID_empty || o_type2.id() == ID_empty)
1590 {
1591 operands[1] = typecast_exprt::conditional_cast(operands[1], void_type());
1592 operands[2] = typecast_exprt::conditional_cast(operands[2], void_type());
1593 expr.type() = void_type();
1594 return;
1595 }
1596
1597 if(operands[1].type().id()==ID_pointer &&
1598 operands[2].type().id()!=ID_pointer)
1599 implicit_typecast(operands[2], operands[1].type());
1600 else if(operands[2].type().id()==ID_pointer &&
1601 operands[1].type().id()!=ID_pointer)
1602 implicit_typecast(operands[1], operands[2].type());
1603
1604 if(operands[1].type().id()==ID_pointer &&
1605 operands[2].type().id()==ID_pointer &&
1606 operands[1].type()!=operands[2].type())
1607 {
1608 exprt tmp1=simplify_expr(operands[1], *this);
1609 exprt tmp2=simplify_expr(operands[2], *this);
1610
1611 // is one of them void * AND null? Convert that to the other.
1612 // (at least that's how GCC behaves)
1613 if(
1614 to_pointer_type(operands[1].type()).base_type().id() == ID_empty &&
1615 tmp1.is_constant() && is_null_pointer(to_constant_expr(tmp1)))
1616 {
1617 implicit_typecast(operands[1], operands[2].type());
1618 }
1619 else if(
1620 to_pointer_type(operands[2].type()).base_type().id() == ID_empty &&
1621 tmp2.is_constant() && is_null_pointer(to_constant_expr(tmp2)))
1622 {
1623 implicit_typecast(operands[2], operands[1].type());
1624 }
1625 else if(
1626 to_pointer_type(operands[1].type()).base_type().id() != ID_code ||
1627 to_pointer_type(operands[2].type()).base_type().id() != ID_code)
1628 {
1629 // Make it void *.
1630 // gcc and clang issue a warning for this.
1631 expr.type() = pointer_type(void_type());
1632 implicit_typecast(operands[1], expr.type());
1633 implicit_typecast(operands[2], expr.type());
1634 }
1635 else
1636 {
1637 // maybe functions without parameter lists
1638 const code_typet &c_type1 =
1639 to_code_type(to_pointer_type(operands[1].type()).base_type());
1640 const code_typet &c_type2 =
1641 to_code_type(to_pointer_type(operands[2].type()).base_type());
1642
1643 if(c_type1.return_type()==c_type2.return_type())
1644 {
1645 if(c_type1.parameters().empty() && c_type1.has_ellipsis())
1646 implicit_typecast(operands[1], operands[2].type());
1647 else if(c_type2.parameters().empty() && c_type2.has_ellipsis())
1648 implicit_typecast(operands[2], operands[1].type());
1649 }
1650 }
1651 }
1652
1653 if(operands[1].type().id()==ID_empty ||
1654 operands[2].type().id()==ID_empty)
1655 {
1656 expr.type()=void_type();
1657 return;
1658 }
1659
1660 if(
1661 operands[1].type() != operands[2].type() ||
1662 operands[1].type().id() == ID_array)
1663 {
1664 implicit_typecast_arithmetic(operands[1], operands[2]);
1665 }
1666
1667 if(operands[1].type() == operands[2].type())
1668 {
1669 expr.type()=operands[1].type();
1670
1671 // GCC says: "A conditional expression is a valid lvalue
1672 // if its type is not void and the true and false branches
1673 // are both valid lvalues."
1674
1675 if(operands[1].get_bool(ID_C_lvalue) &&
1676 operands[2].get_bool(ID_C_lvalue))
1677 expr.set(ID_C_lvalue, true);
1678
1679 return;
1680 }
1681
1683 error() << "operator ?: not defined for types '" << to_string(o_type1)
1684 << "' and '" << to_string(o_type2) << "'" << eom;
1685 throw 0;
1686}
1687
1689 side_effect_exprt &expr)
1690{
1691 // x ? : y is almost the same as x ? x : y,
1692 // but not quite, as x is evaluated only once
1693
1694 exprt::operandst &operands=expr.operands();
1695
1696 if(operands.size()!=2)
1697 {
1699 error() << "gcc conditional_expr expects two operands" << eom;
1700 throw 0;
1701 }
1702
1703 // use typechecking code for "if"
1704
1705 if_exprt if_expr(operands[0], operands[0], operands[1]);
1706 if_expr.add_source_location()=expr.source_location();
1707
1709
1710 // copy the result
1711 operands[0] = if_expr.true_case();
1712 operands[1] = if_expr.false_case();
1713 expr.type()=if_expr.type();
1714}
1715
1717{
1718 exprt &op = to_unary_expr(expr).op();
1719
1721
1722 if(error_opt.has_value())
1724
1725 // special case: address of label
1726 if(op.id()==ID_label)
1727 {
1728 expr.type()=pointer_type(void_type());
1729
1730 // remember the label
1732 return;
1733 }
1734
1735 // special case: address of function designator
1736 // ANSI-C 99 section 6.3.2.1 paragraph 4
1737
1738 if(
1739 op.id() == ID_address_of && op.get_bool(ID_C_implicit) &&
1740 to_address_of_expr(op).object().type().id() == ID_code)
1741 {
1742 // make the implicit address_of an explicit address_of
1743 exprt tmp;
1744 tmp.swap(op);
1745 tmp.set(ID_C_implicit, false);
1746 expr.swap(tmp);
1747 return;
1748 }
1749
1750 if(op.id()==ID_struct ||
1751 op.id()==ID_union ||
1752 op.id()==ID_array ||
1753 op.id()==ID_string_constant)
1754 {
1755 // these are really objects
1756 }
1757 else if(op.get_bool(ID_C_lvalue))
1758 {
1759 // ok
1760 }
1761 else if(op.type().id()==ID_code)
1762 {
1763 // ok
1764 }
1765 else
1766 {
1768 error() << "address_of error: '" << to_string(op) << "' not an lvalue"
1769 << eom;
1770 throw 0;
1771 }
1772
1773 expr.type()=pointer_type(op.type());
1774}
1775
1777{
1778 exprt &op = to_unary_expr(expr).op();
1779
1780 const typet op_type = op.type();
1781
1782 if(op_type.id()==ID_array)
1783 {
1784 // *a is the same as a[0]
1785 expr.id(ID_index);
1786 expr.type() = to_array_type(op_type).element_type();
1788 CHECK_RETURN(expr.operands().size() == 2);
1789 }
1790 else if(op_type.id()==ID_pointer)
1791 {
1792 expr.type() = to_pointer_type(op_type).base_type();
1793
1794 if(
1795 expr.type().id() == ID_empty &&
1797 {
1799 error() << "dereferencing void pointer" << eom;
1800 throw 0;
1801 }
1802 }
1803 else
1804 {
1806 error() << "operand of unary * '" << to_string(op)
1807 << "' is not a pointer, but got '" << to_string(op_type) << "'"
1808 << eom;
1809 throw 0;
1810 }
1811
1812 expr.set(ID_C_lvalue, true);
1813
1814 // if you dereference a pointer pointing to
1815 // a function, you get a pointer again
1816 // allowing ******...*p
1817
1819}
1820
1822{
1823 if(expr.type().id()==ID_code)
1824 {
1825 address_of_exprt tmp(expr, pointer_type(expr.type()));
1826 tmp.set(ID_C_implicit, true);
1827 tmp.add_source_location()=expr.source_location();
1828 expr=tmp;
1829 }
1830}
1831
1833{
1834 const irep_idt &statement=expr.get_statement();
1835
1836 if(statement==ID_preincrement ||
1837 statement==ID_predecrement ||
1838 statement==ID_postincrement ||
1839 statement==ID_postdecrement)
1840 {
1841 const exprt &op0 = to_unary_expr(expr).op();
1842 const typet &type0=op0.type();
1843
1844 if(!op0.get_bool(ID_C_lvalue))
1845 {
1847 error() << "prefix operator error: '" << to_string(op0)
1848 << "' not an lvalue" << eom;
1849 throw 0;
1850 }
1851
1852 if(type0.get_bool(ID_C_constant))
1853 {
1855 error() << "error: '" << to_string(op0) << "' is constant" << eom;
1856 throw 0;
1857 }
1858
1859 if(type0.id() == ID_c_enum_tag)
1860 {
1862 if(enum_type.is_incomplete())
1863 {
1865 error() << "operator '" << statement << "' given incomplete type '"
1866 << to_string(type0) << "'" << eom;
1867 throw 0;
1868 }
1869
1870 // increment/decrement on underlying type
1871 to_unary_expr(expr).op() =
1872 typecast_exprt(op0, enum_type.underlying_type());
1873 expr.type() = enum_type.underlying_type();
1874 }
1875 else if(type0.id() == ID_c_bit_field)
1876 {
1877 // promote to underlying type
1878 typet underlying_type = to_c_bit_field_type(type0).underlying_type();
1879 to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type);
1880 expr.type()=underlying_type;
1881 }
1882 else if(type0.id() == ID_bool || type0.id() == ID_c_bool)
1883 {
1885 expr.type() = op0.type();
1886 }
1887 else if(is_numeric_type(type0))
1888 {
1889 expr.type()=type0;
1890 }
1891 else if(type0.id() == ID_pointer)
1892 {
1894 expr.type() = to_unary_expr(expr).op().type();
1895 }
1896 else
1897 {
1899 error() << "operator '" << statement << "' not defined for type '"
1900 << to_string(type0) << "'" << eom;
1901 throw 0;
1902 }
1903 }
1904 else if(has_prefix(id2string(statement), "assign"))
1906 else if(statement==ID_function_call)
1909 else if(statement==ID_statement_expression)
1911 else if(statement==ID_gcc_conditional_expression)
1913 else
1914 {
1916 error() << "unknown side effect: " << statement << eom;
1917 throw 0;
1918 }
1919}
1920
1923{
1924 INVARIANT(
1925 expr.function().id() == ID_symbol &&
1926 to_symbol_expr(expr.function()).get_identifier() == CPROVER_PREFIX
1927 "typed_target",
1928 "expression must be a " CPROVER_PREFIX "typed_target function call");
1929
1930 auto &f_op = to_symbol_expr(expr.function());
1931
1932 if(expr.arguments().size() != 1)
1933 {
1935 "expected 1 argument for " CPROVER_PREFIX "typed_target, found " +
1936 std::to_string(expr.arguments().size()),
1937 expr.source_location()};
1938 }
1939
1940 auto arg0 = expr.arguments().front();
1941
1942 if(!is_assignable(arg0) || !arg0.get_bool(ID_C_lvalue))
1943 {
1945 "argument of " CPROVER_PREFIX "typed_target must be assignable",
1946 arg0.source_location()};
1947 }
1948
1949 const auto &size = size_of_expr(arg0.type(), *this);
1950 if(!size.has_value())
1951 {
1953 "sizeof not defined for argument of " CPROVER_PREFIX
1954 "typed_target of type " +
1955 to_string(arg0.type()),
1956 arg0.source_location()};
1957 }
1958
1959 // rewrite call to "assignable"
1960 f_op.set_identifier(CPROVER_PREFIX "assignable");
1961 exprt::operandst arguments;
1962 // pointer
1963 arguments.push_back(address_of_exprt(arg0));
1964 // size
1965 arguments.push_back(size.value());
1966 // is_pointer
1967 if(arg0.type().id() == ID_pointer)
1968 arguments.push_back(true_exprt());
1969 else
1970 arguments.push_back(false_exprt());
1971
1972 expr.arguments().swap(arguments);
1973 expr.type() = empty_typet();
1974}
1975
1978{
1979 INVARIANT(
1980 expr.function().id() == ID_symbol &&
1981 to_symbol_expr(expr.function()).get_identifier() == CPROVER_PREFIX
1982 "obeys_contract",
1983 "expression must be a " CPROVER_PREFIX "obeys_contract function call");
1984
1985 if(expr.arguments().size() != 2)
1986 {
1988 "expected 2 arguments for " CPROVER_PREFIX "obeys_contract, found " +
1989 std::to_string(expr.arguments().size()),
1990 expr.source_location()};
1991 }
1992
1993 // the first parameter must be a function pointer typed assignable path
1994 // expression, without side effects or ternary operator
1995 auto &function_pointer = expr.arguments()[0];
1996
1997 if(
1998 function_pointer.type().id() != ID_pointer ||
1999 to_pointer_type(function_pointer.type()).base_type().id() != ID_code ||
2000 !function_pointer.get_bool(ID_C_lvalue))
2001 {
2003 "the first argument of " CPROVER_PREFIX
2004 "obeys_contract must be a function pointer lvalue expression",
2005 function_pointer.source_location());
2006 }
2007
2009 {
2011 "the first argument of " CPROVER_PREFIX
2012 "obeys_contract must have no ternary operator",
2013 function_pointer.source_location());
2014 }
2015
2016 // second parameter must be the address of a function symbol
2017 auto &address_of_contract = expr.arguments()[1];
2018
2019 if(
2022 address_of_contract.type().id() != ID_pointer ||
2023 to_pointer_type(address_of_contract.type()).base_type().id() != ID_code)
2024 {
2026 "the second argument of " CPROVER_PREFIX
2027 "obeys_contract must must be a function symbol",
2028 address_of_contract.source_location());
2029 }
2030
2031 if(function_pointer.type() != address_of_contract.type())
2032 {
2034 "the first and second arguments of " CPROVER_PREFIX
2035 "obeys_contract must have the same function pointer type",
2036 expr.source_location());
2037 }
2038
2039 expr.type() = bool_typet();
2040}
2041
2043{
2044 return ::builtin_factory(
2045 identifier,
2046 config.ansi_c.float16_type,
2049}
2050
2053{
2054 if(expr.operands().size()!=2)
2055 {
2057 error() << "function_call side effect expects two operands" << eom;
2058 throw 0;
2059 }
2060
2061 exprt &f_op=expr.function();
2062
2063 // f_op is not yet typechecked, in contrast to the other arguments.
2064 // This is a big special case!
2065
2066 if(f_op.id()==ID_symbol)
2067 {
2068 irep_idt identifier=to_symbol_expr(f_op).get_identifier();
2069
2070 asm_label_mapt::const_iterator entry=
2071 asm_label_map.find(identifier);
2072 if(entry!=asm_label_map.end())
2073 identifier=entry->second;
2074
2075 if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
2076 {
2077 // This is an undeclared function.
2078
2079 // Is it the polymorphic typed_target function ?
2080 if(identifier == CPROVER_PREFIX "typed_target")
2081 {
2083 }
2084 // Is this a builtin?
2085 else if(!builtin_factory(identifier))
2086 {
2087 // yes, it's a builtin
2088 }
2089 else if(
2090 identifier == "__noop" &&
2092 {
2093 // https://docs.microsoft.com/en-us/cpp/intrinsics/noop
2094 // typecheck and discard, just generating 0 instead
2095 for(auto &op : expr.arguments())
2096 typecheck_expr(op);
2097
2099 expr.swap(result);
2100
2101 return;
2102 }
2103 else if(
2104 identifier == "__builtin_shuffle" &&
2106 {
2108 expr.swap(result);
2109
2110 return;
2111 }
2112 else if(identifier == "__builtin_shufflevector")
2113 {
2115 expr.swap(result);
2116
2117 return;
2118 }
2119 else if(
2120 identifier == CPROVER_PREFIX "saturating_minus" ||
2121 identifier == CPROVER_PREFIX "saturating_plus")
2122 {
2124 expr.swap(result);
2125
2126 return;
2127 }
2128 else if(identifier == CPROVER_PREFIX "equal")
2129 {
2130 if(expr.arguments().size() != 2)
2131 {
2132 error().source_location = f_op.source_location();
2133 error() << "equal expects two operands" << eom;
2134 throw 0;
2135 }
2136
2138 expr.arguments().front(), expr.arguments().back());
2139 equality_expr.add_source_location() = expr.source_location();
2140
2141 if(equality_expr.lhs().type() != equality_expr.rhs().type())
2142 {
2143 error().source_location = f_op.source_location();
2144 error() << "equal expects two operands of same type" << eom;
2145 throw 0;
2146 }
2147
2148 expr.swap(equality_expr);
2149 return;
2150 }
2151 else if(
2152 identifier == CPROVER_PREFIX "overflow_minus" ||
2153 identifier == CPROVER_PREFIX "overflow_mult" ||
2154 identifier == CPROVER_PREFIX "overflow_plus" ||
2155 identifier == CPROVER_PREFIX "overflow_shl")
2156 {
2157 exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
2158 overflow.add_source_location() = f_op.source_location();
2159
2160 if(identifier == CPROVER_PREFIX "overflow_minus")
2161 {
2162 overflow.id(ID_minus);
2164 }
2165 else if(identifier == CPROVER_PREFIX "overflow_mult")
2166 {
2167 overflow.id(ID_mult);
2169 }
2170 else if(identifier == CPROVER_PREFIX "overflow_plus")
2171 {
2172 overflow.id(ID_plus);
2174 }
2175 else if(identifier == CPROVER_PREFIX "overflow_shl")
2176 {
2177 overflow.id(ID_shl);
2179 }
2180
2182 overflow.operands()[0], overflow.id(), overflow.operands()[1]};
2183 of.add_source_location() = overflow.source_location();
2184 expr.swap(of);
2185 return;
2186 }
2187 else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
2188 {
2190 tmp.add_source_location() = f_op.source_location();
2191
2193
2194 unary_minus_overflow_exprt overflow{tmp.operands().front()};
2195 overflow.add_source_location() = tmp.source_location();
2196 expr.swap(overflow);
2197 return;
2198 }
2199 else if(identifier == CPROVER_PREFIX "enum_is_in_range")
2200 {
2201 // Check correct number of arguments
2202 if(expr.arguments().size() != 1)
2203 {
2204 std::ostringstream error_message;
2205 error_message << identifier << " takes exactly 1 argument, but "
2206 << expr.arguments().size() << " were provided";
2208 error_message.str(), expr.source_location()};
2209 }
2210 const auto &arg1 = expr.arguments()[0];
2212 {
2213 // Can't enum range check a non-enum
2214 std::ostringstream error_message;
2215 error_message << identifier << " expects enum, but ("
2216 << expr2c(arg1, *this) << ") has type `"
2217 << type2c(arg1.type(), *this) << '`';
2219 error_message.str(), expr.source_location()};
2220 }
2221
2223 in_range.add_source_location() = expr.source_location();
2224 exprt lowered = in_range.lower(*this);
2225 expr.swap(lowered);
2226 return;
2227 }
2228 else if(
2229 identifier == CPROVER_PREFIX "r_ok" ||
2230 identifier == CPROVER_PREFIX "w_ok" ||
2231 identifier == CPROVER_PREFIX "rw_ok")
2232 {
2233 if(expr.arguments().size() != 1 && expr.arguments().size() != 2)
2234 {
2236 id2string(identifier) + " expects one or two operands",
2237 f_op.source_location()};
2238 }
2239
2240 // the first argument must be a pointer
2241 auto &pointer_expr = expr.arguments()[0];
2242 if(pointer_expr.type().id() == ID_array)
2243 {
2245 dest_type.base_type().set(ID_C_constant, true);
2246 implicit_typecast(pointer_expr, dest_type);
2247 }
2248 else if(pointer_expr.type().id() != ID_pointer)
2249 {
2251 id2string(identifier) + " expects a pointer as first argument",
2252 f_op.source_location()};
2253 }
2254
2255 // The second argument, when given, is a size_t.
2256 // When not given, use the pointer subtype.
2258
2259 if(expr.arguments().size() == 2)
2260 {
2262 size_expr = expr.arguments()[1];
2263 }
2264 else
2265 {
2266 // Won't do void *
2267 const auto &subtype =
2268 to_pointer_type(pointer_expr.type()).base_type();
2269 if(subtype.id() == ID_empty)
2270 {
2272 id2string(identifier) +
2273 " expects a size when given a void pointer",
2274 f_op.source_location()};
2275 }
2276
2277 auto size_expr_opt = size_of_expr(subtype, *this);
2278 CHECK_RETURN(size_expr_opt.has_value());
2279 size_expr = std::move(size_expr_opt.value());
2280 }
2281
2282 irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok
2283 : identifier == CPROVER_PREFIX "w_ok" ? ID_w_ok
2284 : ID_rw_ok;
2285
2286 r_or_w_ok_exprt ok_expr(id, pointer_expr, size_expr);
2287 ok_expr.add_source_location() = expr.source_location();
2288
2289 expr.swap(ok_expr);
2290 return;
2291 }
2292 else if(
2294 {
2296 shadow_memory_builtin->get_identifier();
2297
2298 const auto builtin_code_type =
2300
2301 INVARIANT(
2302 builtin_code_type.has_ellipsis() &&
2303 builtin_code_type.parameters().empty(),
2304 "Shadow memory builtins should be an ellipsis with 0 parameter");
2305
2306 // Add the symbol to the symbol table if it is not present yet.
2308 {
2309 symbolt new_symbol{
2311 new_symbol.base_name = shadow_memory_builtin_id;
2312 new_symbol.location = f_op.source_location();
2313 // Add an empty implementation to avoid warnings about missing
2314 // implementation later on
2315 new_symbol.value = code_blockt{};
2316
2317 symbol_table.add(new_symbol);
2318 }
2319
2320 // Swap the current `function` field with the newly generated
2321 // `shadow_memory_builtin` `symbol_exprt` and carry on with typechecking
2322 f_op = std::move(*shadow_memory_builtin);
2323 }
2324 else if(
2326 identifier, expr.arguments(), f_op.source_location()))
2327 {
2328 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
2329 auto &parameters = to_code_type(gcc_polymorphic->type()).parameters();
2330 INVARIANT(
2331 !parameters.empty(),
2332 "GCC polymorphic built-ins should have at least one parameter");
2333
2334 // For all atomic/sync polymorphic built-ins (which are the ones handled
2335 // by typecheck_gcc_polymorphic_builtin), looking at the first parameter
2336 // suffices to distinguish different implementations.
2337 if(parameters.front().type().id() == ID_pointer)
2338 {
2340 id2string(identifier) + "_" +
2342 to_pointer_type(parameters.front().type()).base_type(), *this);
2343 }
2344 else
2345 {
2347 id2string(identifier) + "_" +
2348 type_to_partial_identifier(parameters.front().type(), *this);
2349 }
2350 gcc_polymorphic->set_identifier(identifier_with_type);
2351
2353 {
2354 for(std::size_t i = 0; i < parameters.size(); ++i)
2355 {
2356 const std::string base_name = "p_" + std::to_string(i);
2357
2358 parameter_symbolt new_symbol;
2359
2360 new_symbol.name =
2361 id2string(identifier_with_type) + "::" + base_name;
2362 new_symbol.base_name = base_name;
2363 new_symbol.location = f_op.source_location();
2364 new_symbol.type = parameters[i].type();
2365 new_symbol.is_parameter = true;
2366 new_symbol.is_lvalue = true;
2367 new_symbol.mode = ID_C;
2368
2369 parameters[i].set_identifier(new_symbol.name);
2370 parameters[i].set_base_name(new_symbol.base_name);
2371
2372 symbol_table.add(new_symbol);
2373 }
2374
2375 symbolt new_symbol{
2377 new_symbol.base_name = identifier_with_type;
2378 new_symbol.location = f_op.source_location();
2379 code_blockt implementation =
2382 return_type = to_code_type(gcc_polymorphic->type()).return_type();
2383 typecheck_code(implementation);
2385 new_symbol.value = implementation;
2386
2387 symbol_table.add(new_symbol);
2388 }
2389
2390 f_op = std::move(*gcc_polymorphic);
2391 }
2392 else
2393 {
2394 // This is an undeclared function that's not a builtin.
2395 // Let's just add it.
2396 // We do a bit of return-type guessing, but just a bit.
2398
2399 // The following isn't really right and sound, but there
2400 // are too many idiots out there who use malloc and the like
2401 // without the right header file.
2402 if(identifier=="malloc" ||
2403 identifier=="realloc" ||
2404 identifier=="reallocf" ||
2405 identifier=="valloc")
2406 {
2408 }
2409
2410 symbolt new_symbol{
2411 identifier, code_typet({}, guessed_return_type), mode};
2412 new_symbol.base_name=identifier;
2413 new_symbol.location=expr.source_location();
2414 new_symbol.type.set(ID_C_incomplete, true);
2415
2416 // TODO: should also guess some argument types
2417
2419 move_symbol(new_symbol, symbol_ptr);
2420
2421 warning().source_location=f_op.find_source_location();
2422 warning() << "function '" << identifier << "' is not declared" << eom;
2423 }
2424 }
2425 }
2426
2427 // typecheck it now
2429
2430 const typet f_op_type = f_op.type();
2431
2433 {
2434 const auto &mathematical_function_type =
2436
2437 // check number of arguments
2438 if(expr.arguments().size() != mathematical_function_type.domain().size())
2439 {
2440 error().source_location = f_op.source_location();
2441 error() << "expected " << mathematical_function_type.domain().size()
2442 << " arguments but got " << expr.arguments().size() << eom;
2443 throw 0;
2444 }
2445
2446 // check the types of the arguments
2447 for(auto &p :
2448 make_range(expr.arguments()).zip(mathematical_function_type.domain()))
2449 {
2450 if(p.first.type() != p.second)
2451 {
2452 error().source_location = p.first.source_location();
2453 error() << "expected argument of type " << to_string(p.second)
2454 << " but got " << to_string(p.first.type()) << eom;
2455 throw 0;
2456 }
2457 }
2458
2459 function_application_exprt function_application(f_op, expr.arguments());
2460
2461 function_application.add_source_location() = expr.source_location();
2462
2463 expr.swap(function_application);
2464 return;
2465 }
2466
2467 if(f_op_type.id()!=ID_pointer)
2468 {
2469 error().source_location = f_op.source_location();
2470 error() << "expected function/function pointer as argument but got '"
2471 << to_string(f_op_type) << "'" << eom;
2472 throw 0;
2473 }
2474
2475 // do implicit dereference
2476 if(f_op.id() == ID_address_of && f_op.get_bool(ID_C_implicit))
2477 {
2478 f_op = to_address_of_expr(f_op).object();
2479 }
2480 else
2481 {
2483 tmp.set(ID_C_implicit, true);
2484 tmp.add_source_location()=f_op.source_location();
2485 f_op.swap(tmp);
2486 }
2487
2488 if(f_op.type().id()!=ID_code)
2489 {
2490 error().source_location = f_op.source_location();
2491 error() << "expected code as argument" << eom;
2492 throw 0;
2493 }
2494
2495 const code_typet &code_type=to_code_type(f_op.type());
2496
2497 expr.type()=code_type.return_type();
2498
2500
2501 if(tmp.is_not_nil())
2502 expr.swap(tmp);
2503 else
2505}
2506
2509{
2510 const exprt &f_op=expr.function();
2511 const source_locationt &source_location=expr.source_location();
2512
2513 // some built-in functions
2514 if(f_op.id()!=ID_symbol)
2515 return nil_exprt();
2516
2517 const irep_idt &identifier=to_symbol_expr(f_op).get_identifier();
2518
2519 if(identifier == CPROVER_PREFIX "is_fresh")
2520 {
2521 if(expr.arguments().size() != 2)
2522 {
2523 error().source_location = f_op.source_location();
2524 error() << CPROVER_PREFIX "is_fresh expects two operands; "
2525 << expr.arguments().size() << "provided." << eom;
2526 throw 0;
2527 }
2529 return nil_exprt();
2530 }
2531 else if(identifier == CPROVER_PREFIX "obeys_contract")
2532 {
2534 // returning nil leaves the call expression in place
2535 return nil_exprt();
2536 }
2537 else if(identifier == CPROVER_PREFIX "pointer_in_range_dfcc")
2538 {
2539 // same as pointer_in_range with experimental support for DFCC contracts
2540 // -- do not use
2541 if(expr.arguments().size() != 3)
2542 {
2544 CPROVER_PREFIX "pointer_in_range_dfcc expects three arguments",
2545 expr.source_location()};
2546 }
2547
2548 for(const auto &arg : expr.arguments())
2549 {
2550 if(arg.type().id() != ID_pointer)
2551 {
2554 "pointer_in_range_dfcc expects pointer-typed arguments",
2555 arg.source_location()};
2556 }
2557 }
2558 return nil_exprt();
2559 }
2560 else if(identifier == CPROVER_PREFIX "same_object")
2561 {
2562 if(expr.arguments().size()!=2)
2563 {
2564 error().source_location = f_op.source_location();
2565 error() << "same_object expects two operands" << eom;
2566 throw 0;
2567 }
2568
2570
2572 same_object(expr.arguments()[0], expr.arguments()[1]);
2573 same_object_expr.add_source_location()=source_location;
2574
2575 return same_object_expr;
2576 }
2577 else if(identifier==CPROVER_PREFIX "get_must")
2578 {
2579 if(expr.arguments().size()!=2)
2580 {
2581 error().source_location = f_op.source_location();
2582 error() << "get_must expects two operands" << eom;
2583 throw 0;
2584 }
2585
2587
2589 expr.arguments()[0], ID_get_must, expr.arguments()[1]);
2590 get_must_expr.add_source_location()=source_location;
2591
2592 return std::move(get_must_expr);
2593 }
2594 else if(identifier==CPROVER_PREFIX "get_may")
2595 {
2596 if(expr.arguments().size()!=2)
2597 {
2598 error().source_location = f_op.source_location();
2599 error() << "get_may expects two operands" << eom;
2600 throw 0;
2601 }
2602
2604
2606 expr.arguments()[0], ID_get_may, expr.arguments()[1]);
2607 get_may_expr.add_source_location()=source_location;
2608
2609 return std::move(get_may_expr);
2610 }
2611 else if(identifier == CPROVER_PREFIX "is_invalid_pointer")
2612 {
2613 if(expr.arguments().size()!=1)
2614 {
2615 error().source_location = f_op.source_location();
2616 error() << "is_invalid_pointer expects one operand" << eom;
2617 throw 0;
2618 }
2619
2621
2623 same_object_expr.add_source_location()=source_location;
2624
2625 return same_object_expr;
2626 }
2627 else if(identifier==CPROVER_PREFIX "buffer_size")
2628 {
2629 if(expr.arguments().size()!=1)
2630 {
2631 error().source_location = f_op.source_location();
2632 error() << "buffer_size expects one operand" << eom;
2633 throw 0;
2634 }
2635
2637
2638 exprt buffer_size_expr("buffer_size", size_type());
2639 buffer_size_expr.operands()=expr.arguments();
2640 buffer_size_expr.add_source_location()=source_location;
2641
2642 return buffer_size_expr;
2643 }
2644 else if(identifier == CPROVER_PREFIX "is_list")
2645 {
2646 // experimental feature for CHC encodings -- do not use
2647 if(expr.arguments().size() != 1)
2648 {
2649 error().source_location = f_op.source_location();
2650 error() << "is_list expects one operand" << eom;
2651 throw 0;
2652 }
2653
2655
2656 if(
2657 expr.arguments()[0].type().id() != ID_pointer ||
2658 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2660 {
2661 error().source_location = expr.arguments()[0].source_location();
2662 error() << "is_list expects a struct-pointer operand" << eom;
2663 throw 0;
2664 }
2665
2666 predicate_exprt is_list_expr("is_list");
2667 is_list_expr.operands() = expr.arguments();
2668 is_list_expr.add_source_location() = source_location;
2669
2670 return std::move(is_list_expr);
2671 }
2672 else if(identifier == CPROVER_PREFIX "is_dll")
2673 {
2674 // experimental feature for CHC encodings -- do not use
2675 if(expr.arguments().size() != 1)
2676 {
2677 error().source_location = f_op.source_location();
2678 error() << "is_dll expects one operand" << eom;
2679 throw 0;
2680 }
2681
2683
2684 if(
2685 expr.arguments()[0].type().id() != ID_pointer ||
2686 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2688 {
2689 error().source_location = expr.arguments()[0].source_location();
2690 error() << "is_dll expects a struct-pointer operand" << eom;
2691 throw 0;
2692 }
2693
2694 predicate_exprt is_dll_expr("is_dll");
2695 is_dll_expr.operands() = expr.arguments();
2696 is_dll_expr.add_source_location() = source_location;
2697
2698 return std::move(is_dll_expr);
2699 }
2700 else if(identifier == CPROVER_PREFIX "is_cyclic_dll")
2701 {
2702 // experimental feature for CHC encodings -- do not use
2703 if(expr.arguments().size() != 1)
2704 {
2705 error().source_location = f_op.source_location();
2706 error() << "is_cyclic_dll expects one operand" << eom;
2707 throw 0;
2708 }
2709
2711
2712 if(
2713 expr.arguments()[0].type().id() != ID_pointer ||
2714 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2716 {
2717 error().source_location = expr.arguments()[0].source_location();
2718 error() << "is_cyclic_dll expects a struct-pointer operand" << eom;
2719 throw 0;
2720 }
2721
2722 predicate_exprt is_cyclic_dll_expr("is_cyclic_dll");
2723 is_cyclic_dll_expr.operands() = expr.arguments();
2724 is_cyclic_dll_expr.add_source_location() = source_location;
2725
2726 return std::move(is_cyclic_dll_expr);
2727 }
2728 else if(identifier == CPROVER_PREFIX "is_sentinel_dll")
2729 {
2730 // experimental feature for CHC encodings -- do not use
2731 if(expr.arguments().size() != 2 && expr.arguments().size() != 3)
2732 {
2733 error().source_location = f_op.source_location();
2734 error() << "is_sentinel_dll expects two or three operands" << eom;
2735 throw 0;
2736 }
2737
2739
2741 args_no_cast.reserve(expr.arguments().size());
2742 for(const auto &argument : expr.arguments())
2743 {
2745 if(
2746 args_no_cast.back().type().id() != ID_pointer ||
2747 to_pointer_type(args_no_cast.back().type()).base_type().id() !=
2749 {
2750 error().source_location = expr.arguments()[0].source_location();
2751 error() << "is_sentinel_dll_node expects struct-pointer operands"
2752 << eom;
2753 throw 0;
2754 }
2755 }
2756
2757 predicate_exprt is_sentinel_dll_expr("is_sentinel_dll");
2759 is_sentinel_dll_expr.add_source_location() = source_location;
2760
2761 return std::move(is_sentinel_dll_expr);
2762 }
2763 else if(identifier == CPROVER_PREFIX "is_cstring")
2764 {
2765 // experimental feature for CHC encodings -- do not use
2766 if(expr.arguments().size() != 1)
2767 {
2768 error().source_location = f_op.source_location();
2769 error() << "is_cstring expects one operand" << eom;
2770 throw 0;
2771 }
2772
2774
2775 if(expr.arguments()[0].type().id() != ID_pointer)
2776 {
2777 error().source_location = expr.arguments()[0].source_location();
2778 error() << "is_cstring expects a pointer operand" << eom;
2779 throw 0;
2780 }
2781
2783 is_cstring_expr.add_source_location() = source_location;
2784
2785 return std::move(is_cstring_expr);
2786 }
2787 else if(identifier == CPROVER_PREFIX "cstrlen")
2788 {
2789 // experimental feature for CHC encodings -- do not use
2790 if(expr.arguments().size() != 1)
2791 {
2792 error().source_location = f_op.source_location();
2793 error() << "cstrlen expects one operand" << eom;
2794 throw 0;
2795 }
2796
2798
2799 if(expr.arguments()[0].type().id() != ID_pointer)
2800 {
2801 error().source_location = expr.arguments()[0].source_location();
2802 error() << "cstrlen expects a pointer operand" << eom;
2803 throw 0;
2804 }
2805
2807 cstrlen_expr.add_source_location() = source_location;
2808
2809 return std::move(cstrlen_expr);
2810 }
2811 else if(identifier==CPROVER_PREFIX "is_zero_string")
2812 {
2813 if(expr.arguments().size()!=1)
2814 {
2815 error().source_location = f_op.source_location();
2816 error() << "is_zero_string expects one operand" << eom;
2817 throw 0;
2818 }
2819
2821
2823 "is_zero_string", expr.arguments()[0], c_bool_type());
2824 is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
2825 is_zero_string_expr.add_source_location()=source_location;
2826
2827 return std::move(is_zero_string_expr);
2828 }
2829 else if(identifier==CPROVER_PREFIX "zero_string_length")
2830 {
2831 if(expr.arguments().size()!=1)
2832 {
2833 error().source_location = f_op.source_location();
2834 error() << "zero_string_length expects one operand" << eom;
2835 throw 0;
2836 }
2837
2839
2840 exprt zero_string_length_expr("zero_string_length", size_type());
2841 zero_string_length_expr.operands()=expr.arguments();
2842 zero_string_length_expr.set(ID_C_lvalue, true); // make it an lvalue
2843 zero_string_length_expr.add_source_location()=source_location;
2844
2846 }
2847 else if(identifier==CPROVER_PREFIX "DYNAMIC_OBJECT")
2848 {
2849 if(expr.arguments().size()!=1)
2850 {
2851 error().source_location = f_op.source_location();
2852 error() << "dynamic_object expects one argument" << eom;
2853 throw 0;
2854 }
2855
2857
2859 is_dynamic_object_expr.add_source_location() = source_location;
2860
2862 }
2863 else if(identifier == CPROVER_PREFIX "LIVE_OBJECT")
2864 {
2865 if(expr.arguments().size() != 1)
2866 {
2867 error().source_location = f_op.source_location();
2868 error() << "live_object expects one argument" << eom;
2869 throw 0;
2870 }
2871
2873
2875 live_object_expr.add_source_location() = source_location;
2876
2877 return live_object_expr;
2878 }
2879 else if(identifier == CPROVER_PREFIX "pointer_in_range")
2880 {
2881 if(expr.arguments().size() != 3)
2882 {
2883 error().source_location = f_op.source_location();
2884 error() << "pointer_in_range expects three arguments" << eom;
2885 throw 0;
2886 }
2887
2889
2891 expr.arguments()[0], expr.arguments()[1], expr.arguments()[2]);
2892 pointer_in_range_expr.add_source_location() = source_location;
2893
2894 return pointer_in_range_expr;
2895 }
2896 else if(identifier == CPROVER_PREFIX "WRITEABLE_OBJECT")
2897 {
2898 if(expr.arguments().size() != 1)
2899 {
2900 error().source_location = f_op.source_location();
2901 error() << "writeable_object expects one argument" << eom;
2902 throw 0;
2903 }
2904
2906
2908 writeable_object_expr.add_source_location() = source_location;
2909
2910 return writeable_object_expr;
2911 }
2912 else if(identifier == CPROVER_PREFIX "separate")
2913 {
2914 // experimental feature for CHC encodings -- do not use
2915 if(expr.arguments().size() < 2)
2916 {
2917 error().source_location = f_op.source_location();
2918 error() << "separate expects two or more arguments" << eom;
2919 throw 0;
2920 }
2921
2923
2925 separate_expr.add_source_location() = source_location;
2926
2927 return separate_expr;
2928 }
2929 else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
2930 {
2931 if(expr.arguments().size()!=1)
2932 {
2933 error().source_location = f_op.source_location();
2934 error() << "pointer_offset expects one argument" << eom;
2935 throw 0;
2936 }
2937
2939
2941 pointer_offset_expr.add_source_location()=source_location;
2942
2944 }
2945 else if(identifier == CPROVER_PREFIX "OBJECT_SIZE")
2946 {
2947 if(expr.arguments().size() != 1)
2948 {
2949 error().source_location = f_op.source_location();
2950 error() << "object_size expects one operand" << eom;
2951 throw 0;
2952 }
2953
2955
2957 object_size_expr.add_source_location() = source_location;
2958
2959 return std::move(object_size_expr);
2960 }
2961 else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
2962 {
2963 if(expr.arguments().size()!=1)
2964 {
2965 error().source_location = f_op.source_location();
2966 error() << "pointer_object expects one argument" << eom;
2967 throw 0;
2968 }
2969
2971
2973 pointer_object_expr.add_source_location() = source_location;
2974
2976 }
2977 else if(identifier=="__builtin_bswap16" ||
2978 identifier=="__builtin_bswap32" ||
2979 identifier=="__builtin_bswap64")
2980 {
2981 if(expr.arguments().size()!=1)
2982 {
2983 error().source_location = f_op.source_location();
2984 error() << identifier << " expects one operand" << eom;
2985 throw 0;
2986 }
2987
2989
2990 // these are hard-wired to 8 bits according to the gcc manual
2991 bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
2992 bswap_expr.add_source_location()=source_location;
2993
2994 return std::move(bswap_expr);
2995 }
2996 else if(
2997 identifier == "__builtin_rotateleft8" ||
2998 identifier == "__builtin_rotateleft16" ||
2999 identifier == "__builtin_rotateleft32" ||
3000 identifier == "__builtin_rotateleft64" ||
3001 identifier == "__builtin_rotateright8" ||
3002 identifier == "__builtin_rotateright16" ||
3003 identifier == "__builtin_rotateright32" ||
3004 identifier == "__builtin_rotateright64")
3005 {
3006 // clang only
3007 if(expr.arguments().size() != 2)
3008 {
3009 error().source_location = f_op.source_location();
3010 error() << identifier << " expects two operands" << eom;
3011 throw 0;
3012 }
3013
3015
3016 irep_idt id = (identifier == "__builtin_rotateleft8" ||
3017 identifier == "__builtin_rotateleft16" ||
3018 identifier == "__builtin_rotateleft32" ||
3019 identifier == "__builtin_rotateleft64")
3020 ? ID_rol
3021 : ID_ror;
3022
3023 shift_exprt rotate_expr(expr.arguments()[0], id, expr.arguments()[1]);
3024 rotate_expr.add_source_location() = source_location;
3025
3026 return std::move(rotate_expr);
3027 }
3028 else if(identifier=="__builtin_nontemporal_load")
3029 {
3030 if(expr.arguments().size()!=1)
3031 {
3032 error().source_location = f_op.source_location();
3033 error() << identifier << " expects one operand" << eom;
3034 throw 0;
3035 }
3036
3038
3039 // these return the subtype of the argument
3040 exprt &ptr_arg=expr.arguments().front();
3041
3042 if(ptr_arg.type().id()!=ID_pointer)
3043 {
3044 error().source_location = f_op.source_location();
3045 error() << "__builtin_nontemporal_load takes pointer as argument" << eom;
3046 throw 0;
3047 }
3048
3049 expr.type() = to_pointer_type(expr.arguments().front().type()).base_type();
3050
3051 return expr;
3052 }
3053 else if(
3054 identifier == "__builtin_fpclassify" ||
3055 identifier == CPROVER_PREFIX "fpclassify")
3056 {
3057 if(expr.arguments().size() != 6)
3058 {
3059 error().source_location = f_op.source_location();
3060 error() << identifier << " expects six arguments" << eom;
3061 throw 0;
3062 }
3063
3065
3066 // This gets 5 integers followed by a float or double.
3067 // The five integers are the return values for the cases
3068 // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
3069 // gcc expects this to be able to produce compile-time constants.
3070
3071 const exprt &fp_value = expr.arguments()[5];
3072
3073 if(fp_value.type().id() != ID_floatbv)
3074 {
3075 error().source_location = fp_value.source_location();
3076 error() << "non-floating-point argument for " << identifier << eom;
3077 throw 0;
3078 }
3079
3080 const auto &floatbv_type = to_floatbv_type(fp_value.type());
3081
3082 const exprt zero = ieee_floatt::zero(floatbv_type).to_expr();
3083
3084 const auto &arguments = expr.arguments();
3085
3086 return if_exprt(
3088 arguments[0],
3089 if_exprt(
3091 arguments[1],
3092 if_exprt(
3094 arguments[2],
3095 if_exprt(
3097 arguments[4],
3098 arguments[3])))); // subnormal
3099 }
3100 else if(identifier==CPROVER_PREFIX "isnanf" ||
3101 identifier==CPROVER_PREFIX "isnand" ||
3102 identifier==CPROVER_PREFIX "isnanld" ||
3103 identifier=="__builtin_isnan")
3104 {
3105 if(expr.arguments().size()!=1)
3106 {
3107 error().source_location = f_op.source_location();
3108 error() << "isnan expects one operand" << eom;
3109 throw 0;
3110 }
3111
3113
3114 isnan_exprt isnan_expr(expr.arguments().front());
3115 isnan_expr.add_source_location()=source_location;
3116
3118 }
3119 else if(identifier==CPROVER_PREFIX "isfinitef" ||
3120 identifier==CPROVER_PREFIX "isfinited" ||
3121 identifier==CPROVER_PREFIX "isfiniteld")
3122 {
3123 if(expr.arguments().size()!=1)
3124 {
3125 error().source_location = f_op.source_location();
3126 error() << "isfinite expects one operand" << eom;
3127 throw 0;
3128 }
3129
3131
3132 isfinite_exprt isfinite_expr(expr.arguments().front());
3133 isfinite_expr.add_source_location()=source_location;
3134
3136 }
3137 else if(identifier==CPROVER_PREFIX "inf" ||
3138 identifier=="__builtin_inf")
3139 {
3143 inf_expr.add_source_location()=source_location;
3144
3145 return std::move(inf_expr);
3146 }
3147 else if(identifier==CPROVER_PREFIX "inff")
3148 {
3152 inff_expr.add_source_location()=source_location;
3153
3154 return std::move(inff_expr);
3155 }
3156 else if(identifier==CPROVER_PREFIX "infl")
3157 {
3161 infl_expr.add_source_location()=source_location;
3162
3163 return std::move(infl_expr);
3164 }
3165 else if(
3166 identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
3167 identifier == CPROVER_PREFIX "llabs" ||
3168 identifier == CPROVER_PREFIX "imaxabs" ||
3169 identifier == CPROVER_PREFIX "fabs" ||
3170 identifier == CPROVER_PREFIX "fabsf" ||
3171 identifier == CPROVER_PREFIX "fabsl")
3172 {
3173 if(expr.arguments().size()!=1)
3174 {
3175 error().source_location = f_op.source_location();
3176 error() << "abs-functions expect one operand" << eom;
3177 throw 0;
3178 }
3179
3181
3182 abs_exprt abs_expr(expr.arguments().front());
3183 abs_expr.add_source_location()=source_location;
3184
3185 return std::move(abs_expr);
3186 }
3187 else if(
3188 identifier == CPROVER_PREFIX "fmod" ||
3189 identifier == CPROVER_PREFIX "fmodf" ||
3190 identifier == CPROVER_PREFIX "fmodl")
3191 {
3192 if(expr.arguments().size() != 2)
3193 {
3194 error().source_location = f_op.source_location();
3195 error() << "fmod-functions expect two operands" << eom;
3196 throw 0;
3197 }
3198
3200
3201 // Note that the semantics differ from the
3202 // "floating point remainder" operation as defined by IEEE.
3203 // Note that these do not take a rounding mode.
3205 expr.arguments()[0], ID_floatbv_mod, expr.arguments()[1]);
3206
3207 fmod_expr.add_source_location() = source_location;
3208
3209 return std::move(fmod_expr);
3210 }
3211 else if(
3212 identifier == CPROVER_PREFIX "remainder" ||
3213 identifier == CPROVER_PREFIX "remainderf" ||
3214 identifier == CPROVER_PREFIX "remainderl")
3215 {
3216 if(expr.arguments().size() != 2)
3217 {
3218 error().source_location = f_op.source_location();
3219 error() << "remainder-functions expect two operands" << eom;
3220 throw 0;
3221 }
3222
3224
3225 // The semantics of these functions is meant to match the
3226 // "floating point remainder" operation as defined by IEEE.
3227 // Note that these do not take a rounding mode.
3229 expr.arguments()[0], ID_floatbv_rem, expr.arguments()[1]);
3230
3231 floatbv_rem_expr.add_source_location() = source_location;
3232
3233 return std::move(floatbv_rem_expr);
3234 }
3235 else if(identifier==CPROVER_PREFIX "allocate")
3236 {
3237 if(expr.arguments().size()!=2)
3238 {
3239 error().source_location = f_op.source_location();
3240 error() << "allocate expects two operands" << eom;
3241 throw 0;
3242 }
3243
3245
3246 side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
3247 malloc_expr.operands()=expr.arguments();
3248
3249 return std::move(malloc_expr);
3250 }
3251 else if(
3252 (identifier == CPROVER_PREFIX "old") ||
3253 (identifier == CPROVER_PREFIX "loop_entry"))
3254 {
3255 if(expr.arguments().size() != 1)
3256 {
3257 error().source_location = f_op.source_location();
3258 error() << identifier << " expects one operand" << eom;
3259 throw 0;
3260 }
3261
3262 const auto &param_id = expr.arguments().front().id();
3263 if(!(param_id == ID_dereference || param_id == ID_member ||
3266 param_id == ID_index))
3267 {
3268 error().source_location = f_op.source_location();
3269 error() << "Tracking history of " << param_id
3270 << " expressions is not supported yet." << eom;
3271 throw 0;
3272 }
3273
3274 irep_idt id = identifier == CPROVER_PREFIX "old" ? ID_old : ID_loop_entry;
3275
3276 history_exprt old_expr(expr.arguments()[0], id);
3277 old_expr.add_source_location() = source_location;
3278
3279 return std::move(old_expr);
3280 }
3281 else if(identifier==CPROVER_PREFIX "isinff" ||
3282 identifier==CPROVER_PREFIX "isinfd" ||
3283 identifier==CPROVER_PREFIX "isinfld" ||
3284 identifier=="__builtin_isinf")
3285 {
3286 if(expr.arguments().size()!=1)
3287 {
3288 error().source_location = f_op.source_location();
3289 error() << identifier << " expects one operand" << eom;
3290 throw 0;
3291 }
3292
3294
3295 const exprt &fp_value = expr.arguments().front();
3296
3297 if(fp_value.type().id() != ID_floatbv)
3298 {
3299 error().source_location = fp_value.source_location();
3300 error() << "non-floating-point argument for " << identifier << eom;
3301 throw 0;
3302 }
3303
3304 isinf_exprt isinf_expr(expr.arguments().front());
3305 isinf_expr.add_source_location()=source_location;
3306
3308 }
3309 else if(identifier == "__builtin_isinf_sign")
3310 {
3311 if(expr.arguments().size() != 1)
3312 {
3313 error().source_location = f_op.source_location();
3314 error() << identifier << " expects one operand" << eom;
3315 throw 0;
3316 }
3317
3319
3320 // returns 1 for +inf and -1 for -inf, and 0 otherwise
3321
3322 const exprt &fp_value = expr.arguments().front();
3323
3324 if(fp_value.type().id() != ID_floatbv)
3325 {
3326 error().source_location = fp_value.source_location();
3327 error() << "non-floating-point argument for " << identifier << eom;
3328 throw 0;
3329 }
3330
3332 isinf_expr.add_source_location() = source_location;
3333
3334 return if_exprt(
3336 if_exprt(
3338 from_integer(-1, expr.type()),
3339 from_integer(1, expr.type())),
3340 from_integer(0, expr.type()));
3341 }
3342 else if(identifier == CPROVER_PREFIX "isnormalf" ||
3343 identifier == CPROVER_PREFIX "isnormald" ||
3344 identifier == CPROVER_PREFIX "isnormalld" ||
3345 identifier == "__builtin_isnormal")
3346 {
3347 if(expr.arguments().size()!=1)
3348 {
3349 error().source_location = f_op.source_location();
3350 error() << identifier << " expects one operand" << eom;
3351 throw 0;
3352 }
3353
3355
3356 const exprt &fp_value = expr.arguments()[0];
3357
3358 if(fp_value.type().id() != ID_floatbv)
3359 {
3360 error().source_location = fp_value.source_location();
3361 error() << "non-floating-point argument for " << identifier << eom;
3362 throw 0;
3363 }
3364
3365 isnormal_exprt isnormal_expr(expr.arguments().front());
3366 isnormal_expr.add_source_location()=source_location;
3367
3369 }
3370 else if(identifier==CPROVER_PREFIX "signf" ||
3371 identifier==CPROVER_PREFIX "signd" ||
3372 identifier==CPROVER_PREFIX "signld" ||
3373 identifier=="__builtin_signbit" ||
3374 identifier=="__builtin_signbitf" ||
3375 identifier=="__builtin_signbitl")
3376 {
3377 if(expr.arguments().size()!=1)
3378 {
3379 error().source_location = f_op.source_location();
3380 error() << identifier << " expects one operand" << eom;
3381 throw 0;
3382 }
3383
3385
3386 sign_exprt sign_expr(expr.arguments().front());
3387 sign_expr.add_source_location()=source_location;
3388
3390 }
3391 else if(identifier=="__builtin_popcount" ||
3392 identifier=="__builtin_popcountl" ||
3393 identifier=="__builtin_popcountll" ||
3394 identifier=="__popcnt16" ||
3395 identifier=="__popcnt" ||
3396 identifier=="__popcnt64")
3397 {
3398 if(expr.arguments().size()!=1)
3399 {
3400 error().source_location = f_op.source_location();
3401 error() << identifier << " expects one operand" << eom;
3402 throw 0;
3403 }
3404
3406
3407 popcount_exprt popcount_expr(expr.arguments().front(), expr.type());
3408 popcount_expr.add_source_location()=source_location;
3409
3410 return std::move(popcount_expr);
3411 }
3412 else if(
3413 identifier == "__builtin_clz" || identifier == "__builtin_clzl" ||
3414 identifier == "__builtin_clzll" || identifier == "__lzcnt16" ||
3415 identifier == "__lzcnt" || identifier == "__lzcnt64")
3416 {
3417 if(expr.arguments().size() != 1)
3418 {
3419 error().source_location = f_op.source_location();
3420 error() << identifier << " expects one operand" << eom;
3421 throw 0;
3422 }
3423
3425
3427 has_prefix(id2string(identifier), "__lzcnt"),
3428 expr.type()};
3429 clz.add_source_location() = source_location;
3430
3431 return std::move(clz);
3432 }
3433 else if(
3434 identifier == "__builtin_ctz" || identifier == "__builtin_ctzl" ||
3435 identifier == "__builtin_ctzll")
3436 {
3437 if(expr.arguments().size() != 1)
3438 {
3439 error().source_location = f_op.source_location();
3440 error() << identifier << " expects one operand" << eom;
3441 throw 0;
3442 }
3443
3445
3447 expr.arguments().front(), false, expr.type()};
3448 ctz.add_source_location() = source_location;
3449
3450 return std::move(ctz);
3451 }
3452 else if(
3453 identifier == "__builtin_ffs" || identifier == "__builtin_ffsl" ||
3454 identifier == "__builtin_ffsll")
3455 {
3456 if(expr.arguments().size() != 1)
3457 {
3458 error().source_location = f_op.source_location();
3459 error() << identifier << " expects one operand" << eom;
3460 throw 0;
3461 }
3462
3464
3465 find_first_set_exprt ffs{expr.arguments().front(), expr.type()};
3466 ffs.add_source_location() = source_location;
3467
3468 return std::move(ffs);
3469 }
3470 else if(identifier=="__builtin_expect")
3471 {
3472 // This is a gcc extension to provide branch prediction.
3473 // We compile it away, but adding some IR instruction for
3474 // this would clearly be an option. Note that the type
3475 // of the return value is wired to "long", i.e.,
3476 // this may trigger a type conversion due to the signature
3477 // of this function.
3478 if(expr.arguments().size()!=2)
3479 {
3480 error().source_location = f_op.source_location();
3481 error() << "__builtin_expect expects two arguments" << eom;
3482 throw 0;
3483 }
3484
3486
3487 return typecast_exprt(expr.arguments()[0], expr.type());
3488 }
3489 else if(identifier=="__builtin_object_size")
3490 {
3491 // this is a gcc extension to provide information about
3492 // object sizes at compile time
3493 // http://gcc.gnu.org/onlinedocs/gcc/Object-Size-Checking.html
3494
3495 if(expr.arguments().size()!=2)
3496 {
3497 error().source_location = f_op.source_location();
3498 error() << "__builtin_object_size expects two arguments" << eom;
3499 throw 0;
3500 }
3501
3503
3504 make_constant(expr.arguments()[1]);
3505
3507
3508 if(expr.arguments()[1].is_true())
3509 arg1=1;
3510 else if(expr.arguments()[1].is_false())
3511 arg1=0;
3512 else if(to_integer(to_constant_expr(expr.arguments()[1]), arg1))
3513 {
3514 error().source_location = f_op.source_location();
3515 error() << "__builtin_object_size expects constant as second argument, "
3516 << "but got " << to_string(expr.arguments()[1]) << eom;
3517 throw 0;
3518 }
3519
3520 exprt tmp;
3521
3522 // the following means "don't know"
3523 if(arg1==0 || arg1==1)
3524 {
3525 tmp=from_integer(-1, size_type());
3526 tmp.add_source_location()=f_op.source_location();
3527 }
3528 else
3529 {
3531 tmp.add_source_location()=f_op.source_location();
3532 }
3533
3534 return tmp;
3535 }
3536 else if(identifier=="__builtin_choose_expr")
3537 {
3538 // this is a gcc extension similar to ?:
3539 if(expr.arguments().size()!=3)
3540 {
3541 error().source_location = f_op.source_location();
3542 error() << "__builtin_choose_expr expects three arguments" << eom;
3543 throw 0;
3544 }
3545
3547
3548 exprt arg0 =
3551
3552 if(arg0.is_true())
3553 return expr.arguments()[1];
3554 else
3555 return expr.arguments()[2];
3556 }
3557 else if(identifier=="__builtin_constant_p")
3558 {
3559 // this is a gcc extension to tell whether the argument
3560 // is known to be a compile-time constant
3561 if(expr.arguments().size()!=1)
3562 {
3563 error().source_location = f_op.source_location();
3564 error() << "__builtin_constant_p expects one argument" << eom;
3565 throw 0;
3566 }
3567
3568 // do not typecheck the argument - it is never evaluated, and thus side
3569 // effects must not show up either
3570
3571 // try to produce constant
3572 exprt tmp1=expr.arguments().front();
3573 simplify(tmp1, *this);
3574
3575 bool is_constant=false;
3576
3577 // Need to do some special treatment for string literals,
3578 // which are (void *)&("lit"[0])
3579 if(
3580 tmp1.id() == ID_typecast &&
3581 to_typecast_expr(tmp1).op().id() == ID_address_of &&
3582 to_address_of_expr(to_typecast_expr(tmp1).op()).object().id() ==
3583 ID_index &&
3585 .array()
3586 .id() == ID_string_constant)
3587 {
3588 is_constant=true;
3589 }
3590 else
3591 is_constant=tmp1.is_constant();
3592
3594 tmp2.add_source_location()=source_location;
3595
3596 return tmp2;
3597 }
3598 else if(identifier=="__builtin_classify_type")
3599 {
3600 // This is a gcc/clang extension that produces an integer
3601 // constant for the type of the argument expression.
3602 if(expr.arguments().size()!=1)
3603 {
3604 error().source_location = f_op.source_location();
3605 error() << "__builtin_classify_type expects one argument" << eom;
3606 throw 0;
3607 }
3608
3610
3611 exprt object=expr.arguments()[0];
3612
3613 // The value doesn't matter at all, we only care about the type.
3614 // Need to sync with typeclass.h.
3615 typet type = follow(object.type());
3616
3617 // use underlying type for bit fields
3618 if(type.id() == ID_c_bit_field)
3619 type = to_c_bit_field_type(type).underlying_type();
3620
3621 unsigned type_number;
3622
3623 if(type.id() == ID_bool || type.id() == ID_c_bool)
3624 {
3625 // clang returns 4 for _Bool, gcc treats these as 'int'.
3626 type_number =
3628 }
3629 else
3630 {
3631 type_number =
3632 type.id() == ID_empty
3633 ? 0u
3634 : (type.id() == ID_bool || type.id() == ID_c_bool)
3635 ? 4u
3636 : (type.id() == ID_pointer || type.id() == ID_array)
3637 ? 5u
3638 : type.id() == ID_floatbv
3639 ? 8u
3640 : (type.id() == ID_complex &&
3641 to_complex_type(type).subtype().id() == ID_floatbv)
3642 ? 9u
3643 : type.id() == ID_struct
3644 ? 12u
3645 : type.id() == ID_union
3646 ? 13u
3647 : 1u; // int, short, char, enum_tag
3648 }
3649
3651 tmp.add_source_location()=source_location;
3652
3653 return tmp;
3654 }
3655 else if(
3656 identifier == "__builtin_add_overflow" ||
3657 identifier == "__builtin_sadd_overflow" ||
3658 identifier == "__builtin_saddl_overflow" ||
3659 identifier == "__builtin_saddll_overflow" ||
3660 identifier == "__builtin_uadd_overflow" ||
3661 identifier == "__builtin_uaddl_overflow" ||
3662 identifier == "__builtin_uaddll_overflow" ||
3663 identifier == "__builtin_add_overflow_p")
3664 {
3665 return typecheck_builtin_overflow(expr, ID_plus);
3666 }
3667 else if(
3668 identifier == "__builtin_sub_overflow" ||
3669 identifier == "__builtin_ssub_overflow" ||
3670 identifier == "__builtin_ssubl_overflow" ||
3671 identifier == "__builtin_ssubll_overflow" ||
3672 identifier == "__builtin_usub_overflow" ||
3673 identifier == "__builtin_usubl_overflow" ||
3674 identifier == "__builtin_usubll_overflow" ||
3675 identifier == "__builtin_sub_overflow_p")
3676 {
3678 }
3679 else if(
3680 identifier == "__builtin_mul_overflow" ||
3681 identifier == "__builtin_smul_overflow" ||
3682 identifier == "__builtin_smull_overflow" ||
3683 identifier == "__builtin_smulll_overflow" ||
3684 identifier == "__builtin_umul_overflow" ||
3685 identifier == "__builtin_umull_overflow" ||
3686 identifier == "__builtin_umulll_overflow" ||
3687 identifier == "__builtin_mul_overflow_p")
3688 {
3689 return typecheck_builtin_overflow(expr, ID_mult);
3690 }
3691 else if(
3692 identifier == "__builtin_bitreverse8" ||
3693 identifier == "__builtin_bitreverse16" ||
3694 identifier == "__builtin_bitreverse32" ||
3695 identifier == "__builtin_bitreverse64")
3696 {
3697 // clang only
3698 if(expr.arguments().size() != 1)
3699 {
3700 std::ostringstream error_message;
3701 error_message << "error: " << identifier << " expects one operand";
3703 error_message.str(), expr.source_location()};
3704 }
3705
3707
3709 bitreverse.add_source_location() = source_location;
3710
3711 return std::move(bitreverse);
3712 }
3713 else
3714 return nil_exprt();
3715 // NOLINTNEXTLINE(readability/fn_size)
3716}
3717
3720 const irep_idt &arith_op)
3721{
3722 const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
3723
3724 // check function signature
3725 if(expr.arguments().size() != 3)
3726 {
3727 std::ostringstream error_message;
3728 error_message << identifier << " takes exactly 3 arguments, but "
3729 << expr.arguments().size() << " were provided";
3731 error_message.str(), expr.source_location()};
3732 }
3733
3735
3736 auto lhs = expr.arguments()[0];
3737 auto rhs = expr.arguments()[1];
3738 auto result = expr.arguments()[2];
3739
3740 const bool is__p_variant = has_suffix(id2string(identifier), "_p");
3741
3742 {
3743 auto const raise_wrong_argument_error =
3744 [this, identifier](
3745 const exprt &wrong_argument, std::size_t argument_number, bool _p) {
3746 std::ostringstream error_message;
3747 error_message << "error: " << identifier << " has signature "
3748 << identifier << "(integral, integral, integral"
3749 << (_p ? "" : "*") << "), "
3750 << "but argument " << argument_number << " ("
3751 << expr2c(wrong_argument, *this) << ") has type `"
3752 << type2c(wrong_argument.type(), *this) << '`';
3754 error_message.str(), wrong_argument.source_location()};
3755 };
3756 for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3757 {
3758 auto const &argument = expr.arguments()[arg_index];
3759
3761 {
3763 }
3764 }
3765 if(
3766 !is__p_variant && (result.type().id() != ID_pointer ||
3768 to_pointer_type(result.type()).base_type())))
3769 {
3771 }
3772 }
3773
3775 std::move(lhs),
3776 std::move(rhs),
3777 std::move(result),
3778 expr.source_location()};
3779}
3780
3783{
3784 const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
3785
3786 // check function signature
3787 if(expr.arguments().size() != 2)
3788 {
3789 std::ostringstream error_message;
3790 error_message << "error: " << identifier
3791 << " takes exactly two arguments, but "
3792 << expr.arguments().size() << " were provided";
3794 error_message.str(), expr.source_location()};
3795 }
3796
3797 exprt result;
3798 if(identifier == CPROVER_PREFIX "saturating_minus")
3799 result = saturating_minus_exprt{expr.arguments()[0], expr.arguments()[1]};
3800 else if(identifier == CPROVER_PREFIX "saturating_plus")
3801 result = saturating_plus_exprt{expr.arguments()[0], expr.arguments()[1]};
3802 else
3804
3806 result.add_source_location() = expr.source_location();
3807
3808 return result;
3809}
3810
3815{
3816 const exprt &f_op=expr.function();
3817 const code_typet &code_type=to_code_type(f_op.type());
3818 exprt::operandst &arguments=expr.arguments();
3819 const code_typet::parameterst &parameters = code_type.parameters();
3820
3821 // no. of arguments test
3822
3823 if(code_type.get_bool(ID_C_incomplete))
3824 {
3825 // can't check
3826 }
3827 else if(code_type.is_KnR())
3828 {
3829 // We are generous on KnR; any number is ok.
3830 // We will fill in missing ones with "nondet".
3831 for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3832 {
3833 arguments.push_back(
3834 side_effect_expr_nondett{parameters[i].type(), expr.source_location()});
3835 }
3836 }
3837 else if(code_type.has_ellipsis())
3838 {
3839 if(parameters.size() > arguments.size())
3840 {
3842 error() << "not enough function arguments" << eom;
3843 throw 0;
3844 }
3845 }
3846 else if(parameters.size() != arguments.size())
3847 {
3849 error() << "wrong number of function arguments: "
3850 << "expected " << parameters.size() << ", but got "
3851 << arguments.size() << eom;
3852 throw 0;
3853 }
3854
3855 for(std::size_t i=0; i<arguments.size(); i++)
3856 {
3857 exprt &op=arguments[i];
3858
3859 if(op.is_nil())
3860 {
3861 // ignore
3862 }
3863 else if(i < parameters.size())
3864 {
3865 const code_typet::parametert &parameter = parameters[i];
3866
3867 if(
3868 parameter.is_boolean() && op.id() == ID_side_effect &&
3869 op.get(ID_statement) == ID_assign && op.type().id() != ID_bool)
3870 {
3872 warning() << "assignment where Boolean argument is expected" << eom;
3873 }
3874
3875 implicit_typecast(op, parameter.type());
3876 }
3877 else
3878 {
3879 // don't know type, just do standard conversion
3880
3881 if(op.type().id() == ID_array)
3882 {
3884 dest_type.base_type().set(ID_C_constant, true);
3886 }
3887 }
3888 }
3889}
3890
3892{
3893 // nothing to do
3894}
3895
3897{
3898 exprt &operand = to_unary_expr(expr).op();
3899
3900 const typet &o_type = operand.type();
3901
3902 if(o_type.id()==ID_vector)
3903 {
3904 if(is_number(to_vector_type(o_type).element_type()))
3905 {
3906 // Vector arithmetic.
3907 expr.type()=operand.type();
3908 return;
3909 }
3910 }
3911
3913
3914 if(is_number(operand.type()))
3915 {
3916 expr.type()=operand.type();
3917 return;
3918 }
3919
3921 error() << "operator '" << expr.id() << "' not defined for type '"
3922 << to_string(operand.type()) << "'" << eom;
3923 throw 0;
3924}
3925
3927{
3929
3930 // This is not quite accurate: the standard says the result
3931 // should be of type 'int'.
3932 // We do 'bool' anyway to get more compact formulae. Eventually,
3933 // this should be achieved by means of simplification, and not
3934 // in the frontend.
3935 expr.type()=bool_typet();
3936}
3937
3939 const vector_typet &type0,
3940 const vector_typet &type1)
3941{
3942 // This is relatively restrictive!
3943
3944 // compare dimension
3945 const auto s0 = numeric_cast<mp_integer>(type0.size());
3946 const auto s1 = numeric_cast<mp_integer>(type1.size());
3947 if(!s0.has_value())
3948 return false;
3949 if(!s1.has_value())
3950 return false;
3951 if(*s0 != *s1)
3952 return false;
3953
3954 // compare subtype
3955 if(
3956 (type0.element_type().id() == ID_signedbv ||
3957 type0.element_type().id() == ID_unsignedbv) &&
3958 (type1.element_type().id() == ID_signedbv ||
3959 type1.element_type().id() == ID_unsignedbv) &&
3960 to_bitvector_type(type0.element_type()).get_width() ==
3961 to_bitvector_type(type1.element_type()).get_width())
3962 return true;
3963
3964 return type0.element_type() == type1.element_type();
3965}
3966
3968{
3969 auto &binary_expr = to_binary_expr(expr);
3970 exprt &op0 = binary_expr.op0();
3971 exprt &op1 = binary_expr.op1();
3972
3973 const typet o_type0 = op0.type();
3974 const typet o_type1 = op1.type();
3975
3976 if(o_type0.id()==ID_vector &&
3977 o_type1.id()==ID_vector)
3978 {
3979 if(
3982 is_number(to_vector_type(o_type0).element_type()))
3983 {
3984 // Vector arithmetic has fairly strict typing rules, no promotion
3985 op1 = typecast_exprt::conditional_cast(op1, op0.type());
3986 expr.type()=op0.type();
3987 return;
3988 }
3989 }
3990 else if(
3991 o_type0.id() == ID_vector && o_type1.id() != ID_vector &&
3993 {
3994 // convert op1 to the vector type
3995 op1 = typecast_exprt(op1, o_type0);
3996 expr.type() = o_type0;
3997 return;
3998 }
3999 else if(
4000 o_type0.id() != ID_vector && o_type1.id() == ID_vector &&
4002 {
4003 // convert op0 to the vector type
4004 op0 = typecast_exprt(op0, o_type1);
4005 expr.type() = o_type1;
4006 return;
4007 }
4008
4009 if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
4010 {
4012 }
4013 else
4014 {
4015 // promote!
4017 }
4018
4019 const typet &type0 = op0.type();
4020 const typet &type1 = op1.type();
4021
4022 if(expr.id()==ID_plus || expr.id()==ID_minus ||
4023 expr.id()==ID_mult || expr.id()==ID_div)
4024 {
4025 if(type0.id()==ID_pointer || type1.id()==ID_pointer)
4026 {
4028 return;
4029 }
4030 else if(type0==type1)
4031 {
4032 if(is_number(type0))
4033 {
4034 expr.type()=type0;
4035 return;
4036 }
4037 }
4038 }
4039 else if(expr.id()==ID_mod)
4040 {
4041 if(type0==type1)
4042 {
4043 if(type0.id()==ID_signedbv || type0.id()==ID_unsignedbv)
4044 {
4045 expr.type()=type0;
4046 return;
4047 }
4048 }
4049 }
4050 else if(
4051 expr.id() == ID_bitand || expr.id() == ID_bitnand ||
4052 expr.id() == ID_bitxor || expr.id() == ID_bitor)
4053 {
4054 if(type0==type1)
4055 {
4056 if(is_number(type0))
4057 {
4058 expr.type()=type0;
4059 return;
4060 }
4061 else if(type0.id()==ID_bool)
4062 {
4063 if(expr.id()==ID_bitand)
4064 expr.id(ID_and);
4065 else if(expr.id() == ID_bitnand)
4066 expr.id(ID_nand);
4067 else if(expr.id()==ID_bitor)
4068 expr.id(ID_or);
4069 else if(expr.id()==ID_bitxor)
4070 expr.id(ID_xor);
4071 else
4073 expr.type()=type0;
4074 return;
4075 }
4076 }
4077 }
4078 else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
4079 {
4080 if(
4081 type0 == type1 &&
4082 (type0.id() == ID_signedbv || type0.id() == ID_unsignedbv))
4083 {
4084 expr.type() = type0;
4085 return;
4086 }
4087 }
4088
4090 error() << "operator '" << expr.id() << "' not defined for types '"
4091 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4092 << eom;
4093 throw 0;
4094}
4095
4097{
4098 PRECONDITION(expr.id() == ID_shl || expr.id() == ID_shr);
4099
4100 exprt &op0=expr.op0();
4101 exprt &op1=expr.op1();
4102
4103 const typet o_type0 = op0.type();
4104 const typet o_type1 = op1.type();
4105
4106 if(o_type0.id()==ID_vector &&
4107 o_type1.id()==ID_vector)
4108 {
4109 if(
4110 to_vector_type(o_type0).element_type() ==
4111 to_vector_type(o_type1).element_type() &&
4112 is_number(to_vector_type(o_type0).element_type()))
4113 {
4114 // {a0, a1, ..., an} >> {b0, b1, ..., bn} ==
4115 // {a0 >> b0, a1 >> b1, ..., an >> bn}
4116 // Fairly strict typing rules, no promotion
4117 expr.type()=op0.type();
4118 return;
4119 }
4120 }
4121
4122 if(
4123 o_type0.id() == ID_vector &&
4124 is_number(to_vector_type(o_type0).element_type()) && is_number(o_type1))
4125 {
4126 // {a0, a1, ..., an} >> b == {a0 >> b, a1 >> b, ..., an >> b}
4127 op1 = typecast_exprt(op1, o_type0);
4128 expr.type()=op0.type();
4129 return;
4130 }
4131
4132 // must do the promotions _separately_!
4135
4136 if(is_number(op0.type()) &&
4137 is_number(op1.type()))
4138 {
4139 expr.type()=op0.type();
4140
4141 if(expr.id()==ID_shr) // shifting operation depends on types
4142 {
4143 const typet &op0_type = op0.type();
4144
4145 if(op0_type.id()==ID_unsignedbv)
4146 {
4147 expr.id(ID_lshr);
4148 return;
4149 }
4150 else if(op0_type.id()==ID_signedbv)
4151 {
4152 expr.id(ID_ashr);
4153 return;
4154 }
4155 }
4156
4157 return;
4158 }
4159
4161 error() << "operator '" << expr.id() << "' not defined for types '"
4162 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4163 << eom;
4164 throw 0;
4165}
4166
4168{
4169 const typet &type=expr.type();
4170 PRECONDITION(type.id() == ID_pointer);
4171
4172 const typet &base_type = to_pointer_type(type).base_type();
4173
4174 if(
4175 base_type.id() == ID_struct_tag &&
4176 follow_tag(to_struct_tag_type(base_type)).is_incomplete())
4177 {
4179 error() << "pointer arithmetic with unknown object size" << eom;
4180 throw 0;
4181 }
4182 else if(
4183 base_type.id() == ID_union_tag &&
4184 follow_tag(to_union_tag_type(base_type)).is_incomplete())
4185 {
4187 error() << "pointer arithmetic with unknown object size" << eom;
4188 throw 0;
4189 }
4190 else if(
4191 base_type.id() == ID_empty &&
4193 {
4195 error() << "pointer arithmetic with unknown object size" << eom;
4196 throw 0;
4197 }
4198 else if(base_type.id() == ID_empty)
4199 {
4200 // This is a gcc extension.
4201 // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
4203 expr.swap(tc);
4204 }
4205}
4206
4208{
4209 auto &binary_expr = to_binary_expr(expr);
4210 exprt &op0 = binary_expr.op0();
4211 exprt &op1 = binary_expr.op1();
4212
4213 const typet &type0 = op0.type();
4214 const typet &type1 = op1.type();
4215
4216 if(expr.id()==ID_minus ||
4217 (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_minus))
4218 {
4219 if(type0.id()==ID_pointer &&
4220 type1.id()==ID_pointer)
4221 {
4222 if(type0 != type1)
4223 {
4225 "pointer subtraction over different types", expr.source_location()};
4226 }
4227 expr.type()=pointer_diff_type();
4230 return;
4231 }
4232
4233 if(type0.id()==ID_pointer &&
4234 (type1.id()==ID_bool ||
4235 type1.id()==ID_c_bool ||
4236 type1.id()==ID_unsignedbv ||
4237 type1.id()==ID_signedbv ||
4238 type1.id()==ID_c_bit_field ||
4239 type1.id()==ID_c_enum_tag))
4240 {
4242 make_index_type(op1);
4243 expr.type() = op0.type();
4244 return;
4245 }
4246 }
4247 else if(expr.id()==ID_plus ||
4248 (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_plus))
4249 {
4250 exprt *p_op, *int_op;
4251
4252 if(type0.id()==ID_pointer)
4253 {
4254 p_op=&op0;
4255 int_op=&op1;
4256 }
4257 else if(type1.id()==ID_pointer)
4258 {
4259 p_op=&op1;
4260 int_op=&op0;
4261 }
4262 else
4263 {
4264 p_op=int_op=nullptr;
4266 }
4267
4268 const typet &int_op_type = int_op->type();
4269
4270 if(int_op_type.id()==ID_bool ||
4271 int_op_type.id()==ID_c_bool ||
4272 int_op_type.id()==ID_unsignedbv ||
4273 int_op_type.id()==ID_signedbv ||
4276 {
4279 expr.type()=p_op->type();
4280 return;
4281 }
4282 }
4283
4284 irep_idt op_name;
4285
4286 if(expr.id()==ID_side_effect)
4287 op_name=to_side_effect_expr(expr).get_statement();
4288 else
4289 op_name=expr.id();
4290
4292 error() << "operator '" << op_name << "' not defined for types '"
4293 << to_string(type0) << "' and '" << to_string(type1) << "'" << eom;
4294 throw 0;
4295}
4296
4298{
4299 auto &binary_expr = to_binary_expr(expr);
4302
4303 // This is not quite accurate: the standard says the result
4304 // should be of type 'int'.
4305 // We do 'bool' anyway to get more compact formulae. Eventually,
4306 // this should be achieved by means of simplification, and not
4307 // in the frontend.
4308 expr.type()=bool_typet();
4309}
4310
4312 side_effect_exprt &expr)
4313{
4314 const irep_idt &statement=expr.get_statement();
4315
4316 auto &binary_expr = to_binary_expr(expr);
4317 exprt &op0 = binary_expr.op0();
4318 exprt &op1 = binary_expr.op1();
4319
4320 {
4321 const typet &type0=op0.type();
4322
4323 if(type0.id()==ID_empty)
4324 {
4326 error() << "cannot assign void" << eom;
4327 throw 0;
4328 }
4329
4330 if(!op0.get_bool(ID_C_lvalue))
4331 {
4333 error() << "assignment error: '" << to_string(op0) << "' not an lvalue"
4334 << eom;
4335 throw 0;
4336 }
4337
4338 if(type0.get_bool(ID_C_constant))
4339 {
4341 error() << "'" << to_string(op0) << "' is constant" << eom;
4342 throw 0;
4343 }
4344
4345 // refuse to assign arrays
4346 if(type0.id() == ID_array)
4347 {
4349 error() << "direct assignments to arrays not permitted" << eom;
4350 throw 0;
4351 }
4352 }
4353
4354 // Add a cast to the underlying type for bit fields.
4355 // In particular, sizeof(s.f=1) works for bit fields.
4356 if(op0.type().id()==ID_c_bit_field)
4357 op0 =
4358 typecast_exprt(op0, to_c_bit_field_type(op0.type()).underlying_type());
4359
4360 const typet o_type0=op0.type();
4361 const typet o_type1=op1.type();
4362
4363 expr.type()=o_type0;
4364
4365 if(statement==ID_assign)
4366 {
4368 return;
4369 }
4370 else if(statement==ID_assign_shl ||
4371 statement==ID_assign_shr)
4372 {
4373 if(o_type0.id() == ID_vector)
4374 {
4376
4377 if(
4378 o_type1.id() == ID_vector &&
4379 vector_o_type0.element_type() ==
4380 to_vector_type(o_type1).element_type() &&
4381 is_number(vector_o_type0.element_type()))
4382 {
4383 return;
4384 }
4385 else if(is_number(vector_o_type0.element_type()) && is_number(o_type1))
4386 {
4387 op1 = typecast_exprt(op1, o_type0);
4388 return;
4389 }
4390 }
4391
4394
4395 if(is_number(op0.type()) && is_number(op1.type()))
4396 {
4397 if(statement==ID_assign_shl)
4398 {
4399 return;
4400 }
4401 else // assign_shr
4402 {
4403 // distinguish arithmetic from logical shifts by looking at type
4404
4405 typet underlying_type=op0.type();
4406
4407 if(underlying_type.id()==ID_unsignedbv ||
4408 underlying_type.id()==ID_c_bool)
4409 {
4411 return;
4412 }
4413 else if(underlying_type.id()==ID_signedbv)
4414 {
4416 return;
4417 }
4418 }
4419 }
4420 }
4421 else if(statement==ID_assign_bitxor ||
4422 statement==ID_assign_bitand ||
4423 statement==ID_assign_bitor)
4424 {
4425 // these are more restrictive
4426 if(o_type0.id()==ID_bool ||
4427 o_type0.id()==ID_c_bool)
4428 {
4430 if(
4431 op1.is_boolean() || op1.type().id() == ID_c_bool ||
4432 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4433 op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
4434 {
4435 return;
4436 }
4437 }
4438 else if(o_type0.id()==ID_c_enum_tag ||
4439 o_type0.id()==ID_unsignedbv ||
4440 o_type0.id()==ID_signedbv ||
4441 o_type0.id()==ID_c_bit_field)
4442 {
4444 if(
4445 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4446 op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
4447 {
4448 return;
4449 }
4450 }
4451 else if(o_type0.id()==ID_vector &&
4452 o_type1.id()==ID_vector)
4453 {
4454 // We are willing to do a modest amount of conversion
4457 {
4459 return;
4460 }
4461 }
4462 else if(
4463 o_type0.id() == ID_vector &&
4464 (o_type1.id() == ID_bool || o_type1.id() == ID_c_bool ||
4465 o_type1.id() == ID_c_enum_tag || o_type1.id() == ID_unsignedbv ||
4466 o_type1.id() == ID_signedbv))
4467 {
4469 op1 = typecast_exprt(op1, o_type0);
4470 return;
4471 }
4472 }
4473 else
4474 {
4475 if(o_type0.id()==ID_pointer &&
4476 (statement==ID_assign_minus || statement==ID_assign_plus))
4477 {
4479 return;
4480 }
4481 else if(o_type0.id()==ID_vector &&
4482 o_type1.id()==ID_vector)
4483 {
4484 // We are willing to do a modest amount of conversion
4487 {
4489 return;
4490 }
4491 }
4492 else if(o_type0.id() == ID_vector)
4493 {
4495
4496 if(
4497 is_number(op1.type()) || op1.is_boolean() ||
4498 op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
4499 {
4500 op1 = typecast_exprt(op1, o_type0);
4501 return;
4502 }
4503 }
4504 else if(o_type0.id()==ID_bool ||
4505 o_type0.id()==ID_c_bool)
4506 {
4508 if(
4509 op1.is_boolean() || op1.type().id() == ID_c_bool ||
4510 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4511 op1.type().id() == ID_signedbv)
4512 {
4513 return;
4514 }
4515 }
4516 else
4517 {
4519
4520 if(
4521 is_number(op1.type()) || op1.is_boolean() ||
4522 op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
4523 {
4524 return;
4525 }
4526 }
4527 }
4528
4530 error() << "assignment '" << statement << "' not defined for types '"
4531 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4532 << eom;
4533
4534 throw 0;
4535}
4536
4541{
4542public:
4544 {
4545 }
4546
4548 bool operator()(const exprt &e) const
4549 {
4550 return is_constant(e);
4551 }
4552
4553protected:
4555
4558 bool is_constant(const exprt &e) const
4559 {
4560 if(e.id() == ID_infinity)
4561 return true;
4562
4563 if(e.is_constant())
4564 return true;
4565
4566 if(e.id() == ID_address_of)
4567 {
4568 return is_constant_address_of(to_address_of_expr(e).object());
4569 }
4570 else if(
4571 e.id() == ID_typecast || e.id() == ID_array_of || e.id() == ID_plus ||
4572 e.id() == ID_mult || e.id() == ID_array || e.id() == ID_with ||
4573 e.id() == ID_struct || e.id() == ID_union || e.id() == ID_empty_union ||
4574 e.id() == ID_equal || e.id() == ID_notequal || e.id() == ID_lt ||
4575 e.id() == ID_le || e.id() == ID_gt || e.id() == ID_ge ||
4576 e.id() == ID_if || e.id() == ID_not || e.id() == ID_and ||
4577 e.id() == ID_or || e.id() == ID_bitnot || e.id() == ID_bitand ||
4578 e.id() == ID_bitor || e.id() == ID_bitxor || e.id() == ID_vector)
4579 {
4580 return std::all_of(
4581 e.operands().begin(), e.operands().end(), [this](const exprt &op) {
4582 return is_constant(op);
4583 });
4584 }
4585
4586 return false;
4587 }
4588
4590 bool is_constant_address_of(const exprt &e) const
4591 {
4592 if(e.id() == ID_symbol)
4593 {
4594 return e.type().id() == ID_code ||
4595 ns.lookup(to_symbol_expr(e).get_identifier()).is_static_lifetime;
4596 }
4597 else if(e.id() == ID_array && e.get_bool(ID_C_string_constant))
4598 return true;
4599 else if(e.id() == ID_label)
4600 return true;
4601 else if(e.id() == ID_index)
4602 {
4604
4605 return is_constant_address_of(index_expr.array()) &&
4606 is_constant(index_expr.index());
4607 }
4608 else if(e.id() == ID_member)
4609 {
4610 return is_constant_address_of(to_member_expr(e).compound());
4611 }
4612 else if(e.id() == ID_dereference)
4613 {
4615
4616 return is_constant(deref.pointer());
4617 }
4618 else if(e.id() == ID_string_constant)
4619 return true;
4620
4621 return false;
4622 }
4623};
4624
4626{
4627 // Floating-point expressions may require a rounding mode.
4628 // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
4629 // Some compilers have command-line options to override.
4630 const auto rounding_mode =
4632 adjust_float_expressions(expr, rounding_mode);
4633
4634 simplify(expr, *this);
4635
4636 if(!is_compile_time_constantt(*this)(expr))
4637 {
4639 error() << "expected constant expression, but got '" << to_string(expr)
4640 << "'" << eom;
4641 throw 0;
4642 }
4643}
4644
4646{
4647 make_constant(expr);
4648 make_index_type(expr);
4649 simplify(expr, *this);
4650
4651 if(!is_compile_time_constantt(*this)(expr))
4652 {
4654 error() << "conversion to integer constant failed" << eom;
4655 throw 0;
4656 }
4657}
4658
4660 const exprt &expr,
4661 const irep_idt &id,
4662 const std::string &message) const
4663{
4664 if(!has_subexpr(expr, id))
4665 return;
4666
4668 error() << message << eom;
4669 throw 0;
4670}
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
API to expression classes that are internal to the C frontend.
ANSI-C Language Type Checking.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
bitvector_typet index_type()
Definition c_types.cpp:22
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:41
unsignedbv_typet size_type()
Definition c_types.cpp:55
empty_typet void_type()
Definition c_types.cpp:250
signedbv_typet signed_int_type()
Definition c_types.cpp:27
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
signedbv_typet pointer_diff_type()
Definition c_types.cpp:225
bitvector_typet char_type()
Definition c_types.cpp:111
floatbv_typet long_double_type()
Definition c_types.cpp:198
typet c_bool_type()
Definition c_types.cpp:105
bitvector_typet c_index_type()
Definition c_types.cpp:16
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition c_types.h:80
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Absolute value.
Definition std_expr.h:379
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
const declaratorst & declarators() const
A base class for binary expressions.
Definition std_expr.h:583
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:676
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
Reverse the order of bits in a bit-vector.
The Boolean type.
Definition std_types.h:36
The byte swap expression.
The type of C enums.
Definition c_types.h:239
static optionalt< std::string > check_address_can_be_taken(const typet &)
virtual void typecheck_obeys_contract_call(side_effect_expr_function_callt &expr)
Checks an obeys_contract predicate occurrence.
virtual void typecheck_expr_main(exprt &expr)
symbol_table_baset & symbol_table
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_alignof(exprt &expr)
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
virtual void typecheck_expr_rel_vector(binary_exprt &expr)
virtual void typecheck_expr_address_of(exprt &expr)
virtual void make_index_type(exprt &expr)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr_constant(exprt &expr)
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
virtual void adjust_float_rel(binary_relation_exprt &)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void typecheck_expr_sizeof(exprt &expr)
virtual optionalt< symbol_exprt > typecheck_shadow_memory_builtin(const side_effect_expr_function_callt &expr)
Typecheck the function if it is a shadow_memory builtin and return a symbol for it.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_shifts(shift_exprt &expr)
virtual void make_constant(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
exprt typecheck_saturating_arithmetic(const side_effect_expr_function_callt &expr)
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
static void add_rounding_mode(exprt &)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
virtual void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
asm_label_mapt asm_label_map
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
exprt typecheck_builtin_overflow(side_effect_expr_function_callt &expr, const irep_idt &arith_op)
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_expr_operands(exprt &expr)
virtual void typecheck_typed_target_call(side_effect_expr_function_callt &expr)
const irep_idt const irep_idt mode
virtual void make_constant_index(exprt &expr)
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...
virtual bool is_complete_type(const typet &type) const
id_type_mapt parameter_map
virtual void typecheck_expr_symbol(exprt &expr)
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_arithmetic_pointer(exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr)
virtual void typecheck_expr_member(exprt &expr)
virtual void typecheck_expr_dereference(exprt &expr)
virtual void typecheck_type(typet &type)
virtual void typecheck_expr_typecast(exprt &expr)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
virtual bool builtin_factory(const irep_idt &)
A codet representing sequential composition of program statements.
Definition std_code.h:130
static code_blockt from_list(const std::list< codet > &_list)
Definition std_code.h:148
A codet representing the declaration of a local variable.
Definition std_code.h:347
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
Data structure for representing an arbitrary statement in a program.
Imaginary part of the expression describing a complex number.
Definition std_expr.h:1971
Real part of the expression describing a complex number.
Definition std_expr.h:1926
Complex numbers made of pair of given subtype.
Definition std_types.h:1077
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition std_expr.h:2942
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool empty() const
Definition dstring.h:90
The empty type.
Definition std_types.h:51
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Definition c_expr.h:326
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:155
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
The Boolean constant false.
Definition std_expr.h:3017
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
A class for an expression that indicates a history variable.
Definition c_expr.h:205
IEEE-floating-point equality.
static ieee_float_spect single_precision()
Definition ieee_float.h:70
static ieee_float_spect double_precision()
Definition ieee_float.h:76
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:211
static ieee_floatt zero(const floatbv_typet &type)
Definition ieee_float.h:195
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
An expression denoting infinity.
Definition std_expr.h:3042
Thrown when we can't handle something in an input source file.
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:490
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
subt & get_sub()
Definition irep.h:456
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
bool is_nil() const
Definition irep.h:376
Architecturally similar to can_forward_propagatet, but specialized for what is a constexpr,...
is_compile_time_constantt(const namespacet &ns)
bool is_constant(const exprt &e) const
This function determines what expressions are to be propagated as "constants".
bool is_constant_address_of(const exprt &e) const
this function determines which reference-typed expressions are constant
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
A predicate that indicates that a zero-terminated string starts at the given address.
Evaluates to true if the operand is a pointer to a dynamic object.
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
A predicate that indicates that the object pointed to is live.
A type for mathematical functions (do not confuse with functions/methods in code)
source_locationt source_location
Definition message.h:247
mstreamt & error() const
Definition message.h:399
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
mstreamt & result() const
Definition message.h:409
static eomt eom
Definition message.h:297
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition namespace.cpp:97
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3026
The null pointer constant.
Expression for finding the size (in bytes) of the object a pointer points to.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition symbol.h:179
The plus expression Associativity is not specified.
Definition std_expr.h:947
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
The popcount (counting the number of bits set to 1) expression.
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition std_expr.h:517
A base class for a predicate that indicates that an address range is ok to read or write or both.
Saturating subtraction expression.
The saturating plus expression.
A predicate that indicates that the objects pointed to are distinct.
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
exprt::operandst & arguments()
Definition std_code.h:1718
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition c_expr.h:117
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:539
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_function() const
Base type for structs and unions.
Definition std_types.h:62
Expression to hold a symbol (variable)
Definition std_expr.h:113
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
bool is_macro
Definition symbol.h:62
bool is_static_lifetime
Definition symbol.h:70
bool is_parameter
Definition symbol.h:76
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
bool is_lvalue
Definition symbol.h:72
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:3008
Type with multiple subtypes.
Definition type.h:189
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
Union constructor from single element.
Definition std_expr.h:1708
The vector type.
Definition std_types.h:1008
A predicate that indicates that the object pointed to is writeable.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4144
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4160
#define Forall_operands(it, expr)
Definition expr.h:27
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition expr_util.cpp:24
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
mp_integer alignment(const typet &type, const namespacet &ns)
Definition padding.cpp:23
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:524
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition std_code.h:1669
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition std_code.h:429
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:77
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:840
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1102
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
Author: Diffblue Ltd.
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.
Type Naming for C.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175