CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_check_c.cpp Source File

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>
25#include <util/mathematical_expr.h>
26#include <util/message.h>
27#include <util/options.h>
28#include <util/pointer_expr.h>
29#include <util/pointer_offset_size.h>
30#include <util/pointer_predicates.h>
31#include <util/simplify_expr.h>
32#include <util/std_code.h>
33#include <util/std_expr.h>
34
35#include <goto-programs/goto_model.h>
36#include <goto-programs/remove_skip.h>
37
38#include <analyses/local_bitvector_analysis.h>
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
421 static 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 || to_symbol_expr(function).identifier() !=
448 CPROVER_PREFIX "allocated_memory")
449 continue;
450
452 instruction.call_arguments();
453 if(
454 args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
455 args[1].type().id() != ID_unsignedbv)
456 throw "expected two unsigned arguments to " CPROVER_PREFIX
457 "allocated_memory";
458
460 args[0].type() == args[1].type(),
461 "arguments of allocated_memory must have same type");
462 allocations.push_back({args[0], args[1]});
463 }
464 }
465}
466
468{
469 if(lhs.id() == ID_index)
470 invalidate(to_index_expr(lhs).array());
471 else if(lhs.id() == ID_member)
472 invalidate(to_member_expr(lhs).struct_op());
473 else if(lhs.id() == ID_symbol)
474 {
475 // clear all assertions about 'symbol'
476 const irep_idt &lhs_id = to_symbol_expr(lhs).identifier();
477
478 for(auto it = assertions.begin(); it != assertions.end();)
479 {
480 if(
481 has_symbol_expr(it->second, lhs_id, false) ||
482 has_subexpr(it->second, ID_dereference))
483 {
484 it = assertions.erase(it);
485 }
486 else
487 ++it;
488 }
489 }
490 else
491 {
492 // give up, clear all
494 }
495}
496
498 const div_exprt &expr,
499 const guardt &guard)
500{
502 return;
503
504 // add divison by zero subgoal
505
506 exprt zero = from_integer(0, expr.op1().type());
507 const notequal_exprt inequality(expr.op1(), std::move(zero));
508
511 "division by zero",
512 "division-by-zero",
513 true, // fatal
515 expr,
516 guard);
517}
518
520 const div_exprt &expr,
521 const guardt &guard)
522{
524 return;
525
526 // add divison by zero subgoal
527
528 exprt zero = from_integer(0, expr.op1().type());
529 const notequal_exprt inequality(expr.op1(), std::move(zero));
530
533 "floating-point division by zero",
534 "float-division-by-zero",
535 false, // fatal
537 expr,
538 guard);
539}
540
542 const exprt &expr,
543 const guardt &guard,
544 bool is_assigned)
545{
547 return;
548
549 if(is_assigned)
550 return; // not in range yet
551
552 // we might be looking at a lowered enum_is_in_range_exprt, skip over these
553 const auto &pragmas = expr.source_location().get_pragmas();
554 for(const auto &d : pragmas)
555 {
556 if(d.first == "disable:enum-range-check")
557 return;
558 }
559
560 const exprt check = enum_is_in_range_exprt{expr}.lower(ns);
561
563 check,
564 "enum range check",
565 "enum-range-check",
566 false, // fatal
568 expr,
569 guard);
570}
571
573 const shift_exprt &expr,
574 const guardt &guard)
575{
577 return;
578
579 // Undefined for all types and shifts if distance exceeds width,
580 // and also undefined for negative distances.
581
582 const typet &distance_type = expr.distance().type();
583
584 if(distance_type.id() == ID_signedbv)
585 {
588
591 "shift distance is negative",
592 "undefined-shift",
593 true, // fatal
595 expr,
596 guard);
597 }
598
599 const typet &op_type = expr.op().type();
600
601 if(op_type.id() == ID_unsignedbv || op_type.id() == ID_signedbv)
602 {
605
607 binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
608 "shift distance too large",
609 "undefined-shift",
610 true, // fatal
612 expr,
613 guard);
614
615 if(op_type.id() == ID_signedbv && expr.id() == ID_shl)
616 {
618 expr.op(), ID_ge, from_integer(0, op_type));
619
622 "shift operand is negative",
623 "undefined-shift",
624 true, // fatal
626 expr,
627 guard);
628 }
629 }
630 else
631 {
633 false_exprt(),
634 "shift of non-integer type",
635 "undefined-shift",
636 true, // fatal
638 expr,
639 guard);
640 }
641}
642
644 const mod_exprt &expr,
645 const guardt &guard)
646{
648 return;
649
650 // add divison by zero subgoal
651
652 exprt zero = from_integer(0, expr.divisor().type());
653 const notequal_exprt inequality(expr.divisor(), std::move(zero));
654
657 "division by zero",
658 "division-by-zero",
659 true, // fatal
661 expr,
662 guard);
663}
664
667 const mod_exprt &expr,
668 const guardt &guard)
669{
671 return;
672
673 const auto &type = expr.type();
674
675 if(type.id() == ID_signedbv)
676 {
677 // INT_MIN % -1 is, in principle, defined to be zero in
678 // ANSI C, C99, C++98, and C++11. Most compilers, however,
679 // fail to produce 0, and in some cases generate an exception.
680 // C11 explicitly makes this case undefined.
681
683 expr.op0(), to_signedbv_type(type).smallest_expr());
684
686 expr.op1(), from_integer(-1, expr.op1().type()));
687
690 "result of signed mod is not representable",
691 "overflow",
692 false, // fatal
694 expr,
695 guard);
696 }
697}
698
700{
702 return;
703
704 // First, check type.
705 const typet &type = expr.type();
706
707 if(type.id() != ID_signedbv && type.id() != ID_unsignedbv)
708 return;
709
710 if(expr.id() == ID_typecast)
711 {
712 const auto &op = to_typecast_expr(expr).op();
713
714 // conversion to signed int may overflow
715 const typet &old_type = op.type();
716
717 if(type.id() == ID_signedbv)
718 {
719 std::size_t new_width = to_signedbv_type(type).get_width();
720
721 if(old_type.id() == ID_signedbv) // signed -> signed
722 {
723 std::size_t old_width = to_signedbv_type(old_type).get_width();
724 if(new_width >= old_width)
725 return; // always ok
726
728 op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
729
731 op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
732
735 "arithmetic overflow on signed type conversion",
736 "overflow",
737 false, // fatal
739 expr,
740 guard);
741 }
742 else if(old_type.id() == ID_unsignedbv) // unsigned -> signed
743 {
744 std::size_t old_width = to_unsignedbv_type(old_type).get_width();
745 if(new_width >= old_width + 1)
746 return; // always ok
747
749 op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
750
753 "arithmetic overflow on unsigned to signed type conversion",
754 "overflow",
755 false, // fatal
757 expr,
758 guard);
759 }
760 else if(old_type.id() == ID_floatbv) // float -> signed
761 {
762 // Note that the fractional part is truncated!
765 upper.from_integer(power(2, new_width - 1));
767 op, ID_lt, upper.to_expr());
768
770 lower.from_integer(-power(2, new_width - 1) - 1);
772 op, ID_gt, lower.to_expr());
773
776 "arithmetic overflow on float to signed integer type conversion",
777 "overflow",
778 false, // fatal
780 expr,
781 guard);
782 }
783 }
784 else if(type.id() == ID_unsignedbv)
785 {
786 std::size_t new_width = to_unsignedbv_type(type).get_width();
787
788 if(old_type.id() == ID_signedbv) // signed -> unsigned
789 {
790 std::size_t old_width = to_signedbv_type(old_type).get_width();
791
792 if(new_width >= old_width - 1)
793 {
794 // only need lower bound check
796 op, ID_ge, from_integer(0, old_type));
797
800 "arithmetic overflow on signed to unsigned type conversion",
801 "overflow",
802 false, // fatal
804 expr,
805 guard);
806 }
807 else
808 {
809 // need both
811 op, ID_le, from_integer(power(2, new_width) - 1, old_type));
812
814 op, ID_ge, from_integer(0, old_type));
815
818 "arithmetic overflow on signed to unsigned type conversion",
819 "overflow",
820 false, // fatal
822 expr,
823 guard);
824 }
825 }
826 else if(old_type.id() == ID_unsignedbv) // unsigned -> unsigned
827 {
828 std::size_t old_width = to_unsignedbv_type(old_type).get_width();
829 if(new_width >= old_width)
830 return; // always ok
831
833 op, ID_le, from_integer(power(2, new_width) - 1, old_type));
834
837 "arithmetic overflow on unsigned to unsigned type conversion",
838 "overflow",
839 false, // fatal
841 expr,
842 guard);
843 }
844 else if(old_type.id() == ID_floatbv) // float -> unsigned
845 {
846 // Note that the fractional part is truncated!
849 upper.from_integer(power(2, new_width));
851 op, ID_lt, upper.to_expr());
852
854 lower.from_integer(-1);
856 op, ID_gt, lower.to_expr());
857
860 "arithmetic overflow on float to unsigned integer type conversion",
861 "overflow",
862 false, // fatal
864 expr,
865 guard);
866 }
867 }
868 }
869}
870
872 const exprt &expr,
873 const guardt &guard)
874{
876 return;
877
878 // First, check type.
879 const typet &type = expr.type();
880
882 return;
883
885 return;
886
887 // add overflow subgoal
888
889 if(expr.id() == ID_div)
890 {
891 // undefined for signed division INT_MIN/-1
892 if(type.id() == ID_signedbv)
893 {
894 const auto &div_expr = to_div_expr(expr);
895
897 div_expr.dividend(), to_signedbv_type(type).smallest_expr());
898
899 equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
900
903 "arithmetic overflow on signed division",
904 "overflow",
905 false, // fatal
907 expr,
908 guard);
909 }
910
911 return;
912 }
913 else if(expr.id() == ID_unary_minus)
914 {
915 if(type.id() == ID_signedbv)
916 {
917 // overflow on unary- on signed integers can only happen with the
918 // smallest representable number 100....0
919
921 to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
922
925 "arithmetic overflow on signed unary minus",
926 "overflow",
927 false, // fatal
929 expr,
930 guard);
931 }
932 else if(type.id() == ID_unsignedbv)
933 {
934 // Overflow on unary- on unsigned integers happens for all operands
935 // that are not zero.
936
938 to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr());
939
942 "arithmetic overflow on unsigned unary minus",
943 "overflow",
944 false, // fatal
946 expr,
947 guard);
948 }
949
950 return;
951 }
952 else if(expr.id() == ID_shl)
953 {
954 if(type.id() == ID_signedbv)
955 {
956 const auto &shl_expr = to_shl_expr(expr);
957 const auto &op = shl_expr.op();
958 const auto &op_type = to_signedbv_type(type);
959 const auto op_width = op_type.get_width();
960 const auto &distance = shl_expr.distance();
961 const auto &distance_type = distance.type();
962
963 // a left shift of a negative value is undefined;
964 // yet this isn't an overflow
966
967 if(op_type.id() == ID_unsignedbv)
969 else
972
973 // a shift with negative distance is undefined;
974 // yet this isn't an overflow
976
977 if(distance_type.id() == ID_unsignedbv)
979 else
980 {
982 distance, ID_lt, from_integer(0, distance_type));
983 }
984
985 // shifting a non-zero value by more than its width is undefined;
986 // yet this isn't an overflow
989
991
993 new_type.set_width(op_width * 2);
994
995 const exprt op_ext = typecast_exprt(op, new_type);
996
997 const exprt op_ext_shifted = shl_exprt(op_ext, distance);
998
999 // The semantics of signed left shifts are contentious for the case
1000 // that a '1' is shifted into the signed bit.
1001 // Assuming 32-bit integers, 1<<31 is implementation-defined
1002 // in ANSI C and C++98, but is explicitly undefined by C99,
1003 // C11 and C++11.
1004 bool allow_shift_into_sign_bit = true;
1005
1006 if(mode == ID_C)
1007 {
1008 if(
1011 {
1013 }
1014 }
1015 else if(mode == ID_cpp)
1016 {
1017 if(
1021 {
1023 }
1024 }
1025
1026 const unsigned number_of_top_bits =
1028
1031 new_type.get_width() - number_of_top_bits,
1033
1034 const exprt top_bits_zero =
1036
1037 // a negative distance shift isn't an overflow;
1038 // a negative value shift isn't an overflow;
1039 // a shift that's too far isn't an overflow;
1040 // a shift of zero isn't overflow;
1041 // else check the top bits
1047 op_zero,
1048 top_bits_zero}),
1049 "arithmetic overflow on signed shl",
1050 "overflow",
1051 false, // fatal
1052 expr.find_source_location(),
1053 expr,
1054 guard);
1055 }
1056
1057 return;
1058 }
1059
1061 "overflow-" + expr.id_string(), expr.operands(), bool_typet());
1062
1063 if(expr.operands().size() >= 3)
1064 {
1065 // The overflow checks are binary!
1066 // We break these up.
1067
1068 for(std::size_t i = 1; i < expr.operands().size(); i++)
1069 {
1070 exprt tmp;
1071
1072 if(i == 1)
1073 tmp = to_multi_ary_expr(expr).op0();
1074 else
1075 {
1076 tmp = expr;
1077 tmp.operands().resize(i);
1078 }
1079
1080 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1081
1083 not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
1084 "arithmetic overflow on " + kind + " " + expr.id_string(),
1085 "overflow",
1086 false, // fatal
1087 expr.find_source_location(),
1088 expr,
1089 guard);
1090 }
1091 }
1092 else if(expr.operands().size() == 2)
1093 {
1094 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1095
1096 const binary_exprt &bexpr = to_binary_expr(expr);
1098 not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
1099 "arithmetic overflow on " + kind + " " + expr.id_string(),
1100 "overflow",
1101 false, // fatal
1102 expr.find_source_location(),
1103 expr,
1104 guard);
1105 }
1106 else
1107 {
1108 PRECONDITION(expr.id() == ID_unary_minus);
1109
1110 std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
1111
1114 "arithmetic overflow on " + kind + " " + expr.id_string(),
1115 "overflow",
1116 false, // fatal
1117 expr.find_source_location(),
1118 expr,
1119 guard);
1120 }
1121}
1122
1124{
1126 return;
1127
1128 // First, check type.
1129 const typet &type = expr.type();
1130
1131 if(type.id() != ID_floatbv)
1132 return;
1133
1134 // add overflow subgoal
1135
1136 if(expr.id() == ID_typecast)
1137 {
1138 // Can overflow if casting from larger
1139 // to smaller type.
1140 const auto &op = to_typecast_expr(expr).op();
1141 if(op.type().id() == ID_floatbv)
1142 {
1143 // float-to-float
1145
1147 std::move(overflow_check),
1148 "arithmetic overflow on floating-point typecast",
1149 "overflow",
1150 false, // fatal
1151 expr.find_source_location(),
1152 expr,
1153 guard);
1154 }
1155 else
1156 {
1157 // non-float-to-float
1159 not_exprt(isinf_exprt(expr)),
1160 "arithmetic overflow on floating-point typecast",
1161 "overflow",
1162 false, // fatal
1163 expr.find_source_location(),
1164 expr,
1165 guard);
1166 }
1167
1168 return;
1169 }
1170 else if(expr.id() == ID_div)
1171 {
1172 // Can overflow if dividing by something small
1174 isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
1175
1177 std::move(overflow_check),
1178 "arithmetic overflow on floating-point division",
1179 "overflow",
1180 false, // fatal
1181 expr.find_source_location(),
1182 expr,
1183 guard);
1184
1185 return;
1186 }
1187 else if(expr.id() == ID_mod)
1188 {
1189 // Can't overflow
1190 return;
1191 }
1192 else if(expr.id() == ID_unary_minus)
1193 {
1194 // Can't overflow
1195 return;
1196 }
1197 else if(expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_minus)
1198 {
1199 if(expr.operands().size() == 2)
1200 {
1201 // Can overflow
1203 isinf_exprt(to_binary_expr(expr).op0()),
1204 isinf_exprt(to_binary_expr(expr).op1()),
1205 not_exprt(isinf_exprt(expr)));
1206
1207 std::string kind = expr.id() == ID_plus ? "addition"
1208 : expr.id() == ID_minus ? "subtraction"
1209 : expr.id() == ID_mult ? "multiplication"
1210 : "";
1211
1213 std::move(overflow_check),
1214 "arithmetic overflow on floating-point " + kind,
1215 "overflow",
1216 false, // fatal
1217 expr.find_source_location(),
1218 expr,
1219 guard);
1220
1221 return;
1222 }
1223 else if(expr.operands().size() >= 3)
1224 {
1225 DATA_INVARIANT(expr.id() != ID_minus, "minus expression must be binary");
1226
1227 // break up
1229 return;
1230 }
1231 }
1232}
1233
1234 void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
1235{
1236 if(!enable_nan_check)
1237 return;
1238
1239 // first, check type
1240 if(expr.type().id() != ID_floatbv)
1241 return;
1242
1243 if(
1244 expr.id() != ID_plus && expr.id() != ID_mult && expr.id() != ID_div &&
1245 expr.id() != ID_minus)
1246 return;
1247
1248 // add NaN subgoal
1249
1250 exprt isnan;
1251
1252 if(expr.id() == ID_div)
1253 {
1254 const auto &div_expr = to_div_expr(expr);
1255
1256 // there a two ways to get a new NaN on division:
1257 // 0/0 = NaN and x/inf = NaN
1258 // (note that x/0 = +-inf for x!=0 and x!=inf)
1261 div_expr.op0(), from_integer(0, div_expr.dividend().type())),
1263 div_expr.op1(), from_integer(0, div_expr.divisor().type())));
1264
1265 const isinf_exprt div_inf(div_expr.op1());
1266
1268 }
1269 else if(expr.id() == ID_mult)
1270 {
1271 if(expr.operands().size() >= 3)
1272 return nan_check(make_binary(expr), guard);
1273
1274 const auto &mult_expr = to_mult_expr(expr);
1275
1276 // Inf * 0 is NaN
1278 isinf_exprt(mult_expr.op0()),
1280 mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
1281
1284 mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
1285 isinf_exprt(mult_expr.op0()));
1286
1288 }
1289 else if(expr.id() == ID_plus)
1290 {
1291 if(expr.operands().size() >= 3)
1292 return nan_check(make_binary(expr), guard);
1293
1294 const auto &plus_expr = to_plus_expr(expr);
1295
1296 // -inf + +inf = NaN and +inf + -inf = NaN,
1297 // i.e., signs differ
1301
1302 isnan = or_exprt(
1303 and_exprt(
1306 and_exprt(
1309 }
1310 else if(expr.id() == ID_minus)
1311 {
1312 // +inf - +inf = NaN and -inf - -inf = NaN,
1313 // i.e., signs match
1314
1315 const auto &minus_expr = to_minus_expr(expr);
1316
1317 ieee_float_spect spec =
1321
1322 isnan = or_exprt(
1323 and_exprt(
1326 and_exprt(
1329 }
1330 else
1332
1335 "NaN on " + expr.id_string(),
1336 "NaN",
1337 false, // fatal
1338 expr.find_source_location(),
1339 expr,
1340 guard);
1341}
1342
1344 const binary_exprt &expr,
1345 const guardt &guard)
1346{
1348 return;
1349
1350 if(
1351 expr.op0().type().id() == ID_pointer &&
1352 expr.op1().type().id() == ID_pointer)
1353 {
1354 // add same-object subgoal
1355
1356 exprt same_object = ::same_object(expr.op0(), expr.op1());
1357
1360 "same object violation",
1361 "pointer",
1362 false, // fatal
1363 expr.find_source_location(),
1364 expr,
1365 guard);
1366
1367 for(const auto &pointer : expr.operands())
1368 {
1369 // just this particular byte must be within object bounds or one past the
1370 // end
1371 const auto size = from_integer(0, size_type());
1372 auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1373
1374 for(const auto &c : conditions)
1375 {
1377 c.assertion,
1378 "pointer relation: " + c.description,
1379 "pointer arithmetic",
1380 true, // fatal
1381 expr.find_source_location(),
1382 pointer,
1383 guard);
1384 }
1385 }
1386 }
1387}
1388
1390 const exprt &expr,
1391 const guardt &guard)
1392{
1394 return;
1395
1396 if(expr.id() != ID_plus && expr.id() != ID_minus)
1397 return;
1398
1400 expr.operands().size() == 2,
1401 "pointer arithmetic expected to have exactly 2 operands");
1402
1403 // multiplying the offset by the object size must not result in arithmetic
1404 // overflow
1405 const typet &object_type = to_pointer_type(expr.type()).base_type();
1406 if(object_type.id() != ID_empty)
1407 {
1408 auto size_of_expr_opt = size_of_expr(object_type, ns);
1409 CHECK_RETURN(size_of_expr_opt.has_value());
1411
1413 exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer
1414 ? binary_expr.rhs()
1415 : binary_expr.lhs();
1416 mult_exprt mul{
1419 mul.add_source_location() = offset_operand.source_location();
1420
1422 override_overflow.set_flag(
1423 enable_signed_overflow_check, true, "signed_overflow_check");
1424 override_overflow.set_flag(
1425 enable_unsigned_overflow_check, true, "unsigned_overflow_check");
1427 }
1428
1429 // the result must be within object bounds or one past the end
1430 const auto size = from_integer(0, size_type());
1431 auto conditions = get_pointer_dereferenceable_conditions(expr, size);
1432
1433 for(const auto &c : conditions)
1434 {
1436 c.assertion,
1437 "pointer arithmetic: " + c.description,
1438 "pointer arithmetic",
1439 true, // fatal
1440 expr.find_source_location(),
1441 expr,
1442 guard);
1443 }
1444}
1445
1447 const dereference_exprt &expr,
1448 const exprt &src_expr,
1449 const guardt &guard)
1450{
1452 return;
1453
1454 const exprt &pointer = expr.pointer();
1455
1456 exprt size;
1457
1458 if(expr.type().id() == ID_empty)
1459 {
1460 // a dereference *p (with p being a pointer to void) is valid if p points to
1461 // valid memory (of any size). the smallest possible size of the memory
1462 // segment p could be pointing to is 1, hence we use this size for the
1463 // address check
1464 size = from_integer(1, size_type());
1465 }
1466 else
1467 {
1468 auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1469 CHECK_RETURN(size_of_expr_opt.has_value());
1470 size = size_of_expr_opt.value();
1471 }
1472
1473 auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1474
1475 for(const auto &c : conditions)
1476 {
1478 c.assertion,
1479 "dereference failure: " + c.description,
1480 "pointer dereference",
1481 true, // fatal
1482 src_expr.find_source_location(),
1483 src_expr,
1484 guard);
1485 }
1486}
1487
1489 const exprt &expr,
1490 const guardt &guard)
1491{
1493 return;
1494
1495 if(expr.source_location().is_built_in())
1496 return;
1497
1498 const exprt pointer =
1499 (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
1500 ? to_r_or_w_ok_expr(expr).pointer()
1502 ? to_prophecy_r_or_w_ok_expr(expr).pointer()
1503 : to_unary_expr(expr).op();
1504
1505 CHECK_RETURN(pointer.type().id() == ID_pointer);
1506
1507 if(pointer.id() == ID_symbol)
1508 {
1509 const auto &symbol_expr = to_symbol_expr(pointer);
1510
1511 if(symbol_expr.identifier().starts_with(CPROVER_PREFIX))
1512 return;
1513 }
1514
1516 pointer, from_integer(0, size_type()));
1517 for(const auto &c : conditions)
1518 {
1520 or_exprt{null_object(pointer), c.assertion},
1521 c.description,
1522 "pointer primitives",
1523 false, // fatal
1524 expr.source_location(),
1525 expr,
1526 guard);
1527 }
1528}
1529
1531{
1532 // we don't need to include the __CPROVER_same_object primitive here as it
1533 // is replaced by lower level primitives in the special function handling
1534 // during typechecking (see c_typecheck_expr.cpp)
1535
1536 // pointer_object and pointer_offset are well-defined for an arbitrary
1537 // pointer-typed operand (and the operands themselves have been checked
1538 // separately for, e.g., invalid pointer dereferencing via check_rec):
1539 // pointer_object and pointer_offset just extract a subset of bits from the
1540 // pointer. If that pointer was unconstrained (non-deterministic), the result
1541 // will equally be non-deterministic.
1542 return can_cast_expr<object_size_exprt>(expr) || expr.id() == ID_r_ok ||
1543 expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
1545 expr.id() == ID_is_dynamic_object;
1546}
1547
1548goto_check_ct::conditionst
1550 const exprt &address,
1551 const exprt &size)
1552{
1553 auto conditions =
1555 if(auto maybe_null_condition = get_pointer_is_null_condition(address, size))
1556 {
1557 conditions.push_front(*maybe_null_condition);
1558 }
1559 return conditions;
1560}
1561
1562 std::string goto_check_ct::array_name(const exprt &expr)
1563{
1564 return ::array_name(ns, expr);
1565}
1566
1568{
1570 return;
1571
1572 if(expr.id() == ID_index)
1574 else if(
1575 (expr.id() == ID_count_leading_zeros &&
1576 !to_count_leading_zeros_expr(expr).zero_permitted()) ||
1577 (expr.id() == ID_count_trailing_zeros &&
1578 !to_count_trailing_zeros_expr(expr).zero_permitted()))
1579 {
1581 }
1582}
1583
1585 const index_exprt &expr,
1586 const guardt &guard)
1587{
1588 const typet &array_type = expr.array().type();
1589
1590 if(array_type.id() == ID_pointer)
1591 throw "index got pointer as array type";
1592 else if(array_type.id() != ID_array && array_type.id() != ID_vector)
1593 throw "bounds check expected array or vector type, got " +
1594 array_type.id_string();
1595
1596 std::string name = array_name(expr.array());
1597
1598 const exprt &index = expr.index();
1600 ode.build(expr, ns);
1601
1602 if(index.type().id() != ID_unsignedbv)
1603 {
1604 // we undo typecasts to signedbv
1605 if(
1606 index.id() == ID_typecast &&
1607 to_typecast_expr(index).op().type().id() == ID_unsignedbv)
1608 {
1609 // ok
1610 }
1611 else
1612 {
1613 const auto i = numeric_cast<mp_integer>(index);
1614
1615 if(!i.has_value() || *i < 0)
1616 {
1617 exprt effective_offset = ode.offset();
1618
1619 if(ode.root_object().id() == ID_dereference)
1620 {
1621 exprt p_offset =
1622 pointer_offset(to_dereference_expr(ode.root_object()).pointer());
1623
1625 p_offset,
1627 effective_offset, p_offset.type())};
1628 }
1629
1630 exprt zero = from_integer(0, effective_offset.type());
1631
1632 // the final offset must not be negative
1634 effective_offset, ID_ge, std::move(zero));
1635
1637 inequality,
1638 name + " lower bound",
1639 "array bounds",
1640 true, // fatal
1641 expr.find_source_location(),
1642 expr,
1643 guard);
1644 }
1645 }
1646 }
1647
1648 if(ode.root_object().id() == ID_dereference)
1649 {
1650 const exprt &pointer = to_dereference_expr(ode.root_object()).pointer();
1651
1653 ode.offset(),
1655 pointer_offset(pointer), ode.offset().type())};
1656
1659 ID_lt,
1661 object_size(pointer), effective_offset.type())};
1662
1665 pointer,
1666 plus_exprt{ode.offset(), from_integer(1, ode.offset().type())});
1667
1670
1672 precond,
1673 name + " dynamic object upper bound",
1674 "array bounds",
1675 false, // fatal
1676 expr.find_source_location(),
1677 expr,
1678 guard);
1679
1680 return;
1681 }
1682
1683 const exprt &size = array_type.id() == ID_array
1684 ? to_array_type(array_type).size()
1685 : to_vector_type(array_type).size();
1686
1687 if(size.is_nil() && !array_type.get_bool(ID_C_flexible_array_member))
1688 {
1689 // Linking didn't complete, we don't have a size.
1690 // Not clear what to do.
1691 }
1692 else if(size.id() == ID_infinity)
1693 {
1694 }
1695 else if(
1696 expr.array().id() == ID_member &&
1697 (size == 0 || array_type.get_bool(ID_C_flexible_array_member)))
1698 {
1699 // a variable sized struct member
1700 //
1701 // Excerpt from the C standard on flexible array members:
1702 // However, when a . (or ->) operator has a left operand that is (a pointer
1703 // to) a structure with a flexible array member and the right operand names
1704 // that member, it behaves as if that member were replaced with the longest
1705 // array (with the same element type) that would not make the structure
1706 // larger than the object being accessed; [...]
1707 const auto type_size_opt =
1708 pointer_offset_size(ode.root_object().type(), ns);
1709 CHECK_RETURN(type_size_opt.has_value());
1710
1712 ode.offset(),
1713 ID_lt,
1714 from_integer(type_size_opt.value(), ode.offset().type()));
1715
1717 inequality,
1718 name + " upper bound",
1719 "array bounds",
1720 true, // fatal
1721 expr.find_source_location(),
1722 expr,
1723 guard);
1724 }
1725 else
1726 {
1728 typecast_exprt::conditional_cast(index, size.type()), ID_lt, size};
1729
1731 inequality,
1732 name + " upper bound",
1733 "array bounds",
1734 true, // fatal
1735 expr.find_source_location(),
1736 expr,
1737 guard);
1738 }
1739}
1740
1742 const unary_exprt &expr,
1743 const guardt &guard)
1744{
1745 std::string name;
1746
1747 if(expr.id() == ID_count_leading_zeros)
1748 name = "leading";
1749 else if(expr.id() == ID_count_trailing_zeros)
1750 name = "trailing";
1751 else
1752 PRECONDITION(false);
1753
1755 notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
1756 "count " + name + " zeros is undefined for value zero",
1757 "bit count",
1758 false, // fatal
1759 expr.find_source_location(),
1760 expr,
1761 guard);
1762}
1763
1765 const exprt &asserted_expr,
1766 const std::string &comment,
1767 const std::string &property_class,
1768 bool is_fatal,
1769 const source_locationt &source_location,
1770 const exprt &src_expr,
1771 const guardt &guard)
1772{
1773 // first try simplifier on it
1774 exprt simplified_expr =
1776
1777 // throw away trivial properties?
1778 if(!retain_trivial && simplified_expr == true)
1779 return;
1780
1781 // add the guard
1782 exprt guarded_expr = guard(simplified_expr);
1783
1784 if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1785 {
1786 std::string source_expr_string;
1788
1789 source_locationt annotated_location = source_location;
1790 annotated_location.set_comment(comment + " in " + source_expr_string);
1791 annotated_location.set_property_class(property_class);
1792
1794
1796 {
1798 std::move(guarded_expr), annotated_location));
1799 }
1800 else
1801 {
1802 if(is_fatal)
1803 annotated_location.property_fatal(true);
1804
1806 std::move(guarded_expr), annotated_location));
1807 }
1808 }
1809}
1810
1812{
1813 // we don't look into quantifiers
1814 if(expr.id() == ID_exists || expr.id() == ID_forall)
1815 return;
1816
1817 if(expr.id() == ID_dereference)
1818 {
1819 check_rec(to_dereference_expr(expr).pointer(), guard, false);
1820 }
1821 else if(expr.id() == ID_index)
1822 {
1823 const index_exprt &index_expr = to_index_expr(expr);
1825 check_rec(index_expr.index(), guard, false);
1826 }
1827 else
1828 {
1829 for(const auto &operand : expr.operands())
1831 }
1832}
1833
1835{
1837 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
1838 INVARIANT(
1839 expr.is_boolean(),
1840 "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
1841
1842 exprt::operandst constraints;
1843
1844 for(const auto &op : expr.operands())
1845 {
1846 INVARIANT(
1847 op.is_boolean(),
1848 "'" + expr.id_string() + "' takes Boolean operands only, but got " +
1849 op.pretty());
1850
1851 auto new_guard = [&guard, &constraints](exprt expr) {
1852 return guard(implication(conjunction(constraints), expr));
1853 };
1854
1855 check_rec(op, new_guard, false);
1856
1857 constraints.push_back(expr.id() == ID_or ? boolean_negate(op) : op);
1858 }
1859}
1860
1862{
1863 INVARIANT(
1864 if_expr.cond().is_boolean(),
1865 "first argument of if must be boolean, but got " + if_expr.cond().pretty());
1866
1867 check_rec(if_expr.cond(), guard, false);
1868
1869 {
1870 auto new_guard = [&guard, &if_expr](exprt expr) {
1871 return guard(implication(if_expr.cond(), std::move(expr)));
1872 };
1873 check_rec(if_expr.true_case(), new_guard, false);
1874 }
1875
1876 {
1877 auto new_guard = [&guard, &if_expr](exprt expr) {
1878 return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
1879 };
1880 check_rec(if_expr.false_case(), new_guard, false);
1881 }
1882}
1883
1885 const member_exprt &member,
1886 const guardt &guard)
1887{
1889
1890 check_rec(deref.pointer(), guard, false);
1891
1892 // avoid building the following expressions when pointer_validity_check
1893 // would return immediately anyway
1895 return true;
1896
1897 // we rewrite s->member into *(s+member_offset)
1898 // to avoid requiring memory safety of the entire struct
1899 auto member_offset_opt = member_offset_expr(member, ns);
1900
1901 if(member_offset_opt.has_value())
1902 {
1904 new_pointer_type.base_type() = member.type();
1905
1907 deref.pointer(), pointer_type(char_type()));
1908
1910 plus_exprt{
1915
1917 new_deref.add_source_location() = deref.source_location();
1919
1920 return true;
1921 }
1922 return false;
1923}
1924
1926 const div_exprt &div_expr,
1927 const guardt &guard)
1928{
1929 if(
1930 div_expr.type().id() == ID_signedbv ||
1931 div_expr.type().id() == ID_unsignedbv || div_expr.type().id() == ID_c_bool)
1932 {
1933 // Division by zero is undefined behavior for all integer types.
1935 }
1936 else if(div_expr.type().id() == ID_floatbv)
1937 {
1938 // Division by zero on floating-point numbers may be undefined behavior.
1939 // Annex F of the ISO C21 suggests that implementations that
1940 // define __STDC_IEC_559__ follow IEEE 754 semantics,
1941 // which defines the outcome of division by zero.
1943 }
1944
1945 if(div_expr.type().id() == ID_signedbv)
1947 else if(div_expr.type().id() == ID_floatbv)
1948 {
1951 }
1952}
1953
1955 const exprt &expr,
1956 const guardt &guard)
1957{
1958 if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1959 {
1961
1962 if(
1963 expr.operands().size() == 2 && expr.id() == ID_minus &&
1964 expr.operands()[0].type().id() == ID_pointer &&
1965 expr.operands()[1].type().id() == ID_pointer)
1966 {
1968 }
1969 }
1970 else if(expr.type().id() == ID_floatbv)
1971 {
1972 nan_check(expr, guard);
1974 }
1975 else if(expr.type().id() == ID_pointer)
1976 {
1978 }
1979}
1980
1982 const exprt &expr,
1983 const guardt &guard,
1984 bool is_assigned)
1985{
1986 if(expr.id() == ID_exists || expr.id() == ID_forall)
1987 {
1988 // the scoped variables may be used in the assertion
1989 const auto &quantifier_expr = to_quantifier_expr(expr);
1990
1991 auto new_guard = [&guard, &quantifier_expr](exprt expr) {
1992 return guard(forall_exprt(quantifier_expr.symbol(), expr));
1993 };
1994
1995 check_rec(quantifier_expr.where(), new_guard, false);
1996 return;
1997 }
1998 else if(expr.id() == ID_address_of)
1999 {
2001 return;
2002 }
2003 else if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
2004 {
2006 return;
2007 }
2008 else if(expr.id() == ID_if)
2009 {
2011 return;
2012 }
2013 else if(
2014 expr.id() == ID_member &&
2015 to_member_expr(expr).struct_op().id() == ID_dereference)
2016 {
2018 return;
2019 }
2020
2021 for(const auto &op : expr.operands())
2022 check_rec(op, guard, false);
2023
2024 if(expr.type().id() == ID_c_enum_tag)
2026
2027 if(expr.id() == ID_index)
2028 {
2029 bounds_check(expr, guard);
2030 }
2031 else if(expr.id() == ID_div)
2032 {
2034 }
2035 else if(expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr)
2036 {
2038
2039 if(expr.id() == ID_shl && expr.type().id() == ID_signedbv)
2041 }
2042 else if(expr.id() == ID_mod)
2043 {
2046 }
2047 else if(
2048 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
2049 expr.id() == ID_unary_minus)
2050 {
2052 }
2053 else if(expr.id() == ID_typecast)
2054 conversion_check(expr, guard);
2055 else if(
2056 expr.id() == ID_le || expr.id() == ID_lt || expr.id() == ID_ge ||
2057 expr.id() == ID_gt)
2059 else if(expr.id() == ID_dereference)
2060 {
2062 }
2064 {
2066 }
2067 else if(
2068 expr.id() == ID_count_leading_zeros || expr.id() == ID_count_trailing_zeros)
2069 {
2070 bounds_check(expr, guard);
2071 }
2072}
2073
2075{
2077}
2078
2080{
2081 const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
2082 const symbol_exprt leak_expr = leak.symbol_expr();
2083
2084 // add self-assignment to get helpful counterexample output
2086
2087 source_locationt source_location;
2088 source_location.set_function(function_id);
2089
2091
2093 eq,
2094 "dynamically allocated memory never freed",
2095 "memory-leak",
2096 false, // fatal
2097 source_location,
2098 eq,
2099 identity);
2100}
2101
2103 const irep_idt &function_identifier,
2104 goto_functiont &goto_function)
2105{
2106 const auto &function_symbol = ns.lookup(function_identifier);
2107 mode = function_symbol.mode;
2108
2109 if(mode != ID_C && mode != ID_cpp)
2110 return;
2111
2112 assertions.clear();
2113
2114 bool did_something = false;
2115
2117 std::make_unique<local_bitvector_analysist>(goto_function, ns);
2118
2119 goto_programt &goto_program = goto_function.body;
2120
2121 Forall_goto_program_instructions(it, goto_program)
2122 {
2123 current_target = it;
2125
2127 const auto &pragmas = i.source_location().get_pragmas();
2128 for(const auto &d : pragmas)
2129 {
2130 // match named-check related pragmas
2131 auto matched = match_named_check(d.first);
2132 if(matched.has_value())
2133 {
2134 auto named_check = matched.value();
2135 auto name = named_check.first;
2136 auto status = named_check.second;
2137 bool *flag = name_to_flag.find(name)->second;
2138 switch(status)
2139 {
2141 resetter.set_flag(*flag, true, name);
2142 break;
2144 resetter.set_flag(*flag, false, name);
2145 break;
2147 resetter.disable_flag(*flag, name);
2148 break;
2149 }
2150 }
2151 }
2152
2153 // add checked pragmas for all active checks
2155
2156 new_code.clear();
2157
2158 // we clear all recorded assertions if
2159 // 1) we want to generate all assertions or
2160 // 2) the instruction is a branch target
2161 if(retain_trivial || i.is_target())
2162 assertions.clear();
2163
2164 if(i.has_condition())
2165 {
2166 check(i.condition(), false);
2167 }
2168
2169 // magic ERROR label?
2170 for(const auto &label : error_labels)
2171 {
2172 if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end())
2173 {
2175 annotated_location.set_property_class("error label");
2176 annotated_location.set_comment("error label " + label);
2177 annotated_location.set("user-provided", true);
2178
2180 {
2181 new_code.add(
2183 }
2184 else
2185 {
2186 new_code.add(
2188 }
2189 }
2190 }
2191
2192 if(i.is_other())
2193 {
2194 const auto &code = i.get_other();
2195 const irep_idt &statement = code.get_statement();
2196
2197 if(statement == ID_expression)
2198 {
2199 check(code, false);
2200 }
2201 else if(statement == ID_printf)
2202 {
2203 for(const auto &op : code.operands())
2204 check(op, false);
2205 }
2206 }
2207 else if(i.is_assign())
2208 {
2209 const exprt &assign_lhs = i.assign_lhs();
2210 const exprt &assign_rhs = i.assign_rhs();
2211
2212 check(assign_lhs, true);
2213 check(assign_rhs, false);
2214
2215 // the LHS might invalidate any assertion
2216 invalidate(assign_lhs);
2217 }
2218 else if(i.is_function_call())
2219 {
2220 check(i.call_lhs(), true);
2221 check(i.call_function(), false);
2222
2223 for(const auto &arg : i.call_arguments())
2224 check(arg, false);
2225
2227
2228 // the call might invalidate any assertion
2229 assertions.clear();
2230 }
2231 else if(i.is_set_return_value())
2232 {
2233 check(i.return_value(), false);
2234 // the return value invalidate any assertion
2236 }
2237 else if(i.is_throw())
2238 {
2239 // this has no successor
2240 assertions.clear();
2241 }
2242 else if(i.is_assume())
2243 {
2244 // These are further 'exit points' of the program
2246 if(
2248 (function_identifier == "abort" || function_identifier == "exit" ||
2249 function_identifier == "_Exit" ||
2250 (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
2251 {
2252 memory_leak_check(function_identifier);
2253 }
2254 }
2255 else if(i.is_dead())
2256 {
2258 {
2259 const symbol_exprt &variable = i.dead_symbol();
2260
2261 // is it dirty?
2262 if(local_bitvector_analysis->dirty(variable))
2263 {
2264 // need to mark the dead variable as dead
2265 exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2267 address_of_exprt(variable), lhs.type());
2268 if_exprt rhs(
2270 std::move(address_of_expr),
2271 lhs);
2273 code_assignt{std::move(lhs), std::move(rhs), i.source_location()},
2274 i.source_location()));
2275 }
2276 }
2277 }
2278 else if(i.is_end_function())
2279 {
2280 if(
2281 function_identifier == goto_functionst::entry_point() &&
2283 {
2284 memory_leak_check(function_identifier);
2285 }
2286 }
2287
2288 for(auto &instruction : new_code.instructions)
2289 {
2290 if(instruction.source_location().is_nil())
2291 {
2292 instruction.source_location_nonconst().id(irep_idt());
2293
2294 if(!it->source_location().get_file().empty())
2295 instruction.source_location_nonconst().set_file(
2296 it->source_location().get_file());
2297
2298 if(!it->source_location().get_line().empty())
2299 instruction.source_location_nonconst().set_line(
2300 it->source_location().get_line());
2301
2302 if(!it->source_location().get_function().empty())
2303 instruction.source_location_nonconst().set_function(
2304 it->source_location().get_function());
2305
2306 if(!it->source_location().get_column().empty())
2307 {
2308 instruction.source_location_nonconst().set_column(
2309 it->source_location().get_column());
2310 }
2311 }
2312 }
2313
2314 // insert new instructions -- make sure targets are not moved
2316
2317 while(!new_code.instructions.empty())
2318 {
2319 goto_program.insert_before_swap(it, new_code.instructions.front());
2320 new_code.instructions.pop_front();
2321 it++;
2322 }
2323 }
2324
2325 if(did_something)
2326 remove_skip(goto_program);
2327}
2328
2331{
2332 if(i.call_function().id() != ID_symbol)
2333 return;
2334
2335 const irep_idt &identifier = to_symbol_expr(i.call_function()).identifier();
2336
2337 if(
2338 identifier == CPROVER_PREFIX "get_field" || identifier == CPROVER_PREFIX
2339 "set_field")
2340 {
2341 const exprt &expr = i.call_arguments()[0];
2342 PRECONDITION(expr.type().id() == ID_pointer);
2343 check(dereference_exprt(expr), false);
2344 }
2345}
2346
2347goto_check_ct::conditionst
2349 const exprt &address,
2350 const exprt &size)
2351{
2353 PRECONDITION(address.type().id() == ID_pointer);
2356
2357 conditionst conditions;
2358
2361
2362 const bool unknown = flags.is_unknown() || flags.is_uninitialized();
2363
2364 if(unknown)
2365 {
2366 conditions.push_back(conditiont{
2367 not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
2368 }
2369
2370 if(unknown || flags.is_dynamic_heap())
2371 {
2372 conditions.push_back(conditiont(
2373 or_exprt(
2375 not_exprt(deallocated(address, ns))),
2376 "deallocated dynamic object"));
2377 }
2378
2379 if(unknown || flags.is_dynamic_local())
2380 {
2381 conditions.push_back(conditiont(
2382 or_exprt(
2384 not_exprt(dead_object(address, ns))),
2385 "dead object"));
2386 }
2387
2388 if(flags.is_dynamic_heap())
2389 {
2391 object_lower_bound(address, nil_exprt()),
2392 object_upper_bound(address, size));
2393
2394 conditions.push_back(conditiont(
2395 or_exprt(
2398 "pointer outside dynamic object bounds"));
2399 }
2400
2401 if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
2402 {
2404 object_lower_bound(address, nil_exprt()),
2405 object_upper_bound(address, size));
2406
2407 conditions.push_back(conditiont(
2408 or_exprt(
2411 "pointer outside object bounds"));
2412 }
2413
2414 if(unknown || flags.is_integer_address())
2415 {
2416 conditions.push_back(conditiont(
2419 "invalid integer address"));
2420 }
2421
2422 return conditions;
2423}
2424
2425std::optional<goto_check_ct::conditiont>
2427 const exprt &address,
2428 const exprt &size)
2429{
2431 PRECONDITION(address.type().id() == ID_pointer);
2434
2435 if(flags.is_unknown() || flags.is_uninitialized() || flags.is_null())
2436 {
2437 return {conditiont{
2438 or_exprt{
2440 not_exprt(null_object(address))},
2441 "pointer NULL"}};
2442 }
2443
2444 return {};
2445}
2446
2448 const exprt &pointer,
2449 const exprt &size)
2450{
2452 for(const auto &a : allocations)
2453 {
2454 typecast_exprt int_ptr(pointer, a.first.type());
2455
2457
2458 plus_exprt upper_bound{
2460
2462 std::move(upper_bound), ID_le, plus_exprt{a.first, a.second}};
2463
2464 alloc_disjuncts.push_back(
2465 and_exprt{std::move(lb_check), std::move(ub_check)});
2466 }
2468}
2469
2471 const irep_idt &function_identifier,
2472 goto_functionst::goto_functiont &goto_function,
2473 const namespacet &ns,
2474 const optionst &options,
2475 message_handlert &message_handler)
2476{
2477 goto_check_ct goto_check(ns, options, message_handler);
2478 goto_check.goto_check(function_identifier, goto_function);
2479}
2480
2482 const namespacet &ns,
2483 const optionst &options,
2484 goto_functionst &goto_functions,
2485 message_handlert &message_handler)
2486{
2487 goto_check_ct goto_check(ns, options, message_handler);
2488
2489 goto_check.collect_allocations(goto_functions);
2490
2491 for(auto &gf_entry : goto_functions.function_map)
2492 {
2493 goto_check.goto_check(gf_entry.first, gf_entry.second);
2494 }
2495}
2496
2498 const optionst &options,
2499 goto_modelt &goto_model,
2500 message_handlert &message_handler)
2501{
2502 const namespacet ns(goto_model.symbol_table);
2503 goto_check_c(ns, options, goto_model.goto_functions, message_handler);
2504}
2505
2507 source_locationt &source_location) const
2508{
2509 for(const auto &entry : name_to_flag)
2510 if(*(entry.second))
2511 source_location.add_pragma("checked:" + id2string(entry.first));
2512}
2513
2515 source_locationt &source_location) const
2516{
2517 for(const auto &entry : name_to_flag)
2518 source_location.add_pragma("checked:" + id2string(entry.first));
2519}
2520
2521goto_check_ct::named_check_statust
2523{
2524 auto s = id2string(named_check);
2525 auto col = s.find(":");
2526
2527 if(col == std::string::npos)
2528 return {}; // separator not found
2529
2530 auto name = s.substr(col + 1);
2531
2532 if(name_to_flag.find(name) == name_to_flag.end())
2533 return {}; // name unknown
2534
2535 check_statust status;
2536 if(!s.compare(0, 6, "enable"))
2537 status = check_statust::ENABLE;
2538 else if(!s.compare(0, 7, "disable"))
2539 status = check_statust::DISABLE;
2540 else if(!s.compare(0, 7, "checked"))
2541 status = check_statust::CHECKED;
2542 else
2543 return {}; // prefix unknow
2544
2545 // success
2546 return std::pair<irep_idt, check_statust>{name, status};
2547}
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.
Definition pointer_expr.h:540
virtual void clear()
Reset the abstract state.
Definition ai.h:269
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
A base class for binary expressions.
Definition std_expr.h:649
exprt & op0()
Definition expr.h:134
exprt & op1()
Definition expr.h:137
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:737
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:784
The Boolean type.
Definition std_types.h:35
A goto_instruction_codet representing an assignment in the program.
exprt::operandst argumentst
struct configt::cppt cpp
struct configt::ansi_ct ansi_c
Operator to dereference a pointer.
Definition pointer_expr.h:834
exprt & pointer()
Definition pointer_expr.h:847
Division.
Definition std_expr.h:1152
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:1339
Base class for all expressions.
Definition expr.h:57
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:68
std::vector< exprt > operandst
Definition expr.h:59
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:229
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
const source_locationt & source_location() const
Definition expr.h:236
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition std_expr.h:3135
Allows to:
~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.
bool enable_pointer_check
bool enable_simplify
void memory_leak_check(const irep_idt &function_id)
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
irep_idt mode
bool retain_trivial
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
@ ENABLE
@ DISABLE
@ CHECKED
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 &)
bool enable_nan_check
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...
bool enable_bounds_check
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)
messaget log
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...
Definition goto_function.h:24
goto_programt body
Definition goto_function.h:26
Definition goto_model.h:27
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.
Definition goto_program.h:180
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition goto_program.h:243
bool is_end_function() const
Definition goto_program.h:507
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition goto_program.h:285
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
Definition goto_program.h:313
labelst labels
Definition goto_program.h:446
bool is_target() const
Is this node a branch target?
Definition goto_program.h:452
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition goto_program.h:257
bool is_set_return_value() const
Definition goto_program.h:491
bool is_dead() const
Definition goto_program.h:500
bool has_condition() const
Does this instruction have a condition?
Definition goto_program.h:359
bool is_assume() const
Definition goto_program.h:501
bool is_other() const
Definition goto_program.h:498
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition goto_program.h:299
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition goto_program.h:199
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition goto_program.h:213
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition goto_program.h:271
bool is_throw() const
Definition goto_program.h:494
bool is_function_call() const
Definition goto_program.h:493
const exprt & condition() const
Get the condition of gotos, assume, assert.
Definition goto_program.h:365
bool is_assign() const
Definition goto_program.h:492
source_locationt & source_location_nonconst()
Definition goto_program.h:337
const source_locationt & source_location() const
Definition goto_program.h:332
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:72
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition goto_program.h:944
instructionst instructions
The list of instructions in the goto program.
Definition goto_program.h:621
void clear()
Clear the goto program.
Definition goto_program.h:819
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition goto_program.h:642
instructionst::const_iterator const_targett
Definition goto_program.h:614
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.
Definition goto_program.h:738
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition goto_program.h:932
Definition guard_expr.h:24
IEEE-floating-point equality.
Definition floatbv_expr.h:328
Definition ieee_float.h:22
static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:209
constant_exprt to_expr() const
Definition ieee_float.cpp:579
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:369
void from_integer(const mp_integer &i)
Definition ieee_float.cpp:813
@ ROUND_TO_EVEN
Definition ieee_float.h:379
The trinary if-then-else operator.
Definition std_expr.h:2426
Boolean implication.
Definition std_expr.h:2154
Array index operator.
Definition std_expr.h:1431
exprt & index()
Definition std_expr.h:1471
exprt & array()
Definition std_expr.h:1461
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.
Definition floatbv_expr.h:196
Extract member of struct or union.
Definition std_expr.h:2866
const exprt & struct_op() const
Definition std_expr.h:2904
Definition message.h:27
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:1216
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition std_expr.h:1236
Binary multiplication Associativity is not specified.
Definition std_expr.h:1104
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:908
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:3144
Boolean negation.
Definition std_expr.h:2388
Disequality.
Definition std_expr.h:1393
The null pointer constant.
Definition pointer_expr.h:909
Split an expression into a base object and a (byte) offset.
Definition pointer_expr.h:181
std::list< std::string > value_listt
Definition options.h:25
Boolean OR All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2193
The plus expression Associativity is not specified.
Definition std_expr.h:1006
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition pointer_expr.h:24
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
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:132
Symbol table entry.
Definition symbol.h:28
Semantic type conversion.
Definition std_expr.h:1995
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:364
const exprt & op() const
Definition std_expr.h:394
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
Definition expr_util.cpp:110
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition expr_util.cpp:98
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)
Definition pointer_expr.h:949
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.
Definition pointer_expr.h:577
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition pointer_expr.h:93
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.
Definition pointer_expr.h:890
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)
Definition race_check.cpp:108
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition remove_skip.cpp:87
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 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:240
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:252
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:828
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1494
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1260
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1134
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2024
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1196
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:721
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1045
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:424
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:991
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2501
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2953
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1085
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:221
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2174
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:502
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1006
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
@ C11
@ C99
exprt assertion
conditiont(const exprt &_assertion, const std::string &_description)
std::string description
bool is_static_lifetime() const
bool is_dynamic_local() const
bool is_dynamic_heap() const
bool is_uninitialized() const
bool is_integer_address() const
bool is_null() const
bool is_unknown() const
#define size_type
Definition unistd.c:186
dstringt irep_idt

AltStyle によって変換されたページ (->オリジナル) /