CBMC
Loading...
Searching...
No Matches
goto_check_c.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Checks for Errors in C/C++ Programs
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_check_c.h"
13
14#include <util/arith_tools.h>
15#include <util/array_name.h>
16#include <util/bitvector_expr.h>
17#include <util/c_types.h>
18#include <util/config.h>
19#include <util/cprover_prefix.h>
20#include <util/expr_util.h>
21#include <util/find_symbols.h>
22#include <util/floatbv_expr.h>
23#include <util/ieee_float.h>
24#include <util/invariant.h>
26#include <util/message.h>
27#include <util/options.h>
28#include <util/pointer_expr.h>
31#include <util/simplify_expr.h>
32#include <util/std_code.h>
33#include <util/std_expr.h>
34
37
39#include <ansi-c/c_expr.h>
40#include <langapi/language.h>
41#include <langapi/mode.h>
42
43#include <algorithm>
44
46{
47public:
49 const namespacet &_ns,
50 const optionst &_options,
53 {
54 enable_bounds_check = _options.get_bool_option("bounds-check");
55 enable_pointer_check = _options.get_bool_option("pointer-check");
56 enable_memory_leak_check = _options.get_bool_option("memory-leak-check");
58 _options.get_bool_option("memory-cleanup-check");
59 enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
61 _options.get_bool_option("float-div-by-zero-check");
62 enable_enum_range_check = _options.get_bool_option("enum-range-check");
64 _options.get_bool_option("signed-overflow-check");
66 _options.get_bool_option("unsigned-overflow-check");
68 _options.get_bool_option("pointer-overflow-check");
69 enable_conversion_check = _options.get_bool_option("conversion-check");
71 _options.get_bool_option("undefined-shift-check");
73 _options.get_bool_option("float-overflow-check");
74 enable_simplify = _options.get_bool_option("simplify");
75 enable_nan_check = _options.get_bool_option("nan-check");
76 retain_trivial = _options.get_bool_option("retain-trivial-checks");
77 enable_assert_to_assume = _options.get_bool_option("assert-to-assume");
78 error_labels = _options.get_list_option("error-label");
80 _options.get_bool_option("pointer-primitive-check");
81 }
82
84
85 void goto_check(
86 const irep_idt &function_identifier,
87 goto_functiont &goto_function);
88
94 void collect_allocations(const goto_functionst &goto_functions);
95
96protected:
97 const namespacet &ns;
98 std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
101
102 using guardt = std::function<exprt(exprt)>;
103 const guardt identity = [](exprt expr) { return expr; };
104
106
112 void check_rec_address(const exprt &expr, const guardt &guard);
113
121 void check_rec_logical_op(const exprt &expr, const guardt &guard);
122
129 void check_rec_if(const if_exprt &if_expr, const guardt &guard);
130
141 bool check_rec_member(const member_exprt &member, const guardt &guard);
142
147 void check_rec_div(const div_exprt &div_expr, const guardt &guard);
148
153 void check_rec_arithmetic_op(const exprt &expr, const guardt &guard);
154
161 void check_rec(const exprt &expr, const guardt &guard, bool is_assigned);
162
166 void check(const exprt &expr, bool is_assigned);
167
169 {
170 conditiont(const exprt &_assertion, const std::string &_description)
171 : assertion(_assertion), description(_description)
172 {
173 }
174
176 std::string description;
177 };
178
179 using conditionst = std::list<conditiont>;
180
181 void bounds_check(const exprt &, const guardt &);
182 void bounds_check_index(const index_exprt &, const guardt &);
183 void bounds_check_bit_count(const unary_exprt &, const guardt &);
184 void div_by_zero_check(const div_exprt &, const guardt &);
185 void float_div_by_zero_check(const div_exprt &, const guardt &);
186 void mod_by_zero_check(const mod_exprt &, const guardt &);
187 void mod_overflow_check(const mod_exprt &, const guardt &);
188 void enum_range_check(const exprt &, const guardt &, bool is_assigned);
189 void undefined_shift_check(const shift_exprt &, const guardt &);
190 void pointer_rel_check(const binary_exprt &, const guardt &);
191 void pointer_overflow_check(const exprt &, const guardt &);
192 void memory_leak_check(const irep_idt &function_id);
193
200 const dereference_exprt &expr,
201 const exprt &src_expr,
202 const guardt &guard);
203
209 void pointer_primitive_check(const exprt &expr, const guardt &guard);
210
217 bool requires_pointer_primitive_check(const exprt &expr);
218
219 std::optional<goto_check_ct::conditiont>
220 get_pointer_is_null_condition(const exprt &address, const exprt &size);
222 const exprt &address,
223 const exprt &size);
225 const exprt &pointer,
226 const exprt &size);
227
229 const exprt &address,
230 const exprt &size);
231 void integer_overflow_check(const exprt &, const guardt &);
232 void conversion_check(const exprt &, const guardt &);
233 void float_overflow_check(const exprt &, const guardt &);
234 void nan_check(const exprt &, const guardt &);
235
236 std::string array_name(const exprt &);
237
248 const exprt &asserted_expr,
249 const std::string &comment,
250 const std::string &property_class,
251 bool is_fatal,
252 const source_locationt &source_location,
253 const exprt &src_expr,
254 const guardt &guard);
255
257 typedef std::set<std::pair<exprt, exprt>> assertionst;
259
264 void invalidate(const exprt &lhs);
265
284
286 std::map<irep_idt, bool *> name_to_flag{
287 {"bounds-check", &enable_bounds_check},
288 {"pointer-check", &enable_pointer_check},
289 {"memory-leak-check", &enable_memory_leak_check},
290 {"memory-cleanup-check", &enable_memory_cleanup_check},
291 {"div-by-zero-check", &enable_div_by_zero_check},
292 {"float-div-by-zero-check", &enable_float_div_by_zero_check},
293 {"enum-range-check", &enable_enum_range_check},
294 {"signed-overflow-check", &enable_signed_overflow_check},
295 {"unsigned-overflow-check", &enable_unsigned_overflow_check},
296 {"pointer-overflow-check", &enable_pointer_overflow_check},
297 {"conversion-check", &enable_conversion_check},
298 {"undefined-shift-check", &enable_undefined_shift_check},
299 {"float-overflow-check", &enable_float_overflow_check},
300 {"nan-check", &enable_nan_check},
301 {"pointer-primitive-check", &enable_pointer_primitive_check}};
302
305
306 // the first element of the pair is the base address,
307 // and the second is the size of the region
308 typedef std::pair<exprt, exprt> allocationt;
309 typedef std::list<allocationt> allocationst;
311
313
316 void add_active_named_check_pragmas(source_locationt &source_location) const;
317
320 void
322
324 typedef enum
325 {
328 CHECKED
330
332 using named_check_statust = std::optional<std::pair<irep_idt, check_statust>>;
333
343};
344
353{
354public:
359
365 void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
366 {
367 // make this a no-op if the flag is disabled
368 if(disabled_flags.find(&flag) != disabled_flags.end())
369 return;
370
371 // detect double sets
372 INVARIANT(
373 flags_to_reset.find(&flag) == flags_to_reset.end(),
374 "Flag " + id2string(flag_name) + " set twice at \n" +
375 source_location.as_string());
376 if(flag != new_value)
377 {
378 flags_to_reset[&flag] = flag;
379 flag = new_value;
380 }
381 }
382
387 void disable_flag(bool &flag, const irep_idt &flag_name)
388 {
389 INVARIANT(
390 disabled_flags.find(&flag) == disabled_flags.end(),
391 "Flag " + id2string(flag_name) + " disabled twice at \n" +
392 source_location.as_string());
393
394 disabled_flags.insert(&flag);
395
396 // If the flag has not already been set,
397 // we store its current value in the reset map.
398 // Otherwise, the reset map already holds
399 // the initial value we want to reset it to, keep it as is.
400 if(flags_to_reset.find(&flag) == flags_to_reset.end())
401 flags_to_reset[&flag] = flag;
402
403 // set the flag to false in all cases.
404 flag = false;
405 }
406
410 {
411 for(const auto &flag_pair : flags_to_reset)
412 *flag_pair.first = flag_pair.second;
413 }
414
415private:
417 std::map<bool *, bool> flags_to_reset;
418 std::set<bool *> disabled_flags;
419};
420
421static exprt implication(exprt lhs, exprt rhs)
422{
423 // rewrite a => (b => c) to (a && b) => c
424 if(rhs.id() == ID_implies)
425 {
426 const auto &rhs_implication = to_implies_expr(rhs);
427 return implies_exprt(
428 and_exprt(std::move(lhs), rhs_implication.lhs()), rhs_implication.rhs());
429 }
430 else
431 {
432 return implies_exprt(std::move(lhs), std::move(rhs));
433 }
434}
435
437{
438 for(const auto &gf_entry : goto_functions.function_map)
439 {
440 for(const auto &instruction : gf_entry.second.body.instructions)
441 {
442 if(!instruction.is_function_call())
443 continue;
444
445 const auto &function = instruction.call_function();
446 if(
447 function.id() != ID_symbol ||
448 to_symbol_expr(function).get_identifier() != CPROVER_PREFIX
449 "allocated_memory")
450 continue;
451
453 instruction.call_arguments();
454 if(
455 args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
456 args[1].type().id() != ID_unsignedbv)
457 throw "expected two unsigned arguments to " CPROVER_PREFIX
458 "allocated_memory";
459
461 args[0].type() == args[1].type(),
462 "arguments of allocated_memory must have same type");
463 allocations.push_back({args[0], args[1]});
464 }
465 }
466}
467
469{
470 if(lhs.id() == ID_index)
471 invalidate(to_index_expr(lhs).array());
472 else if(lhs.id() == ID_member)
473 invalidate(to_member_expr(lhs).struct_op());
474 else if(lhs.id() == ID_symbol)
475 {
476 // clear all assertions about 'symbol'
477 const irep_idt &lhs_id = to_symbol_expr(lhs).get_identifier();
478
479 for(auto it = assertions.begin(); it != assertions.end();)
480 {
481 if(
482 has_symbol_expr(it->second, lhs_id, false) ||
483 has_subexpr(it->second, ID_dereference))
484 {
485 it = assertions.erase(it);
486 }
487 else
488 ++it;
489 }
490 }
491 else
492 {
493 // give up, clear all
495 }
496}
497
499 const div_exprt &expr,
500 const guardt &guard)
501{
503 return;
504
505 // add divison by zero subgoal
506
507 exprt zero = from_integer(0, expr.op1().type());
508 const notequal_exprt inequality(expr.op1(), std::move(zero));
509
512 "division by zero",
513 "division-by-zero",
514 true, // fatal
516 expr,
517 guard);
518}
519
521 const div_exprt &expr,
522 const guardt &guard)
523{
525 return;
526
527 // add divison by zero subgoal
528
529 exprt zero = from_integer(0, expr.op1().type());
530 const notequal_exprt inequality(expr.op1(), std::move(zero));
531
534 "floating-point division by zero",
535 "float-division-by-zero",
536 false, // fatal
538 expr,
539 guard);
540}
541
543 const exprt &expr,
544 const guardt &guard,
545 bool is_assigned)
546{
548 return;
549
550 if(is_assigned)
551 return; // not in range yet
552
553 // we might be looking at a lowered enum_is_in_range_exprt, skip over these
554 const auto &pragmas = expr.source_location().get_pragmas();
555 for(const auto &d : pragmas)
556 {
557 if(d.first == "disable:enum-range-check")
558 return;
559 }
560
561 const exprt check = enum_is_in_range_exprt{expr}.lower(ns);
562
564 check,
565 "enum range check",
566 "enum-range-check",
567 false, // fatal
569 expr,
570 guard);
571}
572
574 const shift_exprt &expr,
575 const guardt &guard)
576{
578 return;
579
580 // Undefined for all types and shifts if distance exceeds width,
581 // and also undefined for negative distances.
582
583 const typet &distance_type = expr.distance().type();
584
585 if(distance_type.id() == ID_signedbv)
586 {
589
592 "shift distance is negative",
593 "undefined-shift",
594 true, // fatal
596 expr,
597 guard);
598 }
599
600 const typet &op_type = expr.op().type();
601
602 if(op_type.id() == ID_unsignedbv || op_type.id() == ID_signedbv)
603 {
606
608 binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
609 "shift distance too large",
610 "undefined-shift",
611 true, // fatal
613 expr,
614 guard);
615
616 if(op_type.id() == ID_signedbv && expr.id() == ID_shl)
617 {
619 expr.op(), ID_ge, from_integer(0, op_type));
620
623 "shift operand is negative",
624 "undefined-shift",
625 true, // fatal
627 expr,
628 guard);
629 }
630 }
631 else
632 {
634 false_exprt(),
635 "shift of non-integer type",
636 "undefined-shift",
637 true, // fatal
639 expr,
640 guard);
641 }
642}
643
645 const mod_exprt &expr,
646 const guardt &guard)
647{
649 return;
650
651 // add divison by zero subgoal
652
653 exprt zero = from_integer(0, expr.divisor().type());
654 const notequal_exprt inequality(expr.divisor(), std::move(zero));
655
658 "division by zero",
659 "division-by-zero",
660 true, // fatal
662 expr,
663 guard);
664}
665
668 const mod_exprt &expr,
669 const guardt &guard)
670{
672 return;
673
674 const auto &type = expr.type();
675
676 if(type.id() == ID_signedbv)
677 {
678 // INT_MIN % -1 is, in principle, defined to be zero in
679 // ANSI C, C99, C++98, and C++11. Most compilers, however,
680 // fail to produce 0, and in some cases generate an exception.
681 // C11 explicitly makes this case undefined.
682
684 expr.op0(), to_signedbv_type(type).smallest_expr());
685
687 expr.op1(), from_integer(-1, expr.op1().type()));
688
691 "result of signed mod is not representable",
692 "overflow",
693 false, // fatal
695 expr,
696 guard);
697 }
698}
699
701{
703 return;
704
705 // First, check type.
706 const typet &type = expr.type();
707
708 if(type.id() != ID_signedbv && type.id() != ID_unsignedbv)
709 return;
710
711 if(expr.id() == ID_typecast)
712 {
713 const auto &op = to_typecast_expr(expr).op();
714
715 // conversion to signed int may overflow
716 const typet &old_type = op.type();
717
718 if(type.id() == ID_signedbv)
719 {
720 std::size_t new_width = to_signedbv_type(type).get_width();
721
722 if(old_type.id() == ID_signedbv) // signed -> signed
723 {
724 std::size_t old_width = to_signedbv_type(old_type).get_width();
725 if(new_width >= old_width)
726 return; // always ok
727
729 op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
730
732 op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
733
736 "arithmetic overflow on signed type conversion",
737 "overflow",
738 false, // fatal
740 expr,
741 guard);
742 }
743 else if(old_type.id() == ID_unsignedbv) // unsigned -> signed
744 {
745 std::size_t old_width = to_unsignedbv_type(old_type).get_width();
746 if(new_width >= old_width + 1)
747 return; // always ok
748
750 op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
751
754 "arithmetic overflow on unsigned to signed type conversion",
755 "overflow",
756 false, // fatal
758 expr,
759 guard);
760 }
761 else if(old_type.id() == ID_floatbv) // float -> signed
762 {
763 // Note that the fractional part is truncated!
766 upper.from_integer(power(2, new_width - 1));
768 op, ID_lt, upper.to_expr());
769
771 lower.from_integer(-power(2, new_width - 1) - 1);
773 op, ID_gt, lower.to_expr());
774
777 "arithmetic overflow on float to signed integer type conversion",
778 "overflow",
779 false, // fatal
781 expr,
782 guard);
783 }
784 }
785 else if(type.id() == ID_unsignedbv)
786 {
787 std::size_t new_width = to_unsignedbv_type(type).get_width();
788
789 if(old_type.id() == ID_signedbv) // signed -> unsigned
790 {
791 std::size_t old_width = to_signedbv_type(old_type).get_width();
792
793 if(new_width >= old_width - 1)
794 {
795 // only need lower bound check
797 op, ID_ge, from_integer(0, old_type));
798
801 "arithmetic overflow on signed to unsigned type conversion",
802 "overflow",
803 false, // fatal
805 expr,
806 guard);
807 }
808 else
809 {
810 // need both
812 op, ID_le, from_integer(power(2, new_width) - 1, old_type));
813
815 op, ID_ge, from_integer(0, old_type));
816
819 "arithmetic overflow on signed to unsigned type conversion",
820 "overflow",
821 false, // fatal
823 expr,
824 guard);
825 }
826 }
827 else if(old_type.id() == ID_unsignedbv) // unsigned -> unsigned
828 {
829 std::size_t old_width = to_unsignedbv_type(old_type).get_width();
830 if(new_width >= old_width)
831 return; // always ok
832
834 op, ID_le, from_integer(power(2, new_width) - 1, old_type));
835
838 "arithmetic overflow on unsigned to unsigned type conversion",
839 "overflow",
840 false, // fatal
842 expr,
843 guard);
844 }
845 else if(old_type.id() == ID_floatbv) // float -> unsigned
846 {
847 // Note that the fractional part is truncated!
850 upper.from_integer(power(2, new_width));
852 op, ID_lt, upper.to_expr());
853
855 lower.from_integer(-1);
857 op, ID_gt, lower.to_expr());
858
861 "arithmetic overflow on float to unsigned integer type conversion",
862 "overflow",
863 false, // fatal
865 expr,
866 guard);
867 }
868 }
869 }
870}
871
873 const exprt &expr,
874 const guardt &guard)
875{
877 return;
878
879 // First, check type.
880 const typet &type = expr.type();
881
883 return;
884
886 return;
887
888 // add overflow subgoal
889
890 if(expr.id() == ID_div)
891 {
892 // undefined for signed division INT_MIN/-1
893 if(type.id() == ID_signedbv)
894 {
895 const auto &div_expr = to_div_expr(expr);
896
898 div_expr.dividend(), to_signedbv_type(type).smallest_expr());
899
900 equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
901
904 "arithmetic overflow on signed division",
905 "overflow",
906 false, // fatal
908 expr,
909 guard);
910 }
911
912 return;
913 }
914 else if(expr.id() == ID_unary_minus)
915 {
916 if(type.id() == ID_signedbv)
917 {
918 // overflow on unary- on signed integers can only happen with the
919 // smallest representable number 100....0
920
922 to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
923
926 "arithmetic overflow on signed unary minus",
927 "overflow",
928 false, // fatal
930 expr,
931 guard);
932 }
933 else if(type.id() == ID_unsignedbv)
934 {
935 // Overflow on unary- on unsigned integers happens for all operands
936 // that are not zero.
937
939 to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr());
940
943 "arithmetic overflow on unsigned unary minus",
944 "overflow",
945 false, // fatal
947 expr,
948 guard);
949 }
950
951 return;
952 }
953 else if(expr.id() == ID_shl)
954 {
955 if(type.id() == ID_signedbv)
956 {
957 const auto &shl_expr = to_shl_expr(expr);
958 const auto &op = shl_expr.op();
959 const auto &op_type = to_signedbv_type(type);
960 const auto op_width = op_type.get_width();
961 const auto &distance = shl_expr.distance();
962 const auto &distance_type = distance.type();
963
964 // a left shift of a negative value is undefined;
965 // yet this isn't an overflow
967
968 if(op_type.id() == ID_unsignedbv)
970 else
973
974 // a shift with negative distance is undefined;
975 // yet this isn't an overflow
977
978 if(distance_type.id() == ID_unsignedbv)
980 else
981 {
983 distance, ID_lt, from_integer(0, distance_type));
984 }
985
986 // shifting a non-zero value by more than its width is undefined;
987 // yet this isn't an overflow
990
992
994 new_type.set_width(op_width * 2);
995
996 const exprt op_ext = typecast_exprt(op, new_type);
997
998 const exprt op_ext_shifted = shl_exprt(op_ext, distance);
999
1000 // The semantics of signed left shifts are contentious for the case
1001 // that a '1' is shifted into the signed bit.
1002 // Assuming 32-bit integers, 1<<31 is implementation-defined
1003 // in ANSI C and C++98, but is explicitly undefined by C99,
1004 // C11 and C++11.
1005 bool allow_shift_into_sign_bit = true;
1006
1007 if(mode == ID_C)
1008 {
1009 if(
1012 {
1014 }
1015 }
1016 else if(mode == ID_cpp)
1017 {
1018 if(
1022 {
1024 }
1025 }
1026
1027 const unsigned number_of_top_bits =
1029
1032 new_type.get_width() - number_of_top_bits,
1034
1035 const exprt top_bits_zero =
1037
1038 // a negative distance shift isn't an overflow;
1039 // a negative value shift isn't an overflow;
1040 // a shift that's too far isn't an overflow;
1041 // a shift of zero isn't overflow;
1042 // else check the top bits
1048 op_zero,
1049 top_bits_zero}),
1050 "arithmetic overflow on signed shl",
1051 "overflow",
1052 false, // fatal
1053 expr.find_source_location(),
1054 expr,
1055 guard);
1056 }
1057
1058 return;
1059 }
1060
1062 "overflow-" + expr.id_string(), expr.operands(), bool_typet());
1063
1064 if(expr.operands().size() >= 3)
1065 {
1066 // The overflow checks are binary!
1067 // We break these up.
1068
1069 for(std::size_t i = 1; i < expr.operands().size(); i++)
1070 {
1071 exprt tmp;
1072
1073 if(i == 1)
1074 tmp = to_multi_ary_expr(expr).op0();
1075 else
1076 {
1077 tmp = expr;
1078 tmp.operands().resize(i);
1079 }
1080
1081 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1082
1084 not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
1085 "arithmetic overflow on " + kind + " " + expr.id_string(),
1086 "overflow",
1087 false, // fatal
1088 expr.find_source_location(),
1089 expr,
1090 guard);
1091 }
1092 }
1093 else if(expr.operands().size() == 2)
1094 {
1095 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1096
1097 const binary_exprt &bexpr = to_binary_expr(expr);
1099 not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
1100 "arithmetic overflow on " + kind + " " + expr.id_string(),
1101 "overflow",
1102 false, // fatal
1103 expr.find_source_location(),
1104 expr,
1105 guard);
1106 }
1107 else
1108 {
1109 PRECONDITION(expr.id() == ID_unary_minus);
1110
1111 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1112
1115 "arithmetic overflow on " + kind + " " + expr.id_string(),
1116 "overflow",
1117 false, // fatal
1118 expr.find_source_location(),
1119 expr,
1120 guard);
1121 }
1122}
1123
1125{
1127 return;
1128
1129 // First, check type.
1130 const typet &type = expr.type();
1131
1132 if(type.id() != ID_floatbv)
1133 return;
1134
1135 // add overflow subgoal
1136
1137 if(expr.id() == ID_typecast)
1138 {
1139 // Can overflow if casting from larger
1140 // to smaller type.
1141 const auto &op = to_typecast_expr(expr).op();
1142 if(op.type().id() == ID_floatbv)
1143 {
1144 // float-to-float
1146
1148 std::move(overflow_check),
1149 "arithmetic overflow on floating-point typecast",
1150 "overflow",
1151 false, // fatal
1152 expr.find_source_location(),
1153 expr,
1154 guard);
1155 }
1156 else
1157 {
1158 // non-float-to-float
1160 not_exprt(isinf_exprt(expr)),
1161 "arithmetic overflow on floating-point typecast",
1162 "overflow",
1163 false, // fatal
1164 expr.find_source_location(),
1165 expr,
1166 guard);
1167 }
1168
1169 return;
1170 }
1171 else if(expr.id() == ID_div)
1172 {
1173 // Can overflow if dividing by something small
1175 isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
1176
1178 std::move(overflow_check),
1179 "arithmetic overflow on floating-point division",
1180 "overflow",
1181 false, // fatal
1182 expr.find_source_location(),
1183 expr,
1184 guard);
1185
1186 return;
1187 }
1188 else if(expr.id() == ID_mod)
1189 {
1190 // Can't overflow
1191 return;
1192 }
1193 else if(expr.id() == ID_unary_minus)
1194 {
1195 // Can't overflow
1196 return;
1197 }
1198 else if(expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_minus)
1199 {
1200 if(expr.operands().size() == 2)
1201 {
1202 // Can overflow
1204 isinf_exprt(to_binary_expr(expr).op0()),
1205 isinf_exprt(to_binary_expr(expr).op1()),
1206 not_exprt(isinf_exprt(expr)));
1207
1208 std::string kind = expr.id() == ID_plus ? "addition"
1209 : expr.id() == ID_minus ? "subtraction"
1210 : expr.id() == ID_mult ? "multiplication"
1211 : "";
1212
1214 std::move(overflow_check),
1215 "arithmetic overflow on floating-point " + kind,
1216 "overflow",
1217 false, // fatal
1218 expr.find_source_location(),
1219 expr,
1220 guard);
1221
1222 return;
1223 }
1224 else if(expr.operands().size() >= 3)
1225 {
1226 DATA_INVARIANT(expr.id() != ID_minus, "minus expression must be binary");
1227
1228 // break up
1230 return;
1231 }
1232 }
1233}
1234
1236{
1237 if(!enable_nan_check)
1238 return;
1239
1240 // first, check type
1241 if(expr.type().id() != ID_floatbv)
1242 return;
1243
1244 if(
1245 expr.id() != ID_plus && expr.id() != ID_mult && expr.id() != ID_div &&
1246 expr.id() != ID_minus)
1247 return;
1248
1249 // add NaN subgoal
1250
1251 exprt isnan;
1252
1253 if(expr.id() == ID_div)
1254 {
1255 const auto &div_expr = to_div_expr(expr);
1256
1257 // there a two ways to get a new NaN on division:
1258 // 0/0 = NaN and x/inf = NaN
1259 // (note that x/0 = +-inf for x!=0 and x!=inf)
1262 div_expr.op0(), from_integer(0, div_expr.dividend().type())),
1264 div_expr.op1(), from_integer(0, div_expr.divisor().type())));
1265
1266 const isinf_exprt div_inf(div_expr.op1());
1267
1269 }
1270 else if(expr.id() == ID_mult)
1271 {
1272 if(expr.operands().size() >= 3)
1273 return nan_check(make_binary(expr), guard);
1274
1275 const auto &mult_expr = to_mult_expr(expr);
1276
1277 // Inf * 0 is NaN
1279 isinf_exprt(mult_expr.op0()),
1281 mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
1282
1285 mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
1286 isinf_exprt(mult_expr.op0()));
1287
1289 }
1290 else if(expr.id() == ID_plus)
1291 {
1292 if(expr.operands().size() >= 3)
1293 return nan_check(make_binary(expr), guard);
1294
1295 const auto &plus_expr = to_plus_expr(expr);
1296
1297 // -inf + +inf = NaN and +inf + -inf = NaN,
1298 // i.e., signs differ
1302
1303 isnan = or_exprt(
1304 and_exprt(
1307 and_exprt(
1310 }
1311 else if(expr.id() == ID_minus)
1312 {
1313 // +inf - +inf = NaN and -inf - -inf = NaN,
1314 // i.e., signs match
1315
1316 const auto &minus_expr = to_minus_expr(expr);
1317
1318 ieee_float_spect spec =
1322
1323 isnan = or_exprt(
1324 and_exprt(
1327 and_exprt(
1330 }
1331 else
1333
1336 "NaN on " + expr.id_string(),
1337 "NaN",
1338 false, // fatal
1339 expr.find_source_location(),
1340 expr,
1341 guard);
1342}
1343
1345 const binary_exprt &expr,
1346 const guardt &guard)
1347{
1349 return;
1350
1351 if(
1352 expr.op0().type().id() == ID_pointer &&
1353 expr.op1().type().id() == ID_pointer)
1354 {
1355 // add same-object subgoal
1356
1357 exprt same_object = ::same_object(expr.op0(), expr.op1());
1358
1361 "same object violation",
1362 "pointer",
1363 false, // fatal
1364 expr.find_source_location(),
1365 expr,
1366 guard);
1367
1368 for(const auto &pointer : expr.operands())
1369 {
1370 // just this particular byte must be within object bounds or one past the
1371 // end
1372 const auto size = from_integer(0, size_type());
1373 auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1374
1375 for(const auto &c : conditions)
1376 {
1378 c.assertion,
1379 "pointer relation: " + c.description,
1380 "pointer arithmetic",
1381 true, // fatal
1382 expr.find_source_location(),
1383 pointer,
1384 guard);
1385 }
1386 }
1387 }
1388}
1389
1391 const exprt &expr,
1392 const guardt &guard)
1393{
1395 return;
1396
1397 if(expr.id() != ID_plus && expr.id() != ID_minus)
1398 return;
1399
1401 expr.operands().size() == 2,
1402 "pointer arithmetic expected to have exactly 2 operands");
1403
1404 // multiplying the offset by the object size must not result in arithmetic
1405 // overflow
1406 const typet &object_type = to_pointer_type(expr.type()).base_type();
1407 if(object_type.id() != ID_empty)
1408 {
1409 auto size_of_expr_opt = size_of_expr(object_type, ns);
1410 CHECK_RETURN(size_of_expr_opt.has_value());
1412
1414 exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer
1415 ? binary_expr.rhs()
1416 : binary_expr.lhs();
1417 mult_exprt mul{
1420 mul.add_source_location() = offset_operand.source_location();
1421
1423 override_overflow.set_flag(
1424 enable_signed_overflow_check, true, "signed_overflow_check");
1425 override_overflow.set_flag(
1426 enable_unsigned_overflow_check, true, "unsigned_overflow_check");
1428 }
1429
1430 // the result must be within object bounds or one past the end
1431 const auto size = from_integer(0, size_type());
1432 auto conditions = get_pointer_dereferenceable_conditions(expr, size);
1433
1434 for(const auto &c : conditions)
1435 {
1437 c.assertion,
1438 "pointer arithmetic: " + c.description,
1439 "pointer arithmetic",
1440 true, // fatal
1441 expr.find_source_location(),
1442 expr,
1443 guard);
1444 }
1445}
1446
1448 const dereference_exprt &expr,
1449 const exprt &src_expr,
1450 const guardt &guard)
1451{
1453 return;
1454
1455 const exprt &pointer = expr.pointer();
1456
1457 exprt size;
1458
1459 if(expr.type().id() == ID_empty)
1460 {
1461 // a dereference *p (with p being a pointer to void) is valid if p points to
1462 // valid memory (of any size). the smallest possible size of the memory
1463 // segment p could be pointing to is 1, hence we use this size for the
1464 // address check
1465 size = from_integer(1, size_type());
1466 }
1467 else
1468 {
1469 auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1470 CHECK_RETURN(size_of_expr_opt.has_value());
1471 size = size_of_expr_opt.value();
1472 }
1473
1474 auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1475
1476 for(const auto &c : conditions)
1477 {
1479 c.assertion,
1480 "dereference failure: " + c.description,
1481 "pointer dereference",
1482 true, // fatal
1483 src_expr.find_source_location(),
1484 src_expr,
1485 guard);
1486 }
1487}
1488
1490 const exprt &expr,
1491 const guardt &guard)
1492{
1494 return;
1495
1496 if(expr.source_location().is_built_in())
1497 return;
1498
1499 const exprt pointer =
1500 (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
1501 ? to_r_or_w_ok_expr(expr).pointer()
1503 ? to_prophecy_r_or_w_ok_expr(expr).pointer()
1504 : to_unary_expr(expr).op();
1505
1506 CHECK_RETURN(pointer.type().id() == ID_pointer);
1507
1508 if(pointer.id() == ID_symbol)
1509 {
1510 const auto &symbol_expr = to_symbol_expr(pointer);
1511
1512 if(symbol_expr.get_identifier().starts_with(CPROVER_PREFIX))
1513 return;
1514 }
1515
1517 pointer, from_integer(0, size_type()));
1518 for(const auto &c : conditions)
1519 {
1521 or_exprt{null_object(pointer), c.assertion},
1522 c.description,
1523 "pointer primitives",
1524 false, // fatal
1525 expr.source_location(),
1526 expr,
1527 guard);
1528 }
1529}
1530
1532{
1533 // we don't need to include the __CPROVER_same_object primitive here as it
1534 // is replaced by lower level primitives in the special function handling
1535 // during typechecking (see c_typecheck_expr.cpp)
1536
1537 // pointer_object and pointer_offset are well-defined for an arbitrary
1538 // pointer-typed operand (and the operands themselves have been checked
1539 // separately for, e.g., invalid pointer dereferencing via check_rec):
1540 // pointer_object and pointer_offset just extract a subset of bits from the
1541 // pointer. If that pointer was unconstrained (non-deterministic), the result
1542 // will equally be non-deterministic.
1543 return can_cast_expr<object_size_exprt>(expr) || expr.id() == ID_r_ok ||
1544 expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
1546 expr.id() == ID_is_dynamic_object;
1547}
1548
1551 const exprt &address,
1552 const exprt &size)
1553{
1554 auto conditions =
1556 if(auto maybe_null_condition = get_pointer_is_null_condition(address, size))
1557 {
1558 conditions.push_front(*maybe_null_condition);
1559 }
1560 return conditions;
1561}
1562
1563std::string goto_check_ct::array_name(const exprt &expr)
1564{
1565 return ::array_name(ns, expr);
1566}
1567
1569{
1571 return;
1572
1573 if(expr.id() == ID_index)
1575 else if(
1576 (expr.id() == ID_count_leading_zeros &&
1577 !to_count_leading_zeros_expr(expr).zero_permitted()) ||
1578 (expr.id() == ID_count_trailing_zeros &&
1579 !to_count_trailing_zeros_expr(expr).zero_permitted()))
1580 {
1582 }
1583}
1584
1586 const index_exprt &expr,
1587 const guardt &guard)
1588{
1589 const typet &array_type = expr.array().type();
1590
1591 if(array_type.id() == ID_pointer)
1592 throw "index got pointer as array type";
1593 else if(array_type.id() != ID_array && array_type.id() != ID_vector)
1594 throw "bounds check expected array or vector type, got " +
1595 array_type.id_string();
1596
1597 std::string name = array_name(expr.array());
1598
1599 const exprt &index = expr.index();
1601 ode.build(expr, ns);
1602
1603 if(index.type().id() != ID_unsignedbv)
1604 {
1605 // we undo typecasts to signedbv
1606 if(
1607 index.id() == ID_typecast &&
1608 to_typecast_expr(index).op().type().id() == ID_unsignedbv)
1609 {
1610 // ok
1611 }
1612 else
1613 {
1614 const auto i = numeric_cast<mp_integer>(index);
1615
1616 if(!i.has_value() || *i < 0)
1617 {
1618 exprt effective_offset = ode.offset();
1619
1620 if(ode.root_object().id() == ID_dereference)
1621 {
1622 exprt p_offset =
1623 pointer_offset(to_dereference_expr(ode.root_object()).pointer());
1624
1626 p_offset,
1628 effective_offset, p_offset.type())};
1629 }
1630
1631 exprt zero = from_integer(0, effective_offset.type());
1632
1633 // the final offset must not be negative
1635 effective_offset, ID_ge, std::move(zero));
1636
1638 inequality,
1639 name + " lower bound",
1640 "array bounds",
1641 true, // fatal
1642 expr.find_source_location(),
1643 expr,
1644 guard);
1645 }
1646 }
1647 }
1648
1649 if(ode.root_object().id() == ID_dereference)
1650 {
1651 const exprt &pointer = to_dereference_expr(ode.root_object()).pointer();
1652
1654 ode.offset(),
1656 pointer_offset(pointer), ode.offset().type())};
1657
1660 ID_lt,
1662 object_size(pointer), effective_offset.type())};
1663
1666 pointer,
1667 plus_exprt{ode.offset(), from_integer(1, ode.offset().type())});
1668
1671
1673 precond,
1674 name + " dynamic object upper bound",
1675 "array bounds",
1676 false, // fatal
1677 expr.find_source_location(),
1678 expr,
1679 guard);
1680
1681 return;
1682 }
1683
1684 const exprt &size = array_type.id() == ID_array
1685 ? to_array_type(array_type).size()
1686 : to_vector_type(array_type).size();
1687
1688 if(size.is_nil() && !array_type.get_bool(ID_C_flexible_array_member))
1689 {
1690 // Linking didn't complete, we don't have a size.
1691 // Not clear what to do.
1692 }
1693 else if(size.id() == ID_infinity)
1694 {
1695 }
1696 else if(
1697 expr.array().id() == ID_member &&
1698 (size.is_zero() || array_type.get_bool(ID_C_flexible_array_member)))
1699 {
1700 // a variable sized struct member
1701 //
1702 // Excerpt from the C standard on flexible array members:
1703 // However, when a . (or ->) operator has a left operand that is (a pointer
1704 // to) a structure with a flexible array member and the right operand names
1705 // that member, it behaves as if that member were replaced with the longest
1706 // array (with the same element type) that would not make the structure
1707 // larger than the object being accessed; [...]
1708 const auto type_size_opt =
1709 pointer_offset_size(ode.root_object().type(), ns);
1710 CHECK_RETURN(type_size_opt.has_value());
1711
1713 ode.offset(),
1714 ID_lt,
1715 from_integer(type_size_opt.value(), ode.offset().type()));
1716
1718 inequality,
1719 name + " upper bound",
1720 "array bounds",
1721 true, // fatal
1722 expr.find_source_location(),
1723 expr,
1724 guard);
1725 }
1726 else
1727 {
1729 typecast_exprt::conditional_cast(index, size.type()), ID_lt, size};
1730
1732 inequality,
1733 name + " upper bound",
1734 "array bounds",
1735 true, // fatal
1736 expr.find_source_location(),
1737 expr,
1738 guard);
1739 }
1740}
1741
1743 const unary_exprt &expr,
1744 const guardt &guard)
1745{
1746 std::string name;
1747
1748 if(expr.id() == ID_count_leading_zeros)
1749 name = "leading";
1750 else if(expr.id() == ID_count_trailing_zeros)
1751 name = "trailing";
1752 else
1753 PRECONDITION(false);
1754
1756 notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
1757 "count " + name + " zeros is undefined for value zero",
1758 "bit count",
1759 false, // fatal
1760 expr.find_source_location(),
1761 expr,
1762 guard);
1763}
1764
1766 const exprt &asserted_expr,
1767 const std::string &comment,
1768 const std::string &property_class,
1769 bool is_fatal,
1770 const source_locationt &source_location,
1771 const exprt &src_expr,
1772 const guardt &guard)
1773{
1774 // first try simplifier on it
1775 exprt simplified_expr =
1777
1778 // throw away trivial properties?
1779 if(!retain_trivial && simplified_expr.is_true())
1780 return;
1781
1782 // add the guard
1783 exprt guarded_expr = guard(simplified_expr);
1784
1785 if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1786 {
1787 std::string source_expr_string;
1789
1790 source_locationt annotated_location = source_location;
1791 annotated_location.set_comment(comment + " in " + source_expr_string);
1792 annotated_location.set_property_class(property_class);
1793
1795
1797 {
1799 std::move(guarded_expr), annotated_location));
1800 }
1801 else
1802 {
1803 if(is_fatal)
1804 annotated_location.property_fatal(true);
1805
1807 std::move(guarded_expr), annotated_location));
1808 }
1809 }
1810}
1811
1813{
1814 // we don't look into quantifiers
1815 if(expr.id() == ID_exists || expr.id() == ID_forall)
1816 return;
1817
1818 if(expr.id() == ID_dereference)
1819 {
1820 check_rec(to_dereference_expr(expr).pointer(), guard, false);
1821 }
1822 else if(expr.id() == ID_index)
1823 {
1824 const index_exprt &index_expr = to_index_expr(expr);
1826 check_rec(index_expr.index(), guard, false);
1827 }
1828 else
1829 {
1830 for(const auto &operand : expr.operands())
1832 }
1833}
1834
1836{
1838 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
1839 INVARIANT(
1840 expr.is_boolean(),
1841 "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
1842
1843 exprt::operandst constraints;
1844
1845 for(const auto &op : expr.operands())
1846 {
1847 INVARIANT(
1848 op.is_boolean(),
1849 "'" + expr.id_string() + "' takes Boolean operands only, but got " +
1850 op.pretty());
1851
1852 auto new_guard = [&guard, &constraints](exprt expr) {
1853 return guard(implication(conjunction(constraints), expr));
1854 };
1855
1856 check_rec(op, new_guard, false);
1857
1858 constraints.push_back(expr.id() == ID_or ? boolean_negate(op) : op);
1859 }
1860}
1861
1863{
1864 INVARIANT(
1865 if_expr.cond().is_boolean(),
1866 "first argument of if must be boolean, but got " + if_expr.cond().pretty());
1867
1868 check_rec(if_expr.cond(), guard, false);
1869
1870 {
1871 auto new_guard = [&guard, &if_expr](exprt expr) {
1872 return guard(implication(if_expr.cond(), std::move(expr)));
1873 };
1874 check_rec(if_expr.true_case(), new_guard, false);
1875 }
1876
1877 {
1878 auto new_guard = [&guard, &if_expr](exprt expr) {
1879 return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
1880 };
1881 check_rec(if_expr.false_case(), new_guard, false);
1882 }
1883}
1884
1886 const member_exprt &member,
1887 const guardt &guard)
1888{
1890
1891 check_rec(deref.pointer(), guard, false);
1892
1893 // avoid building the following expressions when pointer_validity_check
1894 // would return immediately anyway
1896 return true;
1897
1898 // we rewrite s->member into *(s+member_offset)
1899 // to avoid requiring memory safety of the entire struct
1900 auto member_offset_opt = member_offset_expr(member, ns);
1901
1902 if(member_offset_opt.has_value())
1903 {
1905 new_pointer_type.base_type() = member.type();
1906
1908 deref.pointer(), pointer_type(char_type()));
1909
1911 plus_exprt{
1916
1918 new_deref.add_source_location() = deref.source_location();
1920
1921 return true;
1922 }
1923 return false;
1924}
1925
1927 const div_exprt &div_expr,
1928 const guardt &guard)
1929{
1930 if(
1931 div_expr.type().id() == ID_signedbv ||
1932 div_expr.type().id() == ID_unsignedbv || div_expr.type().id() == ID_c_bool)
1933 {
1934 // Division by zero is undefined behavior for all integer types.
1936 }
1937 else if(div_expr.type().id() == ID_floatbv)
1938 {
1939 // Division by zero on floating-point numbers may be undefined behavior.
1940 // Annex F of the ISO C21 suggests that implementations that
1941 // define __STDC_IEC_559__ follow IEEE 754 semantics,
1942 // which defines the outcome of division by zero.
1944 }
1945
1946 if(div_expr.type().id() == ID_signedbv)
1948 else if(div_expr.type().id() == ID_floatbv)
1949 {
1952 }
1953}
1954
1956 const exprt &expr,
1957 const guardt &guard)
1958{
1959 if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1960 {
1962
1963 if(
1964 expr.operands().size() == 2 && expr.id() == ID_minus &&
1965 expr.operands()[0].type().id() == ID_pointer &&
1966 expr.operands()[1].type().id() == ID_pointer)
1967 {
1969 }
1970 }
1971 else if(expr.type().id() == ID_floatbv)
1972 {
1973 nan_check(expr, guard);
1975 }
1976 else if(expr.type().id() == ID_pointer)
1977 {
1979 }
1980}
1981
1983 const exprt &expr,
1984 const guardt &guard,
1985 bool is_assigned)
1986{
1987 if(expr.id() == ID_exists || expr.id() == ID_forall)
1988 {
1989 // the scoped variables may be used in the assertion
1990 const auto &quantifier_expr = to_quantifier_expr(expr);
1991
1992 auto new_guard = [&guard, &quantifier_expr](exprt expr) {
1993 return guard(forall_exprt(quantifier_expr.symbol(), expr));
1994 };
1995
1996 check_rec(quantifier_expr.where(), new_guard, false);
1997 return;
1998 }
1999 else if(expr.id() == ID_address_of)
2000 {
2002 return;
2003 }
2004 else if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
2005 {
2007 return;
2008 }
2009 else if(expr.id() == ID_if)
2010 {
2012 return;
2013 }
2014 else if(
2015 expr.id() == ID_member &&
2016 to_member_expr(expr).struct_op().id() == ID_dereference)
2017 {
2019 return;
2020 }
2021
2022 for(const auto &op : expr.operands())
2023 check_rec(op, guard, false);
2024
2025 if(expr.type().id() == ID_c_enum_tag)
2027
2028 if(expr.id() == ID_index)
2029 {
2030 bounds_check(expr, guard);
2031 }
2032 else if(expr.id() == ID_div)
2033 {
2035 }
2036 else if(expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr)
2037 {
2039
2040 if(expr.id() == ID_shl && expr.type().id() == ID_signedbv)
2042 }
2043 else if(expr.id() == ID_mod)
2044 {
2047 }
2048 else if(
2049 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
2050 expr.id() == ID_unary_minus)
2051 {
2053 }
2054 else if(expr.id() == ID_typecast)
2055 conversion_check(expr, guard);
2056 else if(
2057 expr.id() == ID_le || expr.id() == ID_lt || expr.id() == ID_ge ||
2058 expr.id() == ID_gt)
2060 else if(expr.id() == ID_dereference)
2061 {
2063 }
2065 {
2067 }
2068 else if(
2069 expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
2070 {
2071 bounds_check(expr, guard);
2072 }
2073}
2074
2076{
2078}
2079
2081{
2082 const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
2083 const symbol_exprt leak_expr = leak.symbol_expr();
2084
2085 // add self-assignment to get helpful counterexample output
2087
2088 source_locationt source_location;
2089 source_location.set_function(function_id);
2090
2092
2094 eq,
2095 "dynamically allocated memory never freed",
2096 "memory-leak",
2097 false, // fatal
2098 source_location,
2099 eq,
2100 identity);
2101}
2102
2104 const irep_idt &function_identifier,
2105 goto_functiont &goto_function)
2106{
2107 const auto &function_symbol = ns.lookup(function_identifier);
2108 mode = function_symbol.mode;
2109
2110 if(mode != ID_C && mode != ID_cpp)
2111 return;
2112
2113 assertions.clear();
2114
2115 bool did_something = false;
2116
2118 std::make_unique<local_bitvector_analysist>(goto_function, ns);
2119
2120 goto_programt &goto_program = goto_function.body;
2121
2122 Forall_goto_program_instructions(it, goto_program)
2123 {
2124 current_target = it;
2126
2128 const auto &pragmas = i.source_location().get_pragmas();
2129 for(const auto &d : pragmas)
2130 {
2131 // match named-check related pragmas
2132 auto matched = match_named_check(d.first);
2133 if(matched.has_value())
2134 {
2135 auto named_check = matched.value();
2136 auto name = named_check.first;
2137 auto status = named_check.second;
2138 bool *flag = name_to_flag.find(name)->second;
2139 switch(status)
2140 {
2142 resetter.set_flag(*flag, true, name);
2143 break;
2145 resetter.set_flag(*flag, false, name);
2146 break;
2148 resetter.disable_flag(*flag, name);
2149 break;
2150 }
2151 }
2152 }
2153
2154 // add checked pragmas for all active checks
2156
2157 new_code.clear();
2158
2159 // we clear all recorded assertions if
2160 // 1) we want to generate all assertions or
2161 // 2) the instruction is a branch target
2162 if(retain_trivial || i.is_target())
2163 assertions.clear();
2164
2165 if(i.has_condition())
2166 {
2167 check(i.condition(), false);
2168 }
2169
2170 // magic ERROR label?
2171 for(const auto &label : error_labels)
2172 {
2173 if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end())
2174 {
2176 annotated_location.set_property_class("error label");
2177 annotated_location.set_comment("error label " + label);
2178 annotated_location.set("user-provided", true);
2179
2181 {
2182 new_code.add(
2184 }
2185 else
2186 {
2187 new_code.add(
2189 }
2190 }
2191 }
2192
2193 if(i.is_other())
2194 {
2195 const auto &code = i.get_other();
2196 const irep_idt &statement = code.get_statement();
2197
2198 if(statement == ID_expression)
2199 {
2200 check(code, false);
2201 }
2202 else if(statement == ID_printf)
2203 {
2204 for(const auto &op : code.operands())
2205 check(op, false);
2206 }
2207 }
2208 else if(i.is_assign())
2209 {
2210 const exprt &assign_lhs = i.assign_lhs();
2211 const exprt &assign_rhs = i.assign_rhs();
2212
2213 check(assign_lhs, true);
2214 check(assign_rhs, false);
2215
2216 // the LHS might invalidate any assertion
2217 invalidate(assign_lhs);
2218 }
2219 else if(i.is_function_call())
2220 {
2221 check(i.call_lhs(), true);
2222 check(i.call_function(), false);
2223
2224 for(const auto &arg : i.call_arguments())
2225 check(arg, false);
2226
2228
2229 // the call might invalidate any assertion
2230 assertions.clear();
2231 }
2232 else if(i.is_set_return_value())
2233 {
2234 check(i.return_value(), false);
2235 // the return value invalidate any assertion
2237 }
2238 else if(i.is_throw())
2239 {
2240 // this has no successor
2241 assertions.clear();
2242 }
2243 else if(i.is_assume())
2244 {
2245 // These are further 'exit points' of the program
2247 if(
2249 (function_identifier == "abort" || function_identifier == "exit" ||
2250 function_identifier == "_Exit" ||
2251 (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
2252 {
2253 memory_leak_check(function_identifier);
2254 }
2255 }
2256 else if(i.is_dead())
2257 {
2259 {
2260 const symbol_exprt &variable = i.dead_symbol();
2261
2262 // is it dirty?
2263 if(local_bitvector_analysis->dirty(variable))
2264 {
2265 // need to mark the dead variable as dead
2266 exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2268 address_of_exprt(variable), lhs.type());
2269 if_exprt rhs(
2271 std::move(address_of_expr),
2272 lhs);
2274 code_assignt{std::move(lhs), std::move(rhs), i.source_location()},
2275 i.source_location()));
2276 }
2277 }
2278 }
2279 else if(i.is_end_function())
2280 {
2281 if(
2282 function_identifier == goto_functionst::entry_point() &&
2284 {
2285 memory_leak_check(function_identifier);
2286 }
2287 }
2288
2289 for(auto &instruction : new_code.instructions)
2290 {
2291 if(instruction.source_location().is_nil())
2292 {
2293 instruction.source_location_nonconst().id(irep_idt());
2294
2295 if(!it->source_location().get_file().empty())
2296 instruction.source_location_nonconst().set_file(
2297 it->source_location().get_file());
2298
2299 if(!it->source_location().get_line().empty())
2300 instruction.source_location_nonconst().set_line(
2301 it->source_location().get_line());
2302
2303 if(!it->source_location().get_function().empty())
2304 instruction.source_location_nonconst().set_function(
2305 it->source_location().get_function());
2306
2307 if(!it->source_location().get_column().empty())
2308 {
2309 instruction.source_location_nonconst().set_column(
2310 it->source_location().get_column());
2311 }
2312 }
2313 }
2314
2315 // insert new instructions -- make sure targets are not moved
2317
2318 while(!new_code.instructions.empty())
2319 {
2320 goto_program.insert_before_swap(it, new_code.instructions.front());
2321 new_code.instructions.pop_front();
2322 it++;
2323 }
2324 }
2325
2326 if(did_something)
2327 remove_skip(goto_program);
2328}
2329
2332{
2333 if(i.call_function().id() != ID_symbol)
2334 return;
2335
2336 const irep_idt &identifier =
2337 to_symbol_expr(i.call_function()).get_identifier();
2338
2339 if(
2340 identifier == CPROVER_PREFIX "get_field" || identifier == CPROVER_PREFIX
2341 "set_field")
2342 {
2343 const exprt &expr = i.call_arguments()[0];
2344 PRECONDITION(expr.type().id() == ID_pointer);
2345 check(dereference_exprt(expr), false);
2346 }
2347}
2348
2351 const exprt &address,
2352 const exprt &size)
2353{
2355 PRECONDITION(address.type().id() == ID_pointer);
2358
2359 conditionst conditions;
2360
2363
2364 const bool unknown = flags.is_unknown() || flags.is_uninitialized();
2365
2366 if(unknown)
2367 {
2368 conditions.push_back(conditiont{
2369 not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
2370 }
2371
2372 if(unknown || flags.is_dynamic_heap())
2373 {
2374 conditions.push_back(conditiont(
2375 or_exprt(
2377 not_exprt(deallocated(address, ns))),
2378 "deallocated dynamic object"));
2379 }
2380
2381 if(unknown || flags.is_dynamic_local())
2382 {
2383 conditions.push_back(conditiont(
2384 or_exprt(
2386 not_exprt(dead_object(address, ns))),
2387 "dead object"));
2388 }
2389
2390 if(flags.is_dynamic_heap())
2391 {
2393 object_lower_bound(address, nil_exprt()),
2394 object_upper_bound(address, size));
2395
2396 conditions.push_back(conditiont(
2397 or_exprt(
2400 "pointer outside dynamic object bounds"));
2401 }
2402
2403 if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
2404 {
2406 object_lower_bound(address, nil_exprt()),
2407 object_upper_bound(address, size));
2408
2409 conditions.push_back(conditiont(
2410 or_exprt(
2413 "pointer outside object bounds"));
2414 }
2415
2416 if(unknown || flags.is_integer_address())
2417 {
2418 conditions.push_back(conditiont(
2421 "invalid integer address"));
2422 }
2423
2424 return conditions;
2425}
2426
2427std::optional<goto_check_ct::conditiont>
2429 const exprt &address,
2430 const exprt &size)
2431{
2433 PRECONDITION(address.type().id() == ID_pointer);
2436
2437 if(flags.is_unknown() || flags.is_uninitialized() || flags.is_null())
2438 {
2439 return {conditiont{
2440 or_exprt{
2442 not_exprt(null_object(address))},
2443 "pointer NULL"}};
2444 }
2445
2446 return {};
2447}
2448
2450 const exprt &pointer,
2451 const exprt &size)
2452{
2454 for(const auto &a : allocations)
2455 {
2456 typecast_exprt int_ptr(pointer, a.first.type());
2457
2459
2460 plus_exprt upper_bound{
2462
2464 std::move(upper_bound), ID_le, plus_exprt{a.first, a.second}};
2465
2466 alloc_disjuncts.push_back(
2467 and_exprt{std::move(lb_check), std::move(ub_check)});
2468 }
2470}
2471
2473 const irep_idt &function_identifier,
2474 goto_functionst::goto_functiont &goto_function,
2475 const namespacet &ns,
2476 const optionst &options,
2477 message_handlert &message_handler)
2478{
2479 goto_check_ct goto_check(ns, options, message_handler);
2480 goto_check.goto_check(function_identifier, goto_function);
2481}
2482
2484 const namespacet &ns,
2485 const optionst &options,
2486 goto_functionst &goto_functions,
2487 message_handlert &message_handler)
2488{
2489 goto_check_ct goto_check(ns, options, message_handler);
2490
2491 goto_check.collect_allocations(goto_functions);
2492
2493 for(auto &gf_entry : goto_functions.function_map)
2494 {
2495 goto_check.goto_check(gf_entry.first, gf_entry.second);
2496 }
2497}
2498
2500 const optionst &options,
2501 goto_modelt &goto_model,
2502 message_handlert &message_handler)
2503{
2504 const namespacet ns(goto_model.symbol_table);
2505 goto_check_c(ns, options, goto_model.goto_functions, message_handler);
2506}
2507
2509 source_locationt &source_location) const
2510{
2511 for(const auto &entry : name_to_flag)
2512 if(*(entry.second))
2513 source_location.add_pragma("checked:" + id2string(entry.first));
2514}
2515
2517 source_locationt &source_location) const
2518{
2519 for(const auto &entry : name_to_flag)
2520 source_location.add_pragma("checked:" + id2string(entry.first));
2521}
2522
2525{
2526 auto s = id2string(named_check);
2527 auto col = s.find(":");
2528
2529 if(col == std::string::npos)
2530 return {}; // separator not found
2531
2532 auto name = s.substr(col + 1);
2533
2534 if(name_to_flag.find(name) == name_to_flag.end())
2535 return {}; // name unknown
2536
2537 check_statust status;
2538 if(!s.compare(0, 6, "enable"))
2539 status = check_statust::ENABLE;
2540 else if(!s.compare(0, 7, "disable"))
2541 status = check_statust::DISABLE;
2542 else if(!s.compare(0, 7, "checked"))
2543 status = check_statust::CHECKED;
2544 else
2545 return {}; // prefix unknow
2546
2547 // success
2548 return std::pair<irep_idt, check_statust>{name, status};
2549}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Misc Utilities.
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
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.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
API to expression classes that are internal to the C frontend.
static exprt guard(const exprt::operandst &guards, exprt cond)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
signedbv_typet pointer_diff_type()
Definition c_types.cpp:220
bitvector_typet char_type()
Definition c_types.cpp:106
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
A base class for binary expressions.
Definition std_expr.h:638
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
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:731
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
The Boolean type.
Definition std_types.h:36
A goto_instruction_codet representing an assignment in the program.
struct configt::cppt cpp
struct configt::ansi_ct ansi_c
Operator to dereference a pointer.
Division.
Definition std_expr.h:1157
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Definition c_expr.h:327
Equality.
Definition std_expr.h:1366
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
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
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:231
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition std_expr.h:3199
~flag_overridet()
Restore the values of all flags that have been modified via set_flag.
void disable_flag(bool &flag, const irep_idt &flag_name)
Sets the given flag to false, overriding any previous value.
void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
Store the current value of flag and then set its value to new_value.
std::map< bool *, bool > flags_to_reset
flag_overridet(const source_locationt &source_location)
std::set< bool * > disabled_flags
const source_locationt & source_location
A forall expression.
std::optional< std::pair< irep_idt, check_statust > > named_check_statust
optional (named-check, status) pair
named_check_statust match_named_check(const irep_idt &named_check) const
Matches a named-check string of the form.
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
void check_rec_logical_op(const exprt &expr, const guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
bool enable_float_div_by_zero_check
void check_rec_address(const exprt &expr, const guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
std::function< exprt(exprt)> guardt
std::string array_name(const exprt &)
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
void memory_leak_check(const irep_idt &function_id)
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
std::optional< goto_check_ct::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
void float_div_by_zero_check(const div_exprt &, const guardt &)
const namespacet & ns
check_statust
activation statuses for named checks
void float_overflow_check(const exprt &, const guardt &)
bool enable_pointer_primitive_check
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
bool requires_pointer_primitive_check(const exprt &expr)
Returns true if the given expression is a pointer primitive that requires validation of the operand t...
std::map< irep_idt, bool * > name_to_flag
Maps a named-check name to the corresponding boolean flag.
std::list< conditiont > conditionst
bool enable_float_overflow_check
bool enable_conversion_check
void check_rec_div(const div_exprt &div_expr, const guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
bool enable_pointer_overflow_check
void pointer_primitive_check(const exprt &expr, const guardt &guard)
Generates VCCs to check that pointers passed to pointer primitives are either null or valid.
void bounds_check_index(const index_exprt &, const guardt &)
bool enable_signed_overflow_check
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
void check_rec(const exprt &expr, const guardt &guard, bool is_assigned)
Recursively descend into expr and run the appropriate check for each sub-expression,...
bool check_rec_member(const member_exprt &member, const guardt &guard)
Check that a member expression is valid:
goto_functionst::goto_functiont goto_functiont
void bounds_check(const exprt &, const guardt &)
void check(const exprt &expr, bool is_assigned)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
std::pair< exprt, exprt > allocationt
allocationst allocations
void pointer_overflow_check(const exprt &, const guardt &)
bool enable_memory_leak_check
void add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, bool is_fatal, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
Include the asserted_expr in the code conditioned by the guard.
void conversion_check(const exprt &, const guardt &)
void check_rec_if(const if_exprt &if_expr, const guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
void integer_overflow_check(const exprt &, const guardt &)
bool enable_assert_to_assume
bool enable_memory_cleanup_check
void nan_check(const exprt &, const guardt &)
bool enable_undefined_shift_check
std::list< allocationt > allocationst
bool enable_enum_range_check
goto_programt::const_targett current_target
void add_all_checked_named_check_pragmas(source_locationt &source_location) const
Adds "checked" pragmas for all named checks on the given source location (prevents any the instanciat...
const guardt identity
void div_by_zero_check(const div_exprt &, const guardt &)
optionst::value_listt error_labelst
void add_active_named_check_pragmas(source_locationt &source_location) const
Adds "checked" pragmas for all currently active named checks on the given source location.
assertionst assertions
void pointer_rel_check(const binary_exprt &, const guardt &)
goto_programt new_code
goto_check_ct(const namespacet &_ns, const optionst &_options, message_handlert &_message_handler)
conditionst get_pointer_points_to_valid_memory_conditions(const exprt &address, const exprt &size)
bool enable_unsigned_overflow_check
void bounds_check_bit_count(const unary_exprt &, const guardt &)
bool enable_div_by_zero_check
void check_shadow_memory_api_calls(const goto_programt::instructiont &)
error_labelst error_labels
void check_rec_arithmetic_op(const exprt &expr, const guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
void undefined_shift_check(const shift_exprt &, const guardt &)
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
void enum_range_check(const exprt &, const guardt &, bool is_assigned)
void mod_by_zero_check(const mod_exprt &, const guardt &)
std::set< std::pair< exprt, exprt > > assertionst
void pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr, const guardt &guard)
Generates VCCs for the validity of the given dereferencing operation.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
bool is_target() const
Is this node a branch target?
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
bool has_condition() const
Does this instruction have a condition?
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
const exprt & condition() const
Get the condition of gotos, assume, assert.
source_locationt & source_location_nonconst()
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::const_iterator const_targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
IEEE-floating-point equality.
static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:209
constant_exprt to_expr() const
static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:202
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
Definition ieee_float.h:330
void from_integer(const mp_integer &i)
The trinary if-then-else operator.
Definition std_expr.h:2497
Boolean implication.
Definition std_expr.h:2225
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Evaluates to true if the operand is infinite.
Extract member of struct or union.
Definition std_expr.h:2971
const exprt & struct_op() const
Definition std_expr.h:3009
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1248
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3208
Boolean negation.
Definition std_expr.h:2454
Disequality.
Definition std_expr.h:1425
The null pointer constant.
Split an expression into a base object and a (byte) offset.
std::list< std::string > value_listt
Definition options.h:25
Boolean OR.
Definition std_expr.h:2270
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A base class for shift and rotate operators.
exprt & distance()
Left shift.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
void add_pragma(const irep_idt &pragma)
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
Fixed-width bit-vector with unsigned binary interpretation.
#define CPROVER_PREFIX
static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition expr_util.cpp:38
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
bool has_symbol_expr(const exprt &src, const irep_idt &identifier, bool include_bound_symbols)
Returns true if one of the symbol expressions in src has identifier identifier; if include_bound_symb...
API to expression classes for floating-point arithmetic.
void goto_check_c(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
static exprt implication(exprt lhs, exprt rhs)
Program Transformation.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Abstract interface to support a programming language.
Field-insensitive, location-sensitive bitvector analysis.
int isnan(double d)
Definition math.c:163
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition mode.cpp:51
Options.
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
bool can_cast_expr< object_size_exprt >(const exprt &base)
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 prophecy_r_or_w_ok_exprt & to_prophecy_r_or_w_ok_expr(const exprt &expr)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool can_cast_expr< prophecy_r_or_w_ok_exprt >(const exprt &base)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
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
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:83
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:71
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1277
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1137
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1206
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1086
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2250
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
conditiont(const exprt &_assertion, const std::string &_description)
#define size_type
Definition unistd.c:186
dstringt irep_idt