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
2044{
2045 if(expr.operands().size()!=2)
2046 {
2048 error() << "function_call side effect expects two operands" << eom;
2049 throw 0;
2050 }
2051
2052 exprt &f_op=expr.function();
2053
2054 // f_op is not yet typechecked, in contrast to the other arguments.
2055 // This is a big special case!
2056
2057 if(f_op.id()==ID_symbol)
2058 {
2059 irep_idt identifier=to_symbol_expr(f_op).get_identifier();
2060
2061 asm_label_mapt::const_iterator entry=
2062 asm_label_map.find(identifier);
2063 if(entry!=asm_label_map.end())
2064 identifier=entry->second;
2065
2066 if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
2067 {
2068 // This is an undeclared function.
2069
2070 // Is it the polymorphic typed_target function ?
2071 if(identifier == CPROVER_PREFIX "typed_target")
2072 {
2074 }
2075 // Is this a builtin?
2076 else if(!builtin_factory(identifier, symbol_table, get_message_handler()))
2077 {
2078 // yes, it's a builtin
2079 }
2080 else if(
2081 identifier == "__noop" &&
2083 {
2084 // https://docs.microsoft.com/en-us/cpp/intrinsics/noop
2085 // typecheck and discard, just generating 0 instead
2086 for(auto &op : expr.arguments())
2087 typecheck_expr(op);
2088
2090 expr.swap(result);
2091
2092 return;
2093 }
2094 else if(
2095 identifier == "__builtin_shuffle" &&
2097 {
2099 expr.swap(result);
2100
2101 return;
2102 }
2103 else if(
2104 identifier == "__builtin_shufflevector" &&
2106 {
2108 expr.swap(result);
2109
2110 return;
2111 }
2112 else if(
2113 identifier == CPROVER_PREFIX "saturating_minus" ||
2114 identifier == CPROVER_PREFIX "saturating_plus")
2115 {
2117 expr.swap(result);
2118
2119 return;
2120 }
2121 else if(identifier == CPROVER_PREFIX "equal")
2122 {
2123 if(expr.arguments().size() != 2)
2124 {
2125 error().source_location = f_op.source_location();
2126 error() << "equal expects two operands" << eom;
2127 throw 0;
2128 }
2129
2131 expr.arguments().front(), expr.arguments().back());
2132 equality_expr.add_source_location() = expr.source_location();
2133
2134 if(equality_expr.lhs().type() != equality_expr.rhs().type())
2135 {
2136 error().source_location = f_op.source_location();
2137 error() << "equal expects two operands of same type" << eom;
2138 throw 0;
2139 }
2140
2141 expr.swap(equality_expr);
2142 return;
2143 }
2144 else if(
2145 identifier == CPROVER_PREFIX "overflow_minus" ||
2146 identifier == CPROVER_PREFIX "overflow_mult" ||
2147 identifier == CPROVER_PREFIX "overflow_plus" ||
2148 identifier == CPROVER_PREFIX "overflow_shl")
2149 {
2150 exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
2151 overflow.add_source_location() = f_op.source_location();
2152
2153 if(identifier == CPROVER_PREFIX "overflow_minus")
2154 {
2155 overflow.id(ID_minus);
2157 }
2158 else if(identifier == CPROVER_PREFIX "overflow_mult")
2159 {
2160 overflow.id(ID_mult);
2162 }
2163 else if(identifier == CPROVER_PREFIX "overflow_plus")
2164 {
2165 overflow.id(ID_plus);
2167 }
2168 else if(identifier == CPROVER_PREFIX "overflow_shl")
2169 {
2170 overflow.id(ID_shl);
2172 }
2173
2175 overflow.operands()[0], overflow.id(), overflow.operands()[1]};
2176 of.add_source_location() = overflow.source_location();
2177 expr.swap(of);
2178 return;
2179 }
2180 else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
2181 {
2183 tmp.add_source_location() = f_op.source_location();
2184
2186
2187 unary_minus_overflow_exprt overflow{tmp.operands().front()};
2188 overflow.add_source_location() = tmp.source_location();
2189 expr.swap(overflow);
2190 return;
2191 }
2192 else if(identifier == CPROVER_PREFIX "enum_is_in_range")
2193 {
2194 // Check correct number of arguments
2195 if(expr.arguments().size() != 1)
2196 {
2197 std::ostringstream error_message;
2198 error_message << identifier << " takes exactly 1 argument, but "
2199 << expr.arguments().size() << " were provided";
2201 error_message.str(), expr.source_location()};
2202 }
2203 const auto &arg1 = expr.arguments()[0];
2205 {
2206 // Can't enum range check a non-enum
2207 std::ostringstream error_message;
2208 error_message << identifier << " expects enum, but ("
2209 << expr2c(arg1, *this) << ") has type `"
2210 << type2c(arg1.type(), *this) << '`';
2212 error_message.str(), expr.source_location()};
2213 }
2214
2216 in_range.add_source_location() = expr.source_location();
2217 exprt lowered = in_range.lower(*this);
2218 expr.swap(lowered);
2219 return;
2220 }
2221 else if(
2222 identifier == CPROVER_PREFIX "r_ok" ||
2223 identifier == CPROVER_PREFIX "w_ok" ||
2224 identifier == CPROVER_PREFIX "rw_ok")
2225 {
2226 if(expr.arguments().size() != 1 && expr.arguments().size() != 2)
2227 {
2229 id2string(identifier) + " expects one or two operands",
2230 f_op.source_location()};
2231 }
2232
2233 // the first argument must be a pointer
2234 auto &pointer_expr = expr.arguments()[0];
2235 if(pointer_expr.type().id() == ID_array)
2236 {
2238 dest_type.base_type().set(ID_C_constant, true);
2239 implicit_typecast(pointer_expr, dest_type);
2240 }
2241 else if(pointer_expr.type().id() != ID_pointer)
2242 {
2244 id2string(identifier) + " expects a pointer as first argument",
2245 f_op.source_location()};
2246 }
2247
2248 // The second argument, when given, is a size_t.
2249 // When not given, use the pointer subtype.
2251
2252 if(expr.arguments().size() == 2)
2253 {
2255 size_expr = expr.arguments()[1];
2256 }
2257 else
2258 {
2259 // Won't do void *
2260 const auto &subtype =
2261 to_pointer_type(pointer_expr.type()).base_type();
2262 if(subtype.id() == ID_empty)
2263 {
2265 id2string(identifier) +
2266 " expects a size when given a void pointer",
2267 f_op.source_location()};
2268 }
2269
2270 auto size_expr_opt = size_of_expr(subtype, *this);
2271 CHECK_RETURN(size_expr_opt.has_value());
2272 size_expr = std::move(size_expr_opt.value());
2273 }
2274
2275 irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok
2276 : identifier == CPROVER_PREFIX "w_ok" ? ID_w_ok
2277 : ID_rw_ok;
2278
2279 r_or_w_ok_exprt ok_expr(id, pointer_expr, size_expr);
2280 ok_expr.add_source_location() = expr.source_location();
2281
2282 expr.swap(ok_expr);
2283 return;
2284 }
2285 else if(
2287 {
2289 shadow_memory_builtin->get_identifier();
2290
2291 const auto builtin_code_type =
2293
2294 INVARIANT(
2295 builtin_code_type.has_ellipsis() &&
2296 builtin_code_type.parameters().empty(),
2297 "Shadow memory builtins should be an ellipsis with 0 parameter");
2298
2299 // Add the symbol to the symbol table if it is not present yet.
2301 {
2302 symbolt new_symbol{
2304 new_symbol.base_name = shadow_memory_builtin_id;
2305 new_symbol.location = f_op.source_location();
2306 // Add an empty implementation to avoid warnings about missing
2307 // implementation later on
2308 new_symbol.value = code_blockt{};
2309
2310 symbol_table.add(new_symbol);
2311 }
2312
2313 // Swap the current `function` field with the newly generated
2314 // `shadow_memory_builtin` `symbol_exprt` and carry on with typechecking
2315 f_op = std::move(*shadow_memory_builtin);
2316 }
2317 else if(
2319 identifier, expr.arguments(), f_op.source_location()))
2320 {
2321 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
2322 auto &parameters = to_code_type(gcc_polymorphic->type()).parameters();
2323 INVARIANT(
2324 !parameters.empty(),
2325 "GCC polymorphic built-ins should have at least one parameter");
2326
2327 // For all atomic/sync polymorphic built-ins (which are the ones handled
2328 // by typecheck_gcc_polymorphic_builtin), looking at the first parameter
2329 // suffices to distinguish different implementations.
2330 if(parameters.front().type().id() == ID_pointer)
2331 {
2333 id2string(identifier) + "_" +
2335 to_pointer_type(parameters.front().type()).base_type(), *this);
2336 }
2337 else
2338 {
2340 id2string(identifier) + "_" +
2341 type_to_partial_identifier(parameters.front().type(), *this);
2342 }
2343 gcc_polymorphic->set_identifier(identifier_with_type);
2344
2346 {
2347 for(std::size_t i = 0; i < parameters.size(); ++i)
2348 {
2349 const std::string base_name = "p_" + std::to_string(i);
2350
2351 parameter_symbolt new_symbol;
2352
2353 new_symbol.name =
2354 id2string(identifier_with_type) + "::" + base_name;
2355 new_symbol.base_name = base_name;
2356 new_symbol.location = f_op.source_location();
2357 new_symbol.type = parameters[i].type();
2358 new_symbol.is_parameter = true;
2359 new_symbol.is_lvalue = true;
2360 new_symbol.mode = ID_C;
2361
2362 parameters[i].set_identifier(new_symbol.name);
2363 parameters[i].set_base_name(new_symbol.base_name);
2364
2365 symbol_table.add(new_symbol);
2366 }
2367
2368 symbolt new_symbol{
2370 new_symbol.base_name = identifier_with_type;
2371 new_symbol.location = f_op.source_location();
2372 code_blockt implementation =
2375 return_type = to_code_type(gcc_polymorphic->type()).return_type();
2376 typecheck_code(implementation);
2378 new_symbol.value = implementation;
2379
2380 symbol_table.add(new_symbol);
2381 }
2382
2383 f_op = std::move(*gcc_polymorphic);
2384 }
2385 else
2386 {
2387 // This is an undeclared function that's not a builtin.
2388 // Let's just add it.
2389 // We do a bit of return-type guessing, but just a bit.
2391
2392 // The following isn't really right and sound, but there
2393 // are too many idiots out there who use malloc and the like
2394 // without the right header file.
2395 if(identifier=="malloc" ||
2396 identifier=="realloc" ||
2397 identifier=="reallocf" ||
2398 identifier=="valloc")
2399 {
2401 }
2402
2403 symbolt new_symbol{
2404 identifier, code_typet({}, guessed_return_type), mode};
2405 new_symbol.base_name=identifier;
2406 new_symbol.location=expr.source_location();
2407 new_symbol.type.set(ID_C_incomplete, true);
2408
2409 // TODO: should also guess some argument types
2410
2412 move_symbol(new_symbol, symbol_ptr);
2413
2414 warning().source_location=f_op.find_source_location();
2415 warning() << "function '" << identifier << "' is not declared" << eom;
2416 }
2417 }
2418 }
2419
2420 // typecheck it now
2422
2423 const typet f_op_type = f_op.type();
2424
2426 {
2427 const auto &mathematical_function_type =
2429
2430 // check number of arguments
2431 if(expr.arguments().size() != mathematical_function_type.domain().size())
2432 {
2433 error().source_location = f_op.source_location();
2434 error() << "expected " << mathematical_function_type.domain().size()
2435 << " arguments but got " << expr.arguments().size() << eom;
2436 throw 0;
2437 }
2438
2439 // check the types of the arguments
2440 for(auto &p :
2441 make_range(expr.arguments()).zip(mathematical_function_type.domain()))
2442 {
2443 if(p.first.type() != p.second)
2444 {
2445 error().source_location = p.first.source_location();
2446 error() << "expected argument of type " << to_string(p.second)
2447 << " but got " << to_string(p.first.type()) << eom;
2448 throw 0;
2449 }
2450 }
2451
2452 function_application_exprt function_application(f_op, expr.arguments());
2453
2454 function_application.add_source_location() = expr.source_location();
2455
2456 expr.swap(function_application);
2457 return;
2458 }
2459
2460 if(f_op_type.id()!=ID_pointer)
2461 {
2462 error().source_location = f_op.source_location();
2463 error() << "expected function/function pointer as argument but got '"
2464 << to_string(f_op_type) << "'" << eom;
2465 throw 0;
2466 }
2467
2468 // do implicit dereference
2469 if(f_op.id() == ID_address_of && f_op.get_bool(ID_C_implicit))
2470 {
2471 f_op = to_address_of_expr(f_op).object();
2472 }
2473 else
2474 {
2476 tmp.set(ID_C_implicit, true);
2477 tmp.add_source_location()=f_op.source_location();
2478 f_op.swap(tmp);
2479 }
2480
2481 if(f_op.type().id()!=ID_code)
2482 {
2483 error().source_location = f_op.source_location();
2484 error() << "expected code as argument" << eom;
2485 throw 0;
2486 }
2487
2488 const code_typet &code_type=to_code_type(f_op.type());
2489
2490 expr.type()=code_type.return_type();
2491
2493
2494 if(tmp.is_not_nil())
2495 expr.swap(tmp);
2496 else
2498}
2499
2502{
2503 const exprt &f_op=expr.function();
2504 const source_locationt &source_location=expr.source_location();
2505
2506 // some built-in functions
2507 if(f_op.id()!=ID_symbol)
2508 return nil_exprt();
2509
2510 const irep_idt &identifier=to_symbol_expr(f_op).get_identifier();
2511
2512 if(identifier == CPROVER_PREFIX "is_fresh")
2513 {
2514 if(expr.arguments().size() != 2)
2515 {
2516 error().source_location = f_op.source_location();
2517 error() << CPROVER_PREFIX "is_fresh expects two operands; "
2518 << expr.arguments().size() << "provided." << eom;
2519 throw 0;
2520 }
2522 return nil_exprt();
2523 }
2524 else if(identifier == CPROVER_PREFIX "obeys_contract")
2525 {
2527 // returning nil leaves the call expression in place
2528 return nil_exprt();
2529 }
2530 else if(identifier == CPROVER_PREFIX "pointer_in_range_dfcc")
2531 {
2532 // same as pointer_in_range with experimental support for DFCC contracts
2533 // -- do not use
2534 if(expr.arguments().size() != 3)
2535 {
2537 CPROVER_PREFIX "pointer_in_range_dfcc expects three arguments",
2538 expr.source_location()};
2539 }
2540
2541 for(const auto &arg : expr.arguments())
2542 {
2543 if(arg.type().id() != ID_pointer)
2544 {
2547 "pointer_in_range_dfcc expects pointer-typed arguments",
2548 arg.source_location()};
2549 }
2550 }
2551 return nil_exprt();
2552 }
2553 else if(identifier == CPROVER_PREFIX "same_object")
2554 {
2555 if(expr.arguments().size()!=2)
2556 {
2557 error().source_location = f_op.source_location();
2558 error() << "same_object expects two operands" << eom;
2559 throw 0;
2560 }
2561
2563
2565 same_object(expr.arguments()[0], expr.arguments()[1]);
2566 same_object_expr.add_source_location()=source_location;
2567
2568 return same_object_expr;
2569 }
2570 else if(identifier==CPROVER_PREFIX "get_must")
2571 {
2572 if(expr.arguments().size()!=2)
2573 {
2574 error().source_location = f_op.source_location();
2575 error() << "get_must expects two operands" << eom;
2576 throw 0;
2577 }
2578
2580
2582 expr.arguments()[0], ID_get_must, expr.arguments()[1]);
2583 get_must_expr.add_source_location()=source_location;
2584
2585 return std::move(get_must_expr);
2586 }
2587 else if(identifier==CPROVER_PREFIX "get_may")
2588 {
2589 if(expr.arguments().size()!=2)
2590 {
2591 error().source_location = f_op.source_location();
2592 error() << "get_may expects two operands" << eom;
2593 throw 0;
2594 }
2595
2597
2599 expr.arguments()[0], ID_get_may, expr.arguments()[1]);
2600 get_may_expr.add_source_location()=source_location;
2601
2602 return std::move(get_may_expr);
2603 }
2604 else if(identifier == CPROVER_PREFIX "is_invalid_pointer")
2605 {
2606 if(expr.arguments().size()!=1)
2607 {
2608 error().source_location = f_op.source_location();
2609 error() << "is_invalid_pointer expects one operand" << eom;
2610 throw 0;
2611 }
2612
2614
2616 same_object_expr.add_source_location()=source_location;
2617
2618 return same_object_expr;
2619 }
2620 else if(identifier==CPROVER_PREFIX "buffer_size")
2621 {
2622 if(expr.arguments().size()!=1)
2623 {
2624 error().source_location = f_op.source_location();
2625 error() << "buffer_size expects one operand" << eom;
2626 throw 0;
2627 }
2628
2630
2631 exprt buffer_size_expr("buffer_size", size_type());
2632 buffer_size_expr.operands()=expr.arguments();
2633 buffer_size_expr.add_source_location()=source_location;
2634
2635 return buffer_size_expr;
2636 }
2637 else if(identifier == CPROVER_PREFIX "is_list")
2638 {
2639 // experimental feature for CHC encodings -- do not use
2640 if(expr.arguments().size() != 1)
2641 {
2642 error().source_location = f_op.source_location();
2643 error() << "is_list expects one operand" << eom;
2644 throw 0;
2645 }
2646
2648
2649 if(
2650 expr.arguments()[0].type().id() != ID_pointer ||
2651 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2653 {
2654 error().source_location = expr.arguments()[0].source_location();
2655 error() << "is_list expects a struct-pointer operand" << eom;
2656 throw 0;
2657 }
2658
2659 predicate_exprt is_list_expr("is_list");
2660 is_list_expr.operands() = expr.arguments();
2661 is_list_expr.add_source_location() = source_location;
2662
2663 return std::move(is_list_expr);
2664 }
2665 else if(identifier == CPROVER_PREFIX "is_dll")
2666 {
2667 // experimental feature for CHC encodings -- do not use
2668 if(expr.arguments().size() != 1)
2669 {
2670 error().source_location = f_op.source_location();
2671 error() << "is_dll expects one operand" << eom;
2672 throw 0;
2673 }
2674
2676
2677 if(
2678 expr.arguments()[0].type().id() != ID_pointer ||
2679 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2681 {
2682 error().source_location = expr.arguments()[0].source_location();
2683 error() << "is_dll expects a struct-pointer operand" << eom;
2684 throw 0;
2685 }
2686
2687 predicate_exprt is_dll_expr("is_dll");
2688 is_dll_expr.operands() = expr.arguments();
2689 is_dll_expr.add_source_location() = source_location;
2690
2691 return std::move(is_dll_expr);
2692 }
2693 else if(identifier == CPROVER_PREFIX "is_cyclic_dll")
2694 {
2695 // experimental feature for CHC encodings -- do not use
2696 if(expr.arguments().size() != 1)
2697 {
2698 error().source_location = f_op.source_location();
2699 error() << "is_cyclic_dll expects one operand" << eom;
2700 throw 0;
2701 }
2702
2704
2705 if(
2706 expr.arguments()[0].type().id() != ID_pointer ||
2707 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2709 {
2710 error().source_location = expr.arguments()[0].source_location();
2711 error() << "is_cyclic_dll expects a struct-pointer operand" << eom;
2712 throw 0;
2713 }
2714
2715 predicate_exprt is_cyclic_dll_expr("is_cyclic_dll");
2716 is_cyclic_dll_expr.operands() = expr.arguments();
2717 is_cyclic_dll_expr.add_source_location() = source_location;
2718
2719 return std::move(is_cyclic_dll_expr);
2720 }
2721 else if(identifier == CPROVER_PREFIX "is_sentinel_dll")
2722 {
2723 // experimental feature for CHC encodings -- do not use
2724 if(expr.arguments().size() != 2 && expr.arguments().size() != 3)
2725 {
2726 error().source_location = f_op.source_location();
2727 error() << "is_sentinel_dll expects two or three operands" << eom;
2728 throw 0;
2729 }
2730
2732
2734 args_no_cast.reserve(expr.arguments().size());
2735 for(const auto &argument : expr.arguments())
2736 {
2738 if(
2739 args_no_cast.back().type().id() != ID_pointer ||
2740 to_pointer_type(args_no_cast.back().type()).base_type().id() !=
2742 {
2743 error().source_location = expr.arguments()[0].source_location();
2744 error() << "is_sentinel_dll_node expects struct-pointer operands"
2745 << eom;
2746 throw 0;
2747 }
2748 }
2749
2750 predicate_exprt is_sentinel_dll_expr("is_sentinel_dll");
2752 is_sentinel_dll_expr.add_source_location() = source_location;
2753
2754 return std::move(is_sentinel_dll_expr);
2755 }
2756 else if(identifier == CPROVER_PREFIX "is_cstring")
2757 {
2758 // experimental feature for CHC encodings -- do not use
2759 if(expr.arguments().size() != 1)
2760 {
2761 error().source_location = f_op.source_location();
2762 error() << "is_cstring expects one operand" << eom;
2763 throw 0;
2764 }
2765
2767
2768 if(expr.arguments()[0].type().id() != ID_pointer)
2769 {
2770 error().source_location = expr.arguments()[0].source_location();
2771 error() << "is_cstring expects a pointer operand" << eom;
2772 throw 0;
2773 }
2774
2776 is_cstring_expr.add_source_location() = source_location;
2777
2778 return std::move(is_cstring_expr);
2779 }
2780 else if(identifier == CPROVER_PREFIX "cstrlen")
2781 {
2782 // experimental feature for CHC encodings -- do not use
2783 if(expr.arguments().size() != 1)
2784 {
2785 error().source_location = f_op.source_location();
2786 error() << "cstrlen expects one operand" << eom;
2787 throw 0;
2788 }
2789
2791
2792 if(expr.arguments()[0].type().id() != ID_pointer)
2793 {
2794 error().source_location = expr.arguments()[0].source_location();
2795 error() << "cstrlen expects a pointer operand" << eom;
2796 throw 0;
2797 }
2798
2800 cstrlen_expr.add_source_location() = source_location;
2801
2802 return std::move(cstrlen_expr);
2803 }
2804 else if(identifier==CPROVER_PREFIX "is_zero_string")
2805 {
2806 if(expr.arguments().size()!=1)
2807 {
2808 error().source_location = f_op.source_location();
2809 error() << "is_zero_string expects one operand" << eom;
2810 throw 0;
2811 }
2812
2814
2816 "is_zero_string", expr.arguments()[0], c_bool_type());
2817 is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
2818 is_zero_string_expr.add_source_location()=source_location;
2819
2820 return std::move(is_zero_string_expr);
2821 }
2822 else if(identifier==CPROVER_PREFIX "zero_string_length")
2823 {
2824 if(expr.arguments().size()!=1)
2825 {
2826 error().source_location = f_op.source_location();
2827 error() << "zero_string_length expects one operand" << eom;
2828 throw 0;
2829 }
2830
2832
2833 exprt zero_string_length_expr("zero_string_length", size_type());
2834 zero_string_length_expr.operands()=expr.arguments();
2835 zero_string_length_expr.set(ID_C_lvalue, true); // make it an lvalue
2836 zero_string_length_expr.add_source_location()=source_location;
2837
2839 }
2840 else if(identifier==CPROVER_PREFIX "DYNAMIC_OBJECT")
2841 {
2842 if(expr.arguments().size()!=1)
2843 {
2844 error().source_location = f_op.source_location();
2845 error() << "dynamic_object expects one argument" << eom;
2846 throw 0;
2847 }
2848
2850
2852 is_dynamic_object_expr.add_source_location() = source_location;
2853
2855 }
2856 else if(identifier == CPROVER_PREFIX "LIVE_OBJECT")
2857 {
2858 if(expr.arguments().size() != 1)
2859 {
2860 error().source_location = f_op.source_location();
2861 error() << "live_object expects one argument" << eom;
2862 throw 0;
2863 }
2864
2866
2868 live_object_expr.add_source_location() = source_location;
2869
2870 return live_object_expr;
2871 }
2872 else if(identifier == CPROVER_PREFIX "pointer_in_range")
2873 {
2874 if(expr.arguments().size() != 3)
2875 {
2876 error().source_location = f_op.source_location();
2877 error() << "pointer_in_range expects three arguments" << eom;
2878 throw 0;
2879 }
2880
2882
2884 expr.arguments()[0], expr.arguments()[1], expr.arguments()[2]);
2885 pointer_in_range_expr.add_source_location() = source_location;
2886
2887 return pointer_in_range_expr;
2888 }
2889 else if(identifier == CPROVER_PREFIX "WRITEABLE_OBJECT")
2890 {
2891 if(expr.arguments().size() != 1)
2892 {
2893 error().source_location = f_op.source_location();
2894 error() << "writeable_object expects one argument" << eom;
2895 throw 0;
2896 }
2897
2899
2901 writeable_object_expr.add_source_location() = source_location;
2902
2903 return writeable_object_expr;
2904 }
2905 else if(identifier == CPROVER_PREFIX "separate")
2906 {
2907 // experimental feature for CHC encodings -- do not use
2908 if(expr.arguments().size() < 2)
2909 {
2910 error().source_location = f_op.source_location();
2911 error() << "separate expects two or more arguments" << eom;
2912 throw 0;
2913 }
2914
2916
2918 separate_expr.add_source_location() = source_location;
2919
2920 return separate_expr;
2921 }
2922 else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
2923 {
2924 if(expr.arguments().size()!=1)
2925 {
2926 error().source_location = f_op.source_location();
2927 error() << "pointer_offset expects one argument" << eom;
2928 throw 0;
2929 }
2930
2932
2934 pointer_offset_expr.add_source_location()=source_location;
2935
2937 }
2938 else if(identifier == CPROVER_PREFIX "OBJECT_SIZE")
2939 {
2940 if(expr.arguments().size() != 1)
2941 {
2942 error().source_location = f_op.source_location();
2943 error() << "object_size expects one operand" << eom;
2944 throw 0;
2945 }
2946
2948
2950 object_size_expr.add_source_location() = source_location;
2951
2952 return std::move(object_size_expr);
2953 }
2954 else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
2955 {
2956 if(expr.arguments().size()!=1)
2957 {
2958 error().source_location = f_op.source_location();
2959 error() << "pointer_object expects one argument" << eom;
2960 throw 0;
2961 }
2962
2964
2966 pointer_object_expr.add_source_location() = source_location;
2967
2969 }
2970 else if(identifier=="__builtin_bswap16" ||
2971 identifier=="__builtin_bswap32" ||
2972 identifier=="__builtin_bswap64")
2973 {
2974 if(expr.arguments().size()!=1)
2975 {
2976 error().source_location = f_op.source_location();
2977 error() << identifier << " expects one operand" << eom;
2978 throw 0;
2979 }
2980
2982
2983 // these are hard-wired to 8 bits according to the gcc manual
2984 bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
2985 bswap_expr.add_source_location()=source_location;
2986
2987 return std::move(bswap_expr);
2988 }
2989 else if(
2990 identifier == "__builtin_rotateleft8" ||
2991 identifier == "__builtin_rotateleft16" ||
2992 identifier == "__builtin_rotateleft32" ||
2993 identifier == "__builtin_rotateleft64" ||
2994 identifier == "__builtin_rotateright8" ||
2995 identifier == "__builtin_rotateright16" ||
2996 identifier == "__builtin_rotateright32" ||
2997 identifier == "__builtin_rotateright64")
2998 {
2999 // clang only
3000 if(expr.arguments().size() != 2)
3001 {
3002 error().source_location = f_op.source_location();
3003 error() << identifier << " expects two operands" << eom;
3004 throw 0;
3005 }
3006
3008
3009 irep_idt id = (identifier == "__builtin_rotateleft8" ||
3010 identifier == "__builtin_rotateleft16" ||
3011 identifier == "__builtin_rotateleft32" ||
3012 identifier == "__builtin_rotateleft64")
3013 ? ID_rol
3014 : ID_ror;
3015
3016 shift_exprt rotate_expr(expr.arguments()[0], id, expr.arguments()[1]);
3017 rotate_expr.add_source_location() = source_location;
3018
3019 return std::move(rotate_expr);
3020 }
3021 else if(identifier=="__builtin_nontemporal_load")
3022 {
3023 if(expr.arguments().size()!=1)
3024 {
3025 error().source_location = f_op.source_location();
3026 error() << identifier << " expects one operand" << eom;
3027 throw 0;
3028 }
3029
3031
3032 // these return the subtype of the argument
3033 exprt &ptr_arg=expr.arguments().front();
3034
3035 if(ptr_arg.type().id()!=ID_pointer)
3036 {
3037 error().source_location = f_op.source_location();
3038 error() << "__builtin_nontemporal_load takes pointer as argument" << eom;
3039 throw 0;
3040 }
3041
3042 expr.type() = to_pointer_type(expr.arguments().front().type()).base_type();
3043
3044 return expr;
3045 }
3046 else if(
3047 identifier == "__builtin_fpclassify" ||
3048 identifier == CPROVER_PREFIX "fpclassify")
3049 {
3050 if(expr.arguments().size() != 6)
3051 {
3052 error().source_location = f_op.source_location();
3053 error() << identifier << " expects six arguments" << eom;
3054 throw 0;
3055 }
3056
3058
3059 // This gets 5 integers followed by a float or double.
3060 // The five integers are the return values for the cases
3061 // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
3062 // gcc expects this to be able to produce compile-time constants.
3063
3064 const exprt &fp_value = expr.arguments()[5];
3065
3066 if(fp_value.type().id() != ID_floatbv)
3067 {
3068 error().source_location = fp_value.source_location();
3069 error() << "non-floating-point argument for " << identifier << eom;
3070 throw 0;
3071 }
3072
3073 const auto &floatbv_type = to_floatbv_type(fp_value.type());
3074
3075 const exprt zero = ieee_floatt::zero(floatbv_type).to_expr();
3076
3077 const auto &arguments = expr.arguments();
3078
3079 return if_exprt(
3081 arguments[0],
3082 if_exprt(
3084 arguments[1],
3085 if_exprt(
3087 arguments[2],
3088 if_exprt(
3090 arguments[4],
3091 arguments[3])))); // subnormal
3092 }
3093 else if(identifier==CPROVER_PREFIX "isnanf" ||
3094 identifier==CPROVER_PREFIX "isnand" ||
3095 identifier==CPROVER_PREFIX "isnanld" ||
3096 identifier=="__builtin_isnan")
3097 {
3098 if(expr.arguments().size()!=1)
3099 {
3100 error().source_location = f_op.source_location();
3101 error() << "isnan expects one operand" << eom;
3102 throw 0;
3103 }
3104
3106
3107 isnan_exprt isnan_expr(expr.arguments().front());
3108 isnan_expr.add_source_location()=source_location;
3109
3111 }
3112 else if(identifier==CPROVER_PREFIX "isfinitef" ||
3113 identifier==CPROVER_PREFIX "isfinited" ||
3114 identifier==CPROVER_PREFIX "isfiniteld")
3115 {
3116 if(expr.arguments().size()!=1)
3117 {
3118 error().source_location = f_op.source_location();
3119 error() << "isfinite expects one operand" << eom;
3120 throw 0;
3121 }
3122
3124
3125 isfinite_exprt isfinite_expr(expr.arguments().front());
3126 isfinite_expr.add_source_location()=source_location;
3127
3129 }
3130 else if(identifier==CPROVER_PREFIX "inf" ||
3131 identifier=="__builtin_inf")
3132 {
3136 inf_expr.add_source_location()=source_location;
3137
3138 return std::move(inf_expr);
3139 }
3140 else if(identifier==CPROVER_PREFIX "inff")
3141 {
3145 inff_expr.add_source_location()=source_location;
3146
3147 return std::move(inff_expr);
3148 }
3149 else if(identifier==CPROVER_PREFIX "infl")
3150 {
3154 infl_expr.add_source_location()=source_location;
3155
3156 return std::move(infl_expr);
3157 }
3158 else if(
3159 identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
3160 identifier == CPROVER_PREFIX "llabs" ||
3161 identifier == CPROVER_PREFIX "imaxabs" ||
3162 identifier == CPROVER_PREFIX "fabs" ||
3163 identifier == CPROVER_PREFIX "fabsf" ||
3164 identifier == CPROVER_PREFIX "fabsl")
3165 {
3166 if(expr.arguments().size()!=1)
3167 {
3168 error().source_location = f_op.source_location();
3169 error() << "abs-functions expect one operand" << eom;
3170 throw 0;
3171 }
3172
3174
3175 abs_exprt abs_expr(expr.arguments().front());
3176 abs_expr.add_source_location()=source_location;
3177
3178 return std::move(abs_expr);
3179 }
3180 else if(
3181 identifier == CPROVER_PREFIX "fmod" ||
3182 identifier == CPROVER_PREFIX "fmodf" ||
3183 identifier == CPROVER_PREFIX "fmodl")
3184 {
3185 if(expr.arguments().size() != 2)
3186 {
3187 error().source_location = f_op.source_location();
3188 error() << "fmod-functions expect two operands" << eom;
3189 throw 0;
3190 }
3191
3193
3194 // Note that the semantics differ from the
3195 // "floating point remainder" operation as defined by IEEE.
3196 // Note that these do not take a rounding mode.
3198 expr.arguments()[0], ID_floatbv_mod, expr.arguments()[1]);
3199
3200 fmod_expr.add_source_location() = source_location;
3201
3202 return std::move(fmod_expr);
3203 }
3204 else if(
3205 identifier == CPROVER_PREFIX "remainder" ||
3206 identifier == CPROVER_PREFIX "remainderf" ||
3207 identifier == CPROVER_PREFIX "remainderl")
3208 {
3209 if(expr.arguments().size() != 2)
3210 {
3211 error().source_location = f_op.source_location();
3212 error() << "remainder-functions expect two operands" << eom;
3213 throw 0;
3214 }
3215
3217
3218 // The semantics of these functions is meant to match the
3219 // "floating point remainder" operation as defined by IEEE.
3220 // Note that these do not take a rounding mode.
3222 expr.arguments()[0], ID_floatbv_rem, expr.arguments()[1]);
3223
3224 floatbv_rem_expr.add_source_location() = source_location;
3225
3226 return std::move(floatbv_rem_expr);
3227 }
3228 else if(identifier==CPROVER_PREFIX "allocate")
3229 {
3230 if(expr.arguments().size()!=2)
3231 {
3232 error().source_location = f_op.source_location();
3233 error() << "allocate expects two operands" << eom;
3234 throw 0;
3235 }
3236
3238
3239 side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
3240 malloc_expr.operands()=expr.arguments();
3241
3242 return std::move(malloc_expr);
3243 }
3244 else if(
3245 (identifier == CPROVER_PREFIX "old") ||
3246 (identifier == CPROVER_PREFIX "loop_entry"))
3247 {
3248 if(expr.arguments().size() != 1)
3249 {
3250 error().source_location = f_op.source_location();
3251 error() << identifier << " expects one operand" << eom;
3252 throw 0;
3253 }
3254
3255 const auto &param_id = expr.arguments().front().id();
3256 if(!(param_id == ID_dereference || param_id == ID_member ||
3259 param_id == ID_index))
3260 {
3261 error().source_location = f_op.source_location();
3262 error() << "Tracking history of " << param_id
3263 << " expressions is not supported yet." << eom;
3264 throw 0;
3265 }
3266
3267 irep_idt id = identifier == CPROVER_PREFIX "old" ? ID_old : ID_loop_entry;
3268
3269 history_exprt old_expr(expr.arguments()[0], id);
3270 old_expr.add_source_location() = source_location;
3271
3272 return std::move(old_expr);
3273 }
3274 else if(identifier==CPROVER_PREFIX "isinff" ||
3275 identifier==CPROVER_PREFIX "isinfd" ||
3276 identifier==CPROVER_PREFIX "isinfld" ||
3277 identifier=="__builtin_isinf")
3278 {
3279 if(expr.arguments().size()!=1)
3280 {
3281 error().source_location = f_op.source_location();
3282 error() << identifier << " expects one operand" << eom;
3283 throw 0;
3284 }
3285
3287
3288 const exprt &fp_value = expr.arguments().front();
3289
3290 if(fp_value.type().id() != ID_floatbv)
3291 {
3292 error().source_location = fp_value.source_location();
3293 error() << "non-floating-point argument for " << identifier << eom;
3294 throw 0;
3295 }
3296
3297 isinf_exprt isinf_expr(expr.arguments().front());
3298 isinf_expr.add_source_location()=source_location;
3299
3301 }
3302 else if(identifier == "__builtin_isinf_sign")
3303 {
3304 if(expr.arguments().size() != 1)
3305 {
3306 error().source_location = f_op.source_location();
3307 error() << identifier << " expects one operand" << eom;
3308 throw 0;
3309 }
3310
3312
3313 // returns 1 for +inf and -1 for -inf, and 0 otherwise
3314
3315 const exprt &fp_value = expr.arguments().front();
3316
3317 if(fp_value.type().id() != ID_floatbv)
3318 {
3319 error().source_location = fp_value.source_location();
3320 error() << "non-floating-point argument for " << identifier << eom;
3321 throw 0;
3322 }
3323
3325 isinf_expr.add_source_location() = source_location;
3326
3327 return if_exprt(
3329 if_exprt(
3331 from_integer(-1, expr.type()),
3332 from_integer(1, expr.type())),
3333 from_integer(0, expr.type()));
3334 }
3335 else if(identifier == CPROVER_PREFIX "isnormalf" ||
3336 identifier == CPROVER_PREFIX "isnormald" ||
3337 identifier == CPROVER_PREFIX "isnormalld" ||
3338 identifier == "__builtin_isnormal")
3339 {
3340 if(expr.arguments().size()!=1)
3341 {
3342 error().source_location = f_op.source_location();
3343 error() << identifier << " expects one operand" << eom;
3344 throw 0;
3345 }
3346
3348
3349 const exprt &fp_value = expr.arguments()[0];
3350
3351 if(fp_value.type().id() != ID_floatbv)
3352 {
3353 error().source_location = fp_value.source_location();
3354 error() << "non-floating-point argument for " << identifier << eom;
3355 throw 0;
3356 }
3357
3358 isnormal_exprt isnormal_expr(expr.arguments().front());
3359 isnormal_expr.add_source_location()=source_location;
3360
3362 }
3363 else if(identifier==CPROVER_PREFIX "signf" ||
3364 identifier==CPROVER_PREFIX "signd" ||
3365 identifier==CPROVER_PREFIX "signld" ||
3366 identifier=="__builtin_signbit" ||
3367 identifier=="__builtin_signbitf" ||
3368 identifier=="__builtin_signbitl")
3369 {
3370 if(expr.arguments().size()!=1)
3371 {
3372 error().source_location = f_op.source_location();
3373 error() << identifier << " expects one operand" << eom;
3374 throw 0;
3375 }
3376
3378
3379 sign_exprt sign_expr(expr.arguments().front());
3380 sign_expr.add_source_location()=source_location;
3381
3383 }
3384 else if(identifier=="__builtin_popcount" ||
3385 identifier=="__builtin_popcountl" ||
3386 identifier=="__builtin_popcountll" ||
3387 identifier=="__popcnt16" ||
3388 identifier=="__popcnt" ||
3389 identifier=="__popcnt64")
3390 {
3391 if(expr.arguments().size()!=1)
3392 {
3393 error().source_location = f_op.source_location();
3394 error() << identifier << " expects one operand" << eom;
3395 throw 0;
3396 }
3397
3399
3400 popcount_exprt popcount_expr(expr.arguments().front(), expr.type());
3401 popcount_expr.add_source_location()=source_location;
3402
3403 return std::move(popcount_expr);
3404 }
3405 else if(
3406 identifier == "__builtin_clz" || identifier == "__builtin_clzl" ||
3407 identifier == "__builtin_clzll" || identifier == "__lzcnt16" ||
3408 identifier == "__lzcnt" || identifier == "__lzcnt64")
3409 {
3410 if(expr.arguments().size() != 1)
3411 {
3412 error().source_location = f_op.source_location();
3413 error() << identifier << " expects one operand" << eom;
3414 throw 0;
3415 }
3416
3418
3420 has_prefix(id2string(identifier), "__lzcnt"),
3421 expr.type()};
3422 clz.add_source_location() = source_location;
3423
3424 return std::move(clz);
3425 }
3426 else if(
3427 identifier == "__builtin_ctz" || identifier == "__builtin_ctzl" ||
3428 identifier == "__builtin_ctzll")
3429 {
3430 if(expr.arguments().size() != 1)
3431 {
3432 error().source_location = f_op.source_location();
3433 error() << identifier << " expects one operand" << eom;
3434 throw 0;
3435 }
3436
3438
3440 expr.arguments().front(), false, expr.type()};
3441 ctz.add_source_location() = source_location;
3442
3443 return std::move(ctz);
3444 }
3445 else if(
3446 identifier == "__builtin_ffs" || identifier == "__builtin_ffsl" ||
3447 identifier == "__builtin_ffsll")
3448 {
3449 if(expr.arguments().size() != 1)
3450 {
3451 error().source_location = f_op.source_location();
3452 error() << identifier << " expects one operand" << eom;
3453 throw 0;
3454 }
3455
3457
3458 find_first_set_exprt ffs{expr.arguments().front(), expr.type()};
3459 ffs.add_source_location() = source_location;
3460
3461 return std::move(ffs);
3462 }
3463 else if(identifier=="__builtin_expect")
3464 {
3465 // This is a gcc extension to provide branch prediction.
3466 // We compile it away, but adding some IR instruction for
3467 // this would clearly be an option. Note that the type
3468 // of the return value is wired to "long", i.e.,
3469 // this may trigger a type conversion due to the signature
3470 // of this function.
3471 if(expr.arguments().size()!=2)
3472 {
3473 error().source_location = f_op.source_location();
3474 error() << "__builtin_expect expects two arguments" << eom;
3475 throw 0;
3476 }
3477
3479
3480 return typecast_exprt(expr.arguments()[0], expr.type());
3481 }
3482 else if(identifier=="__builtin_object_size")
3483 {
3484 // this is a gcc extension to provide information about
3485 // object sizes at compile time
3486 // http://gcc.gnu.org/onlinedocs/gcc/Object-Size-Checking.html
3487
3488 if(expr.arguments().size()!=2)
3489 {
3490 error().source_location = f_op.source_location();
3491 error() << "__builtin_object_size expects two arguments" << eom;
3492 throw 0;
3493 }
3494
3496
3497 make_constant(expr.arguments()[1]);
3498
3500
3501 if(expr.arguments()[1].is_true())
3502 arg1=1;
3503 else if(expr.arguments()[1].is_false())
3504 arg1=0;
3505 else if(to_integer(to_constant_expr(expr.arguments()[1]), arg1))
3506 {
3507 error().source_location = f_op.source_location();
3508 error() << "__builtin_object_size expects constant as second argument, "
3509 << "but got " << to_string(expr.arguments()[1]) << eom;
3510 throw 0;
3511 }
3512
3513 exprt tmp;
3514
3515 // the following means "don't know"
3516 if(arg1==0 || arg1==1)
3517 {
3518 tmp=from_integer(-1, size_type());
3519 tmp.add_source_location()=f_op.source_location();
3520 }
3521 else
3522 {
3524 tmp.add_source_location()=f_op.source_location();
3525 }
3526
3527 return tmp;
3528 }
3529 else if(identifier=="__builtin_choose_expr")
3530 {
3531 // this is a gcc extension similar to ?:
3532 if(expr.arguments().size()!=3)
3533 {
3534 error().source_location = f_op.source_location();
3535 error() << "__builtin_choose_expr expects three arguments" << eom;
3536 throw 0;
3537 }
3538
3540
3541 exprt arg0 =
3544
3545 if(arg0.is_true())
3546 return expr.arguments()[1];
3547 else
3548 return expr.arguments()[2];
3549 }
3550 else if(identifier=="__builtin_constant_p")
3551 {
3552 // this is a gcc extension to tell whether the argument
3553 // is known to be a compile-time constant
3554 if(expr.arguments().size()!=1)
3555 {
3556 error().source_location = f_op.source_location();
3557 error() << "__builtin_constant_p expects one argument" << eom;
3558 throw 0;
3559 }
3560
3561 // do not typecheck the argument - it is never evaluated, and thus side
3562 // effects must not show up either
3563
3564 // try to produce constant
3565 exprt tmp1=expr.arguments().front();
3566 simplify(tmp1, *this);
3567
3568 bool is_constant=false;
3569
3570 // Need to do some special treatment for string literals,
3571 // which are (void *)&("lit"[0])
3572 if(
3573 tmp1.id() == ID_typecast &&
3574 to_typecast_expr(tmp1).op().id() == ID_address_of &&
3575 to_address_of_expr(to_typecast_expr(tmp1).op()).object().id() ==
3576 ID_index &&
3578 .array()
3579 .id() == ID_string_constant)
3580 {
3581 is_constant=true;
3582 }
3583 else
3584 is_constant=tmp1.is_constant();
3585
3587 tmp2.add_source_location()=source_location;
3588
3589 return tmp2;
3590 }
3591 else if(identifier=="__builtin_classify_type")
3592 {
3593 // This is a gcc/clang extension that produces an integer
3594 // constant for the type of the argument expression.
3595 if(expr.arguments().size()!=1)
3596 {
3597 error().source_location = f_op.source_location();
3598 error() << "__builtin_classify_type expects one argument" << eom;
3599 throw 0;
3600 }
3601
3603
3604 exprt object=expr.arguments()[0];
3605
3606 // The value doesn't matter at all, we only care about the type.
3607 // Need to sync with typeclass.h.
3608 typet type = follow(object.type());
3609
3610 // use underlying type for bit fields
3611 if(type.id() == ID_c_bit_field)
3612 type = to_c_bit_field_type(type).underlying_type();
3613
3614 unsigned type_number;
3615
3616 if(type.id() == ID_bool || type.id() == ID_c_bool)
3617 {
3618 // clang returns 4 for _Bool, gcc treats these as 'int'.
3619 type_number =
3621 }
3622 else
3623 {
3624 type_number =
3625 type.id() == ID_empty
3626 ? 0u
3627 : (type.id() == ID_bool || type.id() == ID_c_bool)
3628 ? 4u
3629 : (type.id() == ID_pointer || type.id() == ID_array)
3630 ? 5u
3631 : type.id() == ID_floatbv
3632 ? 8u
3633 : (type.id() == ID_complex &&
3634 to_complex_type(type).subtype().id() == ID_floatbv)
3635 ? 9u
3636 : type.id() == ID_struct
3637 ? 12u
3638 : type.id() == ID_union
3639 ? 13u
3640 : 1u; // int, short, char, enum_tag
3641 }
3642
3644 tmp.add_source_location()=source_location;
3645
3646 return tmp;
3647 }
3648 else if(
3649 identifier == "__builtin_add_overflow" ||
3650 identifier == "__builtin_sadd_overflow" ||
3651 identifier == "__builtin_saddl_overflow" ||
3652 identifier == "__builtin_saddll_overflow" ||
3653 identifier == "__builtin_uadd_overflow" ||
3654 identifier == "__builtin_uaddl_overflow" ||
3655 identifier == "__builtin_uaddll_overflow" ||
3656 identifier == "__builtin_add_overflow_p")
3657 {
3658 return typecheck_builtin_overflow(expr, ID_plus);
3659 }
3660 else if(
3661 identifier == "__builtin_sub_overflow" ||
3662 identifier == "__builtin_ssub_overflow" ||
3663 identifier == "__builtin_ssubl_overflow" ||
3664 identifier == "__builtin_ssubll_overflow" ||
3665 identifier == "__builtin_usub_overflow" ||
3666 identifier == "__builtin_usubl_overflow" ||
3667 identifier == "__builtin_usubll_overflow" ||
3668 identifier == "__builtin_sub_overflow_p")
3669 {
3671 }
3672 else if(
3673 identifier == "__builtin_mul_overflow" ||
3674 identifier == "__builtin_smul_overflow" ||
3675 identifier == "__builtin_smull_overflow" ||
3676 identifier == "__builtin_smulll_overflow" ||
3677 identifier == "__builtin_umul_overflow" ||
3678 identifier == "__builtin_umull_overflow" ||
3679 identifier == "__builtin_umulll_overflow" ||
3680 identifier == "__builtin_mul_overflow_p")
3681 {
3682 return typecheck_builtin_overflow(expr, ID_mult);
3683 }
3684 else if(
3685 identifier == "__builtin_bitreverse8" ||
3686 identifier == "__builtin_bitreverse16" ||
3687 identifier == "__builtin_bitreverse32" ||
3688 identifier == "__builtin_bitreverse64")
3689 {
3690 // clang only
3691 if(expr.arguments().size() != 1)
3692 {
3693 std::ostringstream error_message;
3694 error_message << "error: " << identifier << " expects one operand";
3696 error_message.str(), expr.source_location()};
3697 }
3698
3700
3702 bitreverse.add_source_location() = source_location;
3703
3704 return std::move(bitreverse);
3705 }
3706 else
3707 return nil_exprt();
3708 // NOLINTNEXTLINE(readability/fn_size)
3709}
3710
3713 const irep_idt &arith_op)
3714{
3715 const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
3716
3717 // check function signature
3718 if(expr.arguments().size() != 3)
3719 {
3720 std::ostringstream error_message;
3721 error_message << identifier << " takes exactly 3 arguments, but "
3722 << expr.arguments().size() << " were provided";
3724 error_message.str(), expr.source_location()};
3725 }
3726
3728
3729 auto lhs = expr.arguments()[0];
3730 auto rhs = expr.arguments()[1];
3731 auto result = expr.arguments()[2];
3732
3733 const bool is__p_variant = has_suffix(id2string(identifier), "_p");
3734
3735 {
3736 auto const raise_wrong_argument_error =
3737 [this, identifier](
3738 const exprt &wrong_argument, std::size_t argument_number, bool _p) {
3739 std::ostringstream error_message;
3740 error_message << "error: " << identifier << " has signature "
3741 << identifier << "(integral, integral, integral"
3742 << (_p ? "" : "*") << "), "
3743 << "but argument " << argument_number << " ("
3744 << expr2c(wrong_argument, *this) << ") has type `"
3745 << type2c(wrong_argument.type(), *this) << '`';
3747 error_message.str(), wrong_argument.source_location()};
3748 };
3749 for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3750 {
3751 auto const &argument = expr.arguments()[arg_index];
3752
3754 {
3756 }
3757 }
3758 if(
3759 !is__p_variant && (result.type().id() != ID_pointer ||
3761 to_pointer_type(result.type()).base_type())))
3762 {
3764 }
3765 }
3766
3768 std::move(lhs),
3769 std::move(rhs),
3770 std::move(result),
3771 expr.source_location()};
3772}
3773
3776{
3777 const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
3778
3779 // check function signature
3780 if(expr.arguments().size() != 2)
3781 {
3782 std::ostringstream error_message;
3783 error_message << "error: " << identifier
3784 << " takes exactly two arguments, but "
3785 << expr.arguments().size() << " were provided";
3787 error_message.str(), expr.source_location()};
3788 }
3789
3790 exprt result;
3791 if(identifier == CPROVER_PREFIX "saturating_minus")
3792 result = saturating_minus_exprt{expr.arguments()[0], expr.arguments()[1]};
3793 else if(identifier == CPROVER_PREFIX "saturating_plus")
3794 result = saturating_plus_exprt{expr.arguments()[0], expr.arguments()[1]};
3795 else
3797
3799 result.add_source_location() = expr.source_location();
3800
3801 return result;
3802}
3803
3808{
3809 const exprt &f_op=expr.function();
3810 const code_typet &code_type=to_code_type(f_op.type());
3811 exprt::operandst &arguments=expr.arguments();
3812 const code_typet::parameterst &parameters = code_type.parameters();
3813
3814 // no. of arguments test
3815
3816 if(code_type.get_bool(ID_C_incomplete))
3817 {
3818 // can't check
3819 }
3820 else if(code_type.is_KnR())
3821 {
3822 // We are generous on KnR; any number is ok.
3823 // We will fill in missing ones with "nondet".
3824 for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3825 {
3826 arguments.push_back(
3827 side_effect_expr_nondett{parameters[i].type(), expr.source_location()});
3828 }
3829 }
3830 else if(code_type.has_ellipsis())
3831 {
3832 if(parameters.size() > arguments.size())
3833 {
3835 error() << "not enough function arguments" << eom;
3836 throw 0;
3837 }
3838 }
3839 else if(parameters.size() != arguments.size())
3840 {
3842 error() << "wrong number of function arguments: "
3843 << "expected " << parameters.size() << ", but got "
3844 << arguments.size() << eom;
3845 throw 0;
3846 }
3847
3848 for(std::size_t i=0; i<arguments.size(); i++)
3849 {
3850 exprt &op=arguments[i];
3851
3852 if(op.is_nil())
3853 {
3854 // ignore
3855 }
3856 else if(i < parameters.size())
3857 {
3858 const code_typet::parametert &parameter = parameters[i];
3859
3860 if(
3861 parameter.is_boolean() && op.id() == ID_side_effect &&
3862 op.get(ID_statement) == ID_assign && op.type().id() != ID_bool)
3863 {
3865 warning() << "assignment where Boolean argument is expected" << eom;
3866 }
3867
3868 implicit_typecast(op, parameter.type());
3869 }
3870 else
3871 {
3872 // don't know type, just do standard conversion
3873
3874 if(op.type().id() == ID_array)
3875 {
3877 dest_type.base_type().set(ID_C_constant, true);
3879 }
3880 }
3881 }
3882}
3883
3885{
3886 // nothing to do
3887}
3888
3890{
3891 exprt &operand = to_unary_expr(expr).op();
3892
3893 const typet &o_type = operand.type();
3894
3895 if(o_type.id()==ID_vector)
3896 {
3897 if(is_number(to_vector_type(o_type).element_type()))
3898 {
3899 // Vector arithmetic.
3900 expr.type()=operand.type();
3901 return;
3902 }
3903 }
3904
3906
3907 if(is_number(operand.type()))
3908 {
3909 expr.type()=operand.type();
3910 return;
3911 }
3912
3914 error() << "operator '" << expr.id() << "' not defined for type '"
3915 << to_string(operand.type()) << "'" << eom;
3916 throw 0;
3917}
3918
3920{
3922
3923 // This is not quite accurate: the standard says the result
3924 // should be of type 'int'.
3925 // We do 'bool' anyway to get more compact formulae. Eventually,
3926 // this should be achieved by means of simplification, and not
3927 // in the frontend.
3928 expr.type()=bool_typet();
3929}
3930
3932 const vector_typet &type0,
3933 const vector_typet &type1)
3934{
3935 // This is relatively restrictive!
3936
3937 // compare dimension
3938 const auto s0 = numeric_cast<mp_integer>(type0.size());
3939 const auto s1 = numeric_cast<mp_integer>(type1.size());
3940 if(!s0.has_value())
3941 return false;
3942 if(!s1.has_value())
3943 return false;
3944 if(*s0 != *s1)
3945 return false;
3946
3947 // compare subtype
3948 if(
3949 (type0.element_type().id() == ID_signedbv ||
3950 type0.element_type().id() == ID_unsignedbv) &&
3951 (type1.element_type().id() == ID_signedbv ||
3952 type1.element_type().id() == ID_unsignedbv) &&
3953 to_bitvector_type(type0.element_type()).get_width() ==
3954 to_bitvector_type(type1.element_type()).get_width())
3955 return true;
3956
3957 return type0.element_type() == type1.element_type();
3958}
3959
3961{
3962 auto &binary_expr = to_binary_expr(expr);
3963 exprt &op0 = binary_expr.op0();
3964 exprt &op1 = binary_expr.op1();
3965
3966 const typet o_type0 = op0.type();
3967 const typet o_type1 = op1.type();
3968
3969 if(o_type0.id()==ID_vector &&
3970 o_type1.id()==ID_vector)
3971 {
3972 if(
3975 is_number(to_vector_type(o_type0).element_type()))
3976 {
3977 // Vector arithmetic has fairly strict typing rules, no promotion
3978 op1 = typecast_exprt::conditional_cast(op1, op0.type());
3979 expr.type()=op0.type();
3980 return;
3981 }
3982 }
3983 else if(
3984 o_type0.id() == ID_vector && o_type1.id() != ID_vector &&
3986 {
3987 // convert op1 to the vector type
3988 op1 = typecast_exprt(op1, o_type0);
3989 expr.type() = o_type0;
3990 return;
3991 }
3992 else if(
3993 o_type0.id() != ID_vector && o_type1.id() == ID_vector &&
3995 {
3996 // convert op0 to the vector type
3997 op0 = typecast_exprt(op0, o_type1);
3998 expr.type() = o_type1;
3999 return;
4000 }
4001
4002 if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
4003 {
4005 }
4006 else
4007 {
4008 // promote!
4010 }
4011
4012 const typet &type0 = op0.type();
4013 const typet &type1 = op1.type();
4014
4015 if(expr.id()==ID_plus || expr.id()==ID_minus ||
4016 expr.id()==ID_mult || expr.id()==ID_div)
4017 {
4018 if(type0.id()==ID_pointer || type1.id()==ID_pointer)
4019 {
4021 return;
4022 }
4023 else if(type0==type1)
4024 {
4025 if(is_number(type0))
4026 {
4027 expr.type()=type0;
4028 return;
4029 }
4030 }
4031 }
4032 else if(expr.id()==ID_mod)
4033 {
4034 if(type0==type1)
4035 {
4036 if(type0.id()==ID_signedbv || type0.id()==ID_unsignedbv)
4037 {
4038 expr.type()=type0;
4039 return;
4040 }
4041 }
4042 }
4043 else if(
4044 expr.id() == ID_bitand || expr.id() == ID_bitnand ||
4045 expr.id() == ID_bitxor || expr.id() == ID_bitor)
4046 {
4047 if(type0==type1)
4048 {
4049 if(is_number(type0))
4050 {
4051 expr.type()=type0;
4052 return;
4053 }
4054 else if(type0.id()==ID_bool)
4055 {
4056 if(expr.id()==ID_bitand)
4057 expr.id(ID_and);
4058 else if(expr.id() == ID_bitnand)
4059 expr.id(ID_nand);
4060 else if(expr.id()==ID_bitor)
4061 expr.id(ID_or);
4062 else if(expr.id()==ID_bitxor)
4063 expr.id(ID_xor);
4064 else
4066 expr.type()=type0;
4067 return;
4068 }
4069 }
4070 }
4071 else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
4072 {
4073 if(
4074 type0 == type1 &&
4075 (type0.id() == ID_signedbv || type0.id() == ID_unsignedbv))
4076 {
4077 expr.type() = type0;
4078 return;
4079 }
4080 }
4081
4083 error() << "operator '" << expr.id() << "' not defined for types '"
4084 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4085 << eom;
4086 throw 0;
4087}
4088
4090{
4091 PRECONDITION(expr.id() == ID_shl || expr.id() == ID_shr);
4092
4093 exprt &op0=expr.op0();
4094 exprt &op1=expr.op1();
4095
4096 const typet o_type0 = op0.type();
4097 const typet o_type1 = op1.type();
4098
4099 if(o_type0.id()==ID_vector &&
4100 o_type1.id()==ID_vector)
4101 {
4102 if(
4103 to_vector_type(o_type0).element_type() ==
4104 to_vector_type(o_type1).element_type() &&
4105 is_number(to_vector_type(o_type0).element_type()))
4106 {
4107 // {a0, a1, ..., an} >> {b0, b1, ..., bn} ==
4108 // {a0 >> b0, a1 >> b1, ..., an >> bn}
4109 // Fairly strict typing rules, no promotion
4110 expr.type()=op0.type();
4111 return;
4112 }
4113 }
4114
4115 if(
4116 o_type0.id() == ID_vector &&
4117 is_number(to_vector_type(o_type0).element_type()) && is_number(o_type1))
4118 {
4119 // {a0, a1, ..., an} >> b == {a0 >> b, a1 >> b, ..., an >> b}
4120 op1 = typecast_exprt(op1, o_type0);
4121 expr.type()=op0.type();
4122 return;
4123 }
4124
4125 // must do the promotions _separately_!
4128
4129 if(is_number(op0.type()) &&
4130 is_number(op1.type()))
4131 {
4132 expr.type()=op0.type();
4133
4134 if(expr.id()==ID_shr) // shifting operation depends on types
4135 {
4136 const typet &op0_type = op0.type();
4137
4138 if(op0_type.id()==ID_unsignedbv)
4139 {
4140 expr.id(ID_lshr);
4141 return;
4142 }
4143 else if(op0_type.id()==ID_signedbv)
4144 {
4145 expr.id(ID_ashr);
4146 return;
4147 }
4148 }
4149
4150 return;
4151 }
4152
4154 error() << "operator '" << expr.id() << "' not defined for types '"
4155 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4156 << eom;
4157 throw 0;
4158}
4159
4161{
4162 const typet &type=expr.type();
4163 PRECONDITION(type.id() == ID_pointer);
4164
4165 const typet &base_type = to_pointer_type(type).base_type();
4166
4167 if(
4168 base_type.id() == ID_struct_tag &&
4169 follow_tag(to_struct_tag_type(base_type)).is_incomplete())
4170 {
4172 error() << "pointer arithmetic with unknown object size" << eom;
4173 throw 0;
4174 }
4175 else if(
4176 base_type.id() == ID_union_tag &&
4177 follow_tag(to_union_tag_type(base_type)).is_incomplete())
4178 {
4180 error() << "pointer arithmetic with unknown object size" << eom;
4181 throw 0;
4182 }
4183 else if(
4184 base_type.id() == ID_empty &&
4186 {
4188 error() << "pointer arithmetic with unknown object size" << eom;
4189 throw 0;
4190 }
4191 else if(base_type.id() == ID_empty)
4192 {
4193 // This is a gcc extension.
4194 // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
4196 expr.swap(tc);
4197 }
4198}
4199
4201{
4202 auto &binary_expr = to_binary_expr(expr);
4203 exprt &op0 = binary_expr.op0();
4204 exprt &op1 = binary_expr.op1();
4205
4206 const typet &type0 = op0.type();
4207 const typet &type1 = op1.type();
4208
4209 if(expr.id()==ID_minus ||
4210 (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_minus))
4211 {
4212 if(type0.id()==ID_pointer &&
4213 type1.id()==ID_pointer)
4214 {
4215 if(type0 != type1)
4216 {
4218 "pointer subtraction over different types", expr.source_location()};
4219 }
4220 expr.type()=pointer_diff_type();
4223 return;
4224 }
4225
4226 if(type0.id()==ID_pointer &&
4227 (type1.id()==ID_bool ||
4228 type1.id()==ID_c_bool ||
4229 type1.id()==ID_unsignedbv ||
4230 type1.id()==ID_signedbv ||
4231 type1.id()==ID_c_bit_field ||
4232 type1.id()==ID_c_enum_tag))
4233 {
4235 make_index_type(op1);
4236 expr.type() = op0.type();
4237 return;
4238 }
4239 }
4240 else if(expr.id()==ID_plus ||
4241 (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_plus))
4242 {
4243 exprt *p_op, *int_op;
4244
4245 if(type0.id()==ID_pointer)
4246 {
4247 p_op=&op0;
4248 int_op=&op1;
4249 }
4250 else if(type1.id()==ID_pointer)
4251 {
4252 p_op=&op1;
4253 int_op=&op0;
4254 }
4255 else
4256 {
4257 p_op=int_op=nullptr;
4259 }
4260
4261 const typet &int_op_type = int_op->type();
4262
4263 if(int_op_type.id()==ID_bool ||
4264 int_op_type.id()==ID_c_bool ||
4265 int_op_type.id()==ID_unsignedbv ||
4266 int_op_type.id()==ID_signedbv ||
4269 {
4272 expr.type()=p_op->type();
4273 return;
4274 }
4275 }
4276
4277 irep_idt op_name;
4278
4279 if(expr.id()==ID_side_effect)
4280 op_name=to_side_effect_expr(expr).get_statement();
4281 else
4282 op_name=expr.id();
4283
4285 error() << "operator '" << op_name << "' not defined for types '"
4286 << to_string(type0) << "' and '" << to_string(type1) << "'" << eom;
4287 throw 0;
4288}
4289
4291{
4292 auto &binary_expr = to_binary_expr(expr);
4295
4296 // This is not quite accurate: the standard says the result
4297 // should be of type 'int'.
4298 // We do 'bool' anyway to get more compact formulae. Eventually,
4299 // this should be achieved by means of simplification, and not
4300 // in the frontend.
4301 expr.type()=bool_typet();
4302}
4303
4305 side_effect_exprt &expr)
4306{
4307 const irep_idt &statement=expr.get_statement();
4308
4309 auto &binary_expr = to_binary_expr(expr);
4310 exprt &op0 = binary_expr.op0();
4311 exprt &op1 = binary_expr.op1();
4312
4313 {
4314 const typet &type0=op0.type();
4315
4316 if(type0.id()==ID_empty)
4317 {
4319 error() << "cannot assign void" << eom;
4320 throw 0;
4321 }
4322
4323 if(!op0.get_bool(ID_C_lvalue))
4324 {
4326 error() << "assignment error: '" << to_string(op0) << "' not an lvalue"
4327 << eom;
4328 throw 0;
4329 }
4330
4331 if(type0.get_bool(ID_C_constant))
4332 {
4334 error() << "'" << to_string(op0) << "' is constant" << eom;
4335 throw 0;
4336 }
4337
4338 // refuse to assign arrays
4339 if(type0.id() == ID_array)
4340 {
4342 error() << "direct assignments to arrays not permitted" << eom;
4343 throw 0;
4344 }
4345 }
4346
4347 // Add a cast to the underlying type for bit fields.
4348 // In particular, sizeof(s.f=1) works for bit fields.
4349 if(op0.type().id()==ID_c_bit_field)
4350 op0 =
4351 typecast_exprt(op0, to_c_bit_field_type(op0.type()).underlying_type());
4352
4353 const typet o_type0=op0.type();
4354 const typet o_type1=op1.type();
4355
4356 expr.type()=o_type0;
4357
4358 if(statement==ID_assign)
4359 {
4361 return;
4362 }
4363 else if(statement==ID_assign_shl ||
4364 statement==ID_assign_shr)
4365 {
4366 if(o_type0.id() == ID_vector)
4367 {
4369
4370 if(
4371 o_type1.id() == ID_vector &&
4372 vector_o_type0.element_type() ==
4373 to_vector_type(o_type1).element_type() &&
4374 is_number(vector_o_type0.element_type()))
4375 {
4376 return;
4377 }
4378 else if(is_number(vector_o_type0.element_type()) && is_number(o_type1))
4379 {
4380 op1 = typecast_exprt(op1, o_type0);
4381 return;
4382 }
4383 }
4384
4387
4388 if(is_number(op0.type()) && is_number(op1.type()))
4389 {
4390 if(statement==ID_assign_shl)
4391 {
4392 return;
4393 }
4394 else // assign_shr
4395 {
4396 // distinguish arithmetic from logical shifts by looking at type
4397
4398 typet underlying_type=op0.type();
4399
4400 if(underlying_type.id()==ID_unsignedbv ||
4401 underlying_type.id()==ID_c_bool)
4402 {
4404 return;
4405 }
4406 else if(underlying_type.id()==ID_signedbv)
4407 {
4409 return;
4410 }
4411 }
4412 }
4413 }
4414 else if(statement==ID_assign_bitxor ||
4415 statement==ID_assign_bitand ||
4416 statement==ID_assign_bitor)
4417 {
4418 // these are more restrictive
4419 if(o_type0.id()==ID_bool ||
4420 o_type0.id()==ID_c_bool)
4421 {
4423 if(
4424 op1.is_boolean() || op1.type().id() == ID_c_bool ||
4425 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4426 op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
4427 {
4428 return;
4429 }
4430 }
4431 else if(o_type0.id()==ID_c_enum_tag ||
4432 o_type0.id()==ID_unsignedbv ||
4433 o_type0.id()==ID_signedbv ||
4434 o_type0.id()==ID_c_bit_field)
4435 {
4437 if(
4438 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4439 op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
4440 {
4441 return;
4442 }
4443 }
4444 else if(o_type0.id()==ID_vector &&
4445 o_type1.id()==ID_vector)
4446 {
4447 // We are willing to do a modest amount of conversion
4450 {
4452 return;
4453 }
4454 }
4455 else if(
4456 o_type0.id() == ID_vector &&
4457 (o_type1.id() == ID_bool || o_type1.id() == ID_c_bool ||
4458 o_type1.id() == ID_c_enum_tag || o_type1.id() == ID_unsignedbv ||
4459 o_type1.id() == ID_signedbv))
4460 {
4462 op1 = typecast_exprt(op1, o_type0);
4463 return;
4464 }
4465 }
4466 else
4467 {
4468 if(o_type0.id()==ID_pointer &&
4469 (statement==ID_assign_minus || statement==ID_assign_plus))
4470 {
4472 return;
4473 }
4474 else if(o_type0.id()==ID_vector &&
4475 o_type1.id()==ID_vector)
4476 {
4477 // We are willing to do a modest amount of conversion
4480 {
4482 return;
4483 }
4484 }
4485 else if(o_type0.id() == ID_vector)
4486 {
4488
4489 if(
4490 is_number(op1.type()) || op1.is_boolean() ||
4491 op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
4492 {
4493 op1 = typecast_exprt(op1, o_type0);
4494 return;
4495 }
4496 }
4497 else if(o_type0.id()==ID_bool ||
4498 o_type0.id()==ID_c_bool)
4499 {
4501 if(
4502 op1.is_boolean() || op1.type().id() == ID_c_bool ||
4503 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4504 op1.type().id() == ID_signedbv)
4505 {
4506 return;
4507 }
4508 }
4509 else
4510 {
4512
4513 if(
4514 is_number(op1.type()) || op1.is_boolean() ||
4515 op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
4516 {
4517 return;
4518 }
4519 }
4520 }
4521
4523 error() << "assignment '" << statement << "' not defined for types '"
4524 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4525 << eom;
4526
4527 throw 0;
4528}
4529
4534{
4535public:
4537 {
4538 }
4539
4541 bool operator()(const exprt &e) const
4542 {
4543 return is_constant(e);
4544 }
4545
4546protected:
4548
4551 bool is_constant(const exprt &e) const
4552 {
4553 if(e.id() == ID_infinity)
4554 return true;
4555
4556 if(e.is_constant())
4557 return true;
4558
4559 if(e.id() == ID_address_of)
4560 {
4561 return is_constant_address_of(to_address_of_expr(e).object());
4562 }
4563 else if(
4564 e.id() == ID_typecast || e.id() == ID_array_of || e.id() == ID_plus ||
4565 e.id() == ID_mult || e.id() == ID_array || e.id() == ID_with ||
4566 e.id() == ID_struct || e.id() == ID_union || e.id() == ID_empty_union ||
4567 e.id() == ID_equal || e.id() == ID_notequal || e.id() == ID_lt ||
4568 e.id() == ID_le || e.id() == ID_gt || e.id() == ID_ge ||
4569 e.id() == ID_if || e.id() == ID_not || e.id() == ID_and ||
4570 e.id() == ID_or || e.id() == ID_bitnot || e.id() == ID_bitand ||
4571 e.id() == ID_bitor || e.id() == ID_bitxor || e.id() == ID_vector)
4572 {
4573 return std::all_of(
4574 e.operands().begin(), e.operands().end(), [this](const exprt &op) {
4575 return is_constant(op);
4576 });
4577 }
4578
4579 return false;
4580 }
4581
4583 bool is_constant_address_of(const exprt &e) const
4584 {
4585 if(e.id() == ID_symbol)
4586 {
4587 return e.type().id() == ID_code ||
4588 ns.lookup(to_symbol_expr(e).get_identifier()).is_static_lifetime;
4589 }
4590 else if(e.id() == ID_array && e.get_bool(ID_C_string_constant))
4591 return true;
4592 else if(e.id() == ID_label)
4593 return true;
4594 else if(e.id() == ID_index)
4595 {
4597
4598 return is_constant_address_of(index_expr.array()) &&
4599 is_constant(index_expr.index());
4600 }
4601 else if(e.id() == ID_member)
4602 {
4603 return is_constant_address_of(to_member_expr(e).compound());
4604 }
4605 else if(e.id() == ID_dereference)
4606 {
4608
4609 return is_constant(deref.pointer());
4610 }
4611 else if(e.id() == ID_string_constant)
4612 return true;
4613
4614 return false;
4615 }
4616};
4617
4619{
4620 // Floating-point expressions may require a rounding mode.
4621 // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
4622 // Some compilers have command-line options to override.
4623 const auto rounding_mode =
4625 adjust_float_expressions(expr, rounding_mode);
4626
4627 simplify(expr, *this);
4628
4629 if(!is_compile_time_constantt(*this)(expr))
4630 {
4632 error() << "expected constant expression, but got '" << to_string(expr)
4633 << "'" << eom;
4634 throw 0;
4635 }
4636}
4637
4639{
4640 make_constant(expr);
4641 make_index_type(expr);
4642 simplify(expr, *this);
4643
4644 if(!is_compile_time_constantt(*this)(expr))
4645 {
4647 error() << "conversion to integer constant failed" << eom;
4648 throw 0;
4649 }
4650}
4651
4653 const exprt &expr,
4654 const irep_idt &id,
4655 const std::string &message) const
4656{
4657 if(!has_subexpr(expr, id))
4658 return;
4659
4661 error() << message << eom;
4662 throw 0;
4663}
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.
bool builtin_factory(const irep_idt &identifier, symbol_table_baset &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
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.
virtual void clear()
Reset the abstract state.
Definition ai.h:266
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)
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