cprover
goto_check.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_check.h"
13 
14 #include <algorithm>
15 
16 #include <util/arith_tools.h>
17 #include <util/array_name.h>
18 #include <util/bitvector_expr.h>
19 #include <util/c_types.h>
20 #include <util/config.h>
21 #include <util/cprover_prefix.h>
22 #include <util/expr_util.h>
23 #include <util/find_symbols.h>
24 #include <util/floatbv_expr.h>
25 #include <util/ieee_float.h>
26 #include <util/invariant.h>
27 #include <util/make_unique.h>
28 #include <util/options.h>
29 #include <util/pointer_expr.h>
32 #include <util/prefix.h>
33 #include <util/simplify_expr.h>
34 #include <util/std_expr.h>
35 #include <util/std_types.h>
36 
37 #include <langapi/language.h>
38 #include <langapi/mode.h>
39 
41 
42 #include "guard.h"
44 
46 {
47 public:
49  const namespacet &_ns,
50  const optionst &_options):
51  ns(_ns),
53  {
54  no_enum_check = false;
55  enable_bounds_check=_options.get_bool_option("bounds-check");
56  enable_pointer_check=_options.get_bool_option("pointer-check");
57  enable_memory_leak_check=_options.get_bool_option("memory-leak-check");
58  enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
59  enable_enum_range_check = _options.get_bool_option("enum-range-check");
61  _options.get_bool_option("signed-overflow-check");
63  _options.get_bool_option("unsigned-overflow-check");
65  _options.get_bool_option("pointer-overflow-check");
66  enable_conversion_check=_options.get_bool_option("conversion-check");
68  _options.get_bool_option("undefined-shift-check");
70  _options.get_bool_option("float-overflow-check");
71  enable_simplify=_options.get_bool_option("simplify");
72  enable_nan_check=_options.get_bool_option("nan-check");
73  retain_trivial = _options.get_bool_option("retain-trivial-checks");
74  enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
75  enable_assertions=_options.get_bool_option("assertions");
76  enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
77  enable_assumptions=_options.get_bool_option("assumptions");
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 
96 protected:
97  const namespacet &ns;
98  std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
102 
108  void check_rec_address(const exprt &expr, guardt &guard);
109 
117  void check_rec_logical_op(const exprt &expr, guardt &guard);
118 
125  void check_rec_if(const if_exprt &if_expr, guardt &guard);
126 
137  bool check_rec_member(const member_exprt &member, guardt &guard);
138 
143  void check_rec_div(const div_exprt &div_expr, guardt &guard);
144 
149  void check_rec_arithmetic_op(const exprt &expr, guardt &guard);
150 
156  void check_rec(const exprt &expr, guardt &guard);
157 
160  void check(const exprt &expr);
161 
162  struct conditiont
163  {
164  conditiont(const exprt &_assertion, const std::string &_description)
165  : assertion(_assertion), description(_description)
166  {
167  }
168 
170  std::string description;
171  };
172 
173  using conditionst = std::list<conditiont>;
174 
175  void bounds_check(const index_exprt &, const guardt &);
176  void div_by_zero_check(const div_exprt &, const guardt &);
177  void mod_by_zero_check(const mod_exprt &, const guardt &);
178  void mod_overflow_check(const mod_exprt &, const guardt &);
179  void enum_range_check(const exprt &, const guardt &);
180  void undefined_shift_check(const shift_exprt &, const guardt &);
181  void pointer_rel_check(const binary_exprt &, const guardt &);
182  void pointer_overflow_check(const exprt &, const guardt &);
183 
190  const dereference_exprt &expr,
191  const exprt &src_expr,
192  const guardt &guard);
193 
199  void pointer_primitive_check(const exprt &expr, const guardt &guard);
200 
206  bool is_pointer_primitive(const exprt &expr);
207 
209  get_pointer_is_null_condition(const exprt &address, const exprt &size);
211  const exprt &address,
212  const exprt &size);
214  const exprt &pointer,
215  const exprt &size);
216 
218  const exprt &address,
219  const exprt &size);
220  void integer_overflow_check(const exprt &, const guardt &);
221  void conversion_check(const exprt &, const guardt &);
222  void float_overflow_check(const exprt &, const guardt &);
223  void nan_check(const exprt &, const guardt &);
225 
226  std::string array_name(const exprt &);
227 
237  const exprt &asserted_expr,
238  const std::string &comment,
239  const std::string &property_class,
240  const source_locationt &source_location,
241  const exprt &src_expr,
242  const guardt &guard);
243 
245  typedef std::set<std::pair<exprt, exprt>> assertionst;
247 
252  void invalidate(const exprt &lhs);
253 
273 
276 
277  // the first element of the pair is the base address,
278  // and the second is the size of the region
279  typedef std::pair<exprt, exprt> allocationt;
280  typedef std::list<allocationt> allocationst;
282 
284 };
285 
287  const goto_functionst &goto_functions)
288 {
289  if(
292  {
293  return;
294  }
295 
296  for(const auto &gf_entry : goto_functions.function_map)
297  {
298  for(const auto &instruction : gf_entry.second.body.instructions)
299  {
300  if(!instruction.is_function_call())
301  continue;
302 
303  const code_function_callt &call=
304  to_code_function_call(instruction.code);
305  if(call.function().id()!=ID_symbol ||
307  CPROVER_PREFIX "allocated_memory")
308  continue;
309 
310  const code_function_callt::argumentst &args= call.arguments();
311  if(args.size()!=2 ||
312  args[0].type().id()!=ID_unsignedbv ||
313  args[1].type().id()!=ID_unsignedbv)
314  throw "expected two unsigned arguments to "
315  CPROVER_PREFIX "allocated_memory";
316 
317  assert(args[0].type()==args[1].type());
318  allocations.push_back({args[0], args[1]});
319  }
320  }
321 }
322 
324 {
325  if(lhs.id()==ID_index)
326  invalidate(to_index_expr(lhs).array());
327  else if(lhs.id()==ID_member)
328  invalidate(to_member_expr(lhs).struct_op());
329  else if(lhs.id()==ID_symbol)
330  {
331  // clear all assertions about 'symbol'
332  find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
333 
334  for(auto it = assertions.begin(); it != assertions.end();)
335  {
336  if(
337  has_symbol(it->second, find_symbols_set) ||
338  has_subexpr(it->second, ID_dereference))
339  {
340  it = assertions.erase(it);
341  }
342  else
343  ++it;
344  }
345  }
346  else
347  {
348  // give up, clear all
349  assertions.clear();
350  }
351 }
352 
354  const div_exprt &expr,
355  const guardt &guard)
356 {
358  return;
359 
360  // add divison by zero subgoal
361 
362  exprt zero=from_integer(0, expr.op1().type());
363  const notequal_exprt inequality(expr.op1(), std::move(zero));
364 
366  inequality,
367  "division by zero",
368  "division-by-zero",
369  expr.find_source_location(),
370  expr,
371  guard);
372 }
373 
374 void goto_checkt::enum_range_check(const exprt &expr, const guardt &guard)
375 {
377  return;
378 
379  const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type());
380  symbolt enum_type = ns.lookup(c_enum_tag_type.get_identifier());
381  const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type);
382 
383  const c_enum_typet::memberst enum_values = c_enum_type.members();
384 
385  std::vector<exprt> disjuncts;
386  for(const auto &enum_value : enum_values)
387  {
388  const constant_exprt val{enum_value.get_value(), c_enum_tag_type};
389  disjuncts.push_back(equal_exprt(expr, val));
390  }
391 
392  const exprt check = disjunction(disjuncts);
393 
395  check,
396  "enum range check",
397  "enum-range-check",
398  expr.find_source_location(),
399  expr,
400  guard);
401 }
402 
404  const shift_exprt &expr,
405  const guardt &guard)
406 {
408  return;
409 
410  // Undefined for all types and shifts if distance exceeds width,
411  // and also undefined for negative distances.
412 
413  const typet &distance_type = expr.distance().type();
414 
415  if(distance_type.id()==ID_signedbv)
416  {
417  binary_relation_exprt inequality(
418  expr.distance(), ID_ge, from_integer(0, distance_type));
419 
421  inequality,
422  "shift distance is negative",
423  "undefined-shift",
424  expr.find_source_location(),
425  expr,
426  guard);
427  }
428 
429  const typet &op_type = expr.op().type();
430 
431  if(op_type.id()==ID_unsignedbv || op_type.id()==ID_signedbv)
432  {
433  exprt width_expr=
434  from_integer(to_bitvector_type(op_type).get_width(), distance_type);
435 
437  binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
438  "shift distance too large",
439  "undefined-shift",
440  expr.find_source_location(),
441  expr,
442  guard);
443 
444  if(op_type.id()==ID_signedbv && expr.id()==ID_shl)
445  {
446  binary_relation_exprt inequality(
447  expr.op(), ID_ge, from_integer(0, op_type));
448 
450  inequality,
451  "shift operand is negative",
452  "undefined-shift",
453  expr.find_source_location(),
454  expr,
455  guard);
456  }
457  }
458  else
459  {
461  false_exprt(),
462  "shift of non-integer type",
463  "undefined-shift",
464  expr.find_source_location(),
465  expr,
466  guard);
467  }
468 }
469 
471  const mod_exprt &expr,
472  const guardt &guard)
473 {
474  if(!enable_div_by_zero_check || mode == ID_java)
475  return;
476 
477  // add divison by zero subgoal
478 
479  exprt zero=from_integer(0, expr.op1().type());
480  const notequal_exprt inequality(expr.op1(), std::move(zero));
481 
483  inequality,
484  "division by zero",
485  "division-by-zero",
486  expr.find_source_location(),
487  expr,
488  guard);
489 }
490 
492 void goto_checkt::mod_overflow_check(const mod_exprt &expr, const guardt &guard)
493 {
495  return;
496 
497  const auto &type = expr.type();
498 
499  if(type.id() == ID_signedbv)
500  {
501  // INT_MIN % -1 is, in principle, defined to be zero in
502  // ANSI C, C99, C++98, and C++11. Most compilers, however,
503  // fail to produce 0, and in some cases generate an exception.
504  // C11 explicitly makes this case undefined.
505 
506  notequal_exprt int_min_neq(
507  expr.op0(), to_signedbv_type(type).smallest_expr());
508 
509  notequal_exprt minus_one_neq(
510  expr.op1(), from_integer(-1, expr.op1().type()));
511 
513  or_exprt(int_min_neq, minus_one_neq),
514  "result of signed mod is not representable",
515  "overflow",
516  expr.find_source_location(),
517  expr,
518  guard);
519  }
520 }
521 
523  const exprt &expr,
524  const guardt &guard)
525 {
527  return;
528 
529  // First, check type.
530  const typet &type = expr.type();
531 
532  if(type.id()!=ID_signedbv &&
533  type.id()!=ID_unsignedbv)
534  return;
535 
536  if(expr.id()==ID_typecast)
537  {
538  const auto &op = to_typecast_expr(expr).op();
539 
540  // conversion to signed int may overflow
541  const typet &old_type = op.type();
542 
543  if(type.id()==ID_signedbv)
544  {
545  std::size_t new_width=to_signedbv_type(type).get_width();
546 
547  if(old_type.id()==ID_signedbv) // signed -> signed
548  {
549  std::size_t old_width=to_signedbv_type(old_type).get_width();
550  if(new_width>=old_width)
551  return; // always ok
552 
553  const binary_relation_exprt no_overflow_upper(
554  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
555 
556  const binary_relation_exprt no_overflow_lower(
557  op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
558 
560  and_exprt(no_overflow_lower, no_overflow_upper),
561  "arithmetic overflow on signed type conversion",
562  "overflow",
563  expr.find_source_location(),
564  expr,
565  guard);
566  }
567  else if(old_type.id()==ID_unsignedbv) // unsigned -> signed
568  {
569  std::size_t old_width=to_unsignedbv_type(old_type).get_width();
570  if(new_width>=old_width+1)
571  return; // always ok
572 
573  const binary_relation_exprt no_overflow_upper(
574  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
575 
577  no_overflow_upper,
578  "arithmetic overflow on unsigned to signed type conversion",
579  "overflow",
580  expr.find_source_location(),
581  expr,
582  guard);
583  }
584  else if(old_type.id()==ID_floatbv) // float -> signed
585  {
586  // Note that the fractional part is truncated!
587  ieee_floatt upper(to_floatbv_type(old_type));
588  upper.from_integer(power(2, new_width-1));
589  const binary_relation_exprt no_overflow_upper(
590  op, ID_lt, upper.to_expr());
591 
592  ieee_floatt lower(to_floatbv_type(old_type));
593  lower.from_integer(-power(2, new_width-1)-1);
594  const binary_relation_exprt no_overflow_lower(
595  op, ID_gt, lower.to_expr());
596 
598  and_exprt(no_overflow_lower, no_overflow_upper),
599  "arithmetic overflow on float to signed integer type conversion",
600  "overflow",
601  expr.find_source_location(),
602  expr,
603  guard);
604  }
605  }
606  else if(type.id()==ID_unsignedbv)
607  {
608  std::size_t new_width=to_unsignedbv_type(type).get_width();
609 
610  if(old_type.id()==ID_signedbv) // signed -> unsigned
611  {
612  std::size_t old_width=to_signedbv_type(old_type).get_width();
613 
614  if(new_width>=old_width-1)
615  {
616  // only need lower bound check
617  const binary_relation_exprt no_overflow_lower(
618  op, ID_ge, from_integer(0, old_type));
619 
621  no_overflow_lower,
622  "arithmetic overflow on signed to unsigned type conversion",
623  "overflow",
624  expr.find_source_location(),
625  expr,
626  guard);
627  }
628  else
629  {
630  // need both
631  const binary_relation_exprt no_overflow_upper(
632  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
633 
634  const binary_relation_exprt no_overflow_lower(
635  op, ID_ge, from_integer(0, old_type));
636 
638  and_exprt(no_overflow_lower, no_overflow_upper),
639  "arithmetic overflow on signed to unsigned type conversion",
640  "overflow",
641  expr.find_source_location(),
642  expr,
643  guard);
644  }
645  }
646  else if(old_type.id()==ID_unsignedbv) // unsigned -> unsigned
647  {
648  std::size_t old_width=to_unsignedbv_type(old_type).get_width();
649  if(new_width>=old_width)
650  return; // always ok
651 
652  const binary_relation_exprt no_overflow_upper(
653  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
654 
656  no_overflow_upper,
657  "arithmetic overflow on unsigned to unsigned type conversion",
658  "overflow",
659  expr.find_source_location(),
660  expr,
661  guard);
662  }
663  else if(old_type.id()==ID_floatbv) // float -> unsigned
664  {
665  // Note that the fractional part is truncated!
666  ieee_floatt upper(to_floatbv_type(old_type));
667  upper.from_integer(power(2, new_width)-1);
668  const binary_relation_exprt no_overflow_upper(
669  op, ID_lt, upper.to_expr());
670 
671  ieee_floatt lower(to_floatbv_type(old_type));
672  lower.from_integer(-1);
673  const binary_relation_exprt no_overflow_lower(
674  op, ID_gt, lower.to_expr());
675 
677  and_exprt(no_overflow_lower, no_overflow_upper),
678  "arithmetic overflow on float to unsigned integer type conversion",
679  "overflow",
680  expr.find_source_location(),
681  expr,
682  guard);
683  }
684  }
685  }
686 }
687 
689  const exprt &expr,
690  const guardt &guard)
691 {
694  return;
695 
696  // First, check type.
697  const typet &type = expr.type();
698 
699  if(type.id()==ID_signedbv && !enable_signed_overflow_check)
700  return;
701 
702  if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
703  return;
704 
705  // add overflow subgoal
706 
707  if(expr.id()==ID_div)
708  {
709  // undefined for signed division INT_MIN/-1
710  if(type.id()==ID_signedbv)
711  {
712  const auto &div_expr = to_div_expr(expr);
713 
714  equal_exprt int_min_eq(
715  div_expr.dividend(), to_signedbv_type(type).smallest_expr());
716 
717  equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
718 
720  not_exprt(and_exprt(int_min_eq, minus_one_eq)),
721  "arithmetic overflow on signed division",
722  "overflow",
723  expr.find_source_location(),
724  expr,
725  guard);
726  }
727 
728  return;
729  }
730  else if(expr.id()==ID_unary_minus)
731  {
732  if(type.id()==ID_signedbv)
733  {
734  // overflow on unary- can only happen with the smallest
735  // representable number 100....0
736 
737  equal_exprt int_min_eq(
738  to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
739 
741  not_exprt(int_min_eq),
742  "arithmetic overflow on signed unary minus",
743  "overflow",
744  expr.find_source_location(),
745  expr,
746  guard);
747  }
748 
749  return;
750  }
751  else if(expr.id() == ID_shl)
752  {
753  if(type.id() == ID_signedbv)
754  {
755  const auto &shl_expr = to_shl_expr(expr);
756  const auto &op = shl_expr.op();
757  const auto &op_type = to_signedbv_type(type);
758  const auto op_width = op_type.get_width();
759  const auto &distance = shl_expr.distance();
760  const auto &distance_type = distance.type();
761 
762  // a left shift of a negative value is undefined;
763  // yet this isn't an overflow
764  exprt neg_value_shift;
765 
766  if(op_type.id() == ID_unsignedbv)
767  neg_value_shift = false_exprt();
768  else
769  neg_value_shift =
770  binary_relation_exprt(op, ID_lt, from_integer(0, op_type));
771 
772  // a shift with negative distance is undefined;
773  // yet this isn't an overflow
774  exprt neg_dist_shift;
775 
776  if(distance_type.id() == ID_unsignedbv)
777  neg_dist_shift = false_exprt();
778  else
779  neg_dist_shift =
780  binary_relation_exprt(op, ID_lt, from_integer(0, distance_type));
781 
782  // shifting a non-zero value by more than its width is undefined;
783  // yet this isn't an overflow
784  const exprt dist_too_large = binary_predicate_exprt(
785  distance, ID_gt, from_integer(op_width, distance_type));
786 
787  const exprt op_zero = equal_exprt(op, from_integer(0, op_type));
788 
789  auto new_type = to_bitvector_type(op_type);
790  new_type.set_width(op_width * 2);
791 
792  const exprt op_ext = typecast_exprt(op, new_type);
793 
794  const exprt op_ext_shifted = shl_exprt(op_ext, distance);
795 
796  // The semantics of signed left shifts are contentious for the case
797  // that a '1' is shifted into the signed bit.
798  // Assuming 32-bit integers, 1<<31 is implementation-defined
799  // in ANSI C and C++98, but is explicitly undefined by C99,
800  // C11 and C++11.
801  bool allow_shift_into_sign_bit = true;
802 
803  if(mode == ID_C)
804  {
805  if(
808  {
809  allow_shift_into_sign_bit = false;
810  }
811  }
812  else if(mode == ID_cpp)
813  {
814  if(
817  {
818  allow_shift_into_sign_bit = false;
819  }
820  }
821 
822  const unsigned number_of_top_bits =
823  allow_shift_into_sign_bit ? op_width : op_width + 1;
824 
825  const exprt top_bits = extractbits_exprt(
826  op_ext_shifted,
827  new_type.get_width() - 1,
828  new_type.get_width() - number_of_top_bits,
829  unsignedbv_typet(number_of_top_bits));
830 
831  const exprt top_bits_zero =
832  equal_exprt(top_bits, from_integer(0, top_bits.type()));
833 
834  // a negative distance shift isn't an overflow;
835  // a negative value shift isn't an overflow;
836  // a shift that's too far isn't an overflow;
837  // a shift of zero isn't overflow;
838  // else check the top bits
840  disjunction({neg_value_shift,
841  neg_dist_shift,
842  dist_too_large,
843  op_zero,
844  top_bits_zero}),
845  "arithmetic overflow on signed shl",
846  "overflow",
847  expr.find_source_location(),
848  expr,
849  guard);
850  }
851 
852  return;
853  }
854 
855  multi_ary_exprt overflow(
856  "overflow-" + expr.id_string(), expr.operands(), bool_typet());
857 
858  if(expr.operands().size()>=3)
859  {
860  // The overflow checks are binary!
861  // We break these up.
862 
863  for(std::size_t i=1; i<expr.operands().size(); i++)
864  {
865  exprt tmp;
866 
867  if(i==1)
868  tmp = to_multi_ary_expr(expr).op0();
869  else
870  {
871  tmp=expr;
872  tmp.operands().resize(i);
873  }
874 
875  overflow.operands().resize(2);
876  overflow.op0()=tmp;
877  overflow.op1()=expr.operands()[i];
878 
879  std::string kind=
880  type.id()==ID_unsignedbv?"unsigned":"signed";
881 
883  not_exprt(overflow),
884  "arithmetic overflow on " + kind + " " + expr.id_string(),
885  "overflow",
886  expr.find_source_location(),
887  expr,
888  guard);
889  }
890  }
891  else
892  {
893  std::string kind=
894  type.id()==ID_unsignedbv?"unsigned":"signed";
895 
897  not_exprt(overflow),
898  "arithmetic overflow on " + kind + " " + expr.id_string(),
899  "overflow",
900  expr.find_source_location(),
901  expr,
902  guard);
903  }
904 }
905 
907  const exprt &expr,
908  const guardt &guard)
909 {
911  return;
912 
913  // First, check type.
914  const typet &type = expr.type();
915 
916  if(type.id()!=ID_floatbv)
917  return;
918 
919  // add overflow subgoal
920 
921  if(expr.id()==ID_typecast)
922  {
923  // Can overflow if casting from larger
924  // to smaller type.
925  const auto &op = to_typecast_expr(expr).op();
926  if(op.type().id() == ID_floatbv)
927  {
928  // float-to-float
929  or_exprt overflow_check{isinf_exprt(op), not_exprt(isinf_exprt(expr))};
930 
932  std::move(overflow_check),
933  "arithmetic overflow on floating-point typecast",
934  "overflow",
935  expr.find_source_location(),
936  expr,
937  guard);
938  }
939  else
940  {
941  // non-float-to-float
943  not_exprt(isinf_exprt(expr)),
944  "arithmetic overflow on floating-point typecast",
945  "overflow",
946  expr.find_source_location(),
947  expr,
948  guard);
949  }
950 
951  return;
952  }
953  else if(expr.id()==ID_div)
954  {
955  // Can overflow if dividing by something small
956  or_exprt overflow_check(
957  isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
958 
960  std::move(overflow_check),
961  "arithmetic overflow on floating-point division",
962  "overflow",
963  expr.find_source_location(),
964  expr,
965  guard);
966 
967  return;
968  }
969  else if(expr.id()==ID_mod)
970  {
971  // Can't overflow
972  return;
973  }
974  else if(expr.id()==ID_unary_minus)
975  {
976  // Can't overflow
977  return;
978  }
979  else if(expr.id()==ID_plus || expr.id()==ID_mult ||
980  expr.id()==ID_minus)
981  {
982  if(expr.operands().size()==2)
983  {
984  // Can overflow
985  or_exprt overflow_check(
986  isinf_exprt(to_binary_expr(expr).op0()),
987  isinf_exprt(to_binary_expr(expr).op1()),
988  not_exprt(isinf_exprt(expr)));
989 
990  std::string kind=
991  expr.id()==ID_plus?"addition":
992  expr.id()==ID_minus?"subtraction":
993  expr.id()==ID_mult?"multiplication":"";
994 
996  std::move(overflow_check),
997  "arithmetic overflow on floating-point " + kind,
998  "overflow",
999  expr.find_source_location(),
1000  expr,
1001  guard);
1002 
1003  return;
1004  }
1005  else if(expr.operands().size()>=3)
1006  {
1007  assert(expr.id()!=ID_minus);
1008 
1009  // break up
1010  float_overflow_check(make_binary(expr), guard);
1011  return;
1012  }
1013  }
1014 }
1015 
1017  const exprt &expr,
1018  const guardt &guard)
1019 {
1020  if(!enable_nan_check)
1021  return;
1022 
1023  // first, check type
1024  if(expr.type().id()!=ID_floatbv)
1025  return;
1026 
1027  if(expr.id()!=ID_plus &&
1028  expr.id()!=ID_mult &&
1029  expr.id()!=ID_div &&
1030  expr.id()!=ID_minus)
1031  return;
1032 
1033  // add NaN subgoal
1034 
1035  exprt isnan;
1036 
1037  if(expr.id()==ID_div)
1038  {
1039  const auto &div_expr = to_div_expr(expr);
1040 
1041  // there a two ways to get a new NaN on division:
1042  // 0/0 = NaN and x/inf = NaN
1043  // (note that x/0 = +-inf for x!=0 and x!=inf)
1044  const and_exprt zero_div_zero(
1046  div_expr.op0(), from_integer(0, div_expr.dividend().type())),
1048  div_expr.op1(), from_integer(0, div_expr.divisor().type())));
1049 
1050  const isinf_exprt div_inf(div_expr.op1());
1051 
1052  isnan=or_exprt(zero_div_zero, div_inf);
1053  }
1054  else if(expr.id()==ID_mult)
1055  {
1056  if(expr.operands().size()>=3)
1057  return nan_check(make_binary(expr), guard);
1058 
1059  const auto &mult_expr = to_mult_expr(expr);
1060 
1061  // Inf * 0 is NaN
1062  const and_exprt inf_times_zero(
1063  isinf_exprt(mult_expr.op0()),
1065  mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
1066 
1067  const and_exprt zero_times_inf(
1069  mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
1070  isinf_exprt(mult_expr.op0()));
1071 
1072  isnan=or_exprt(inf_times_zero, zero_times_inf);
1073  }
1074  else if(expr.id()==ID_plus)
1075  {
1076  if(expr.operands().size()>=3)
1077  return nan_check(make_binary(expr), guard);
1078 
1079  const auto &plus_expr = to_plus_expr(expr);
1080 
1081  // -inf + +inf = NaN and +inf + -inf = NaN,
1082  // i.e., signs differ
1083  ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
1084  exprt plus_inf=ieee_floatt::plus_infinity(spec).to_expr();
1085  exprt minus_inf=ieee_floatt::minus_infinity(spec).to_expr();
1086 
1087  isnan = or_exprt(
1088  and_exprt(
1089  equal_exprt(plus_expr.op0(), minus_inf),
1090  equal_exprt(plus_expr.op1(), plus_inf)),
1091  and_exprt(
1092  equal_exprt(plus_expr.op0(), plus_inf),
1093  equal_exprt(plus_expr.op1(), minus_inf)));
1094  }
1095  else if(expr.id()==ID_minus)
1096  {
1097  // +inf - +inf = NaN and -inf - -inf = NaN,
1098  // i.e., signs match
1099 
1100  const auto &minus_expr = to_minus_expr(expr);
1101 
1102  ieee_float_spect spec =
1103  ieee_float_spect(to_floatbv_type(minus_expr.type()));
1104  exprt plus_inf=ieee_floatt::plus_infinity(spec).to_expr();
1105  exprt minus_inf=ieee_floatt::minus_infinity(spec).to_expr();
1106 
1107  isnan = or_exprt(
1108  and_exprt(
1109  equal_exprt(minus_expr.lhs(), plus_inf),
1110  equal_exprt(minus_expr.rhs(), plus_inf)),
1111  and_exprt(
1112  equal_exprt(minus_expr.lhs(), minus_inf),
1113  equal_exprt(minus_expr.rhs(), minus_inf)));
1114  }
1115  else
1116  UNREACHABLE;
1117 
1119  boolean_negate(isnan),
1120  "NaN on " + expr.id_string(),
1121  "NaN",
1122  expr.find_source_location(),
1123  expr,
1124  guard);
1125 }
1126 
1128  const binary_exprt &expr,
1129  const guardt &guard)
1130 {
1132  return;
1133 
1134  if(expr.op0().type().id()==ID_pointer &&
1135  expr.op1().type().id()==ID_pointer)
1136  {
1137  // add same-object subgoal
1138 
1139  exprt same_object = ::same_object(expr.op0(), expr.op1());
1140 
1142  same_object,
1143  "same object violation",
1144  "pointer",
1145  expr.find_source_location(),
1146  expr,
1147  guard);
1148 
1149  for(const auto &pointer : expr.operands())
1150  {
1151  // just this particular byte must be within object bounds or one past the
1152  // end
1153  const auto size = from_integer(0, size_type());
1154  auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1155 
1156  for(const auto &c : conditions)
1157  {
1159  c.assertion,
1160  "pointer relation: " + c.description,
1161  "pointer arithmetic",
1162  expr.find_source_location(),
1163  pointer,
1164  guard);
1165  }
1166  }
1167  }
1168 }
1169 
1171  const exprt &expr,
1172  const guardt &guard)
1173 {
1175  return;
1176 
1177  if(expr.id() != ID_plus && expr.id() != ID_minus)
1178  return;
1179 
1181  expr.operands().size() == 2,
1182  "pointer arithmetic expected to have exactly 2 operands");
1183 
1184  // the result must be within object bounds or one past the end
1185  const auto size = from_integer(0, size_type());
1186  auto conditions = get_pointer_dereferenceable_conditions(expr, size);
1187 
1188  for(const auto &c : conditions)
1189  {
1191  c.assertion,
1192  "pointer arithmetic: " + c.description,
1193  "pointer arithmetic",
1194  expr.find_source_location(),
1195  expr,
1196  guard);
1197  }
1198 }
1199 
1201  const dereference_exprt &expr,
1202  const exprt &src_expr,
1203  const guardt &guard)
1204 {
1206  return;
1207 
1208  const exprt &pointer=expr.pointer();
1209 
1210  exprt size;
1211 
1212  if(expr.type().id() == ID_empty)
1213  {
1214  // a dereference *p (with p being a pointer to void) is valid if p points to
1215  // valid memory (of any size). the smallest possible size of the memory
1216  // segment p could be pointing to is 1, hence we use this size for the
1217  // address check
1218  size = from_integer(1, size_type());
1219  }
1220  else
1221  {
1222  auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1223  CHECK_RETURN(size_of_expr_opt.has_value());
1224  size = size_of_expr_opt.value();
1225  }
1226 
1227  auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
1228 
1229  for(const auto &c : conditions)
1230  {
1232  c.assertion,
1233  "dereference failure: " + c.description,
1234  "pointer dereference",
1235  src_expr.find_source_location(),
1236  src_expr,
1237  guard);
1238  }
1239 }
1240 
1242  const exprt &expr,
1243  const guardt &guard)
1244 {
1246  return;
1247 
1248  if(expr.source_location().is_built_in())
1249  return;
1250 
1251  const exprt pointer = (expr.id() == ID_r_ok || expr.id() == ID_w_ok)
1252  ? to_binary_expr(expr).lhs()
1253  : to_unary_expr(expr).op();
1254 
1255  CHECK_RETURN(pointer.type().id() == ID_pointer);
1256 
1257  if(pointer.id() == ID_symbol)
1258  {
1259  const auto &symbol_expr = to_symbol_expr(pointer);
1260 
1261  if(has_prefix(id2string(symbol_expr.get_identifier()), CPROVER_PREFIX))
1262  return;
1263  }
1264 
1265  const auto size_of_expr_opt = size_of_expr(pointer.type().subtype(), ns);
1266 
1267  const exprt size = !size_of_expr_opt.has_value()
1268  ? from_integer(1, size_type())
1269  : size_of_expr_opt.value();
1270 
1271  const conditionst &conditions =
1273  for(const auto &c : conditions)
1274  {
1276  or_exprt{null_object(pointer), c.assertion},
1277  c.description,
1278  "pointer primitives",
1279  expr.source_location(),
1280  expr,
1281  guard);
1282  }
1283 }
1284 
1286 {
1287  // we don't need to include the __CPROVER_same_object primitive here as it
1288  // is replaced by lower level primitives in the special function handling
1289  // during typechecking (see c_typecheck_expr.cpp)
1290  return expr.id() == ID_pointer_object || expr.id() == ID_pointer_offset ||
1291  expr.id() == ID_object_size || expr.id() == ID_r_ok ||
1292  expr.id() == ID_w_ok || expr.id() == ID_is_dynamic_object;
1293 }
1294 
1296  const exprt &address,
1297  const exprt &size)
1298 {
1299  auto conditions =
1301  if(auto maybe_null_condition = get_pointer_is_null_condition(address, size))
1302  {
1303  conditions.push_front(*maybe_null_condition);
1304  }
1305  return conditions;
1306 }
1307 
1308 std::string goto_checkt::array_name(const exprt &expr)
1309 {
1310  return ::array_name(ns, expr);
1311 }
1312 
1314  const index_exprt &expr,
1315  const guardt &guard)
1316 {
1317  if(!enable_bounds_check)
1318  return;
1319 
1320  if(expr.find("bounds_check").is_not_nil() &&
1321  !expr.get_bool("bounds_check"))
1322  return;
1323 
1324  typet array_type = expr.array().type();
1325 
1326  if(array_type.id()==ID_pointer)
1327  throw "index got pointer as array type";
1328  else if(array_type.id()!=ID_array && array_type.id()!=ID_vector)
1329  throw "bounds check expected array or vector type, got "
1330  +array_type.id_string();
1331 
1332  std::string name=array_name(expr.array());
1333 
1334  const exprt &index=expr.index();
1336  ode.build(expr, ns);
1337 
1338  if(index.type().id()!=ID_unsignedbv)
1339  {
1340  // we undo typecasts to signedbv
1341  if(
1342  index.id() == ID_typecast &&
1343  to_typecast_expr(index).op().type().id() == ID_unsignedbv)
1344  {
1345  // ok
1346  }
1347  else
1348  {
1349  const auto i = numeric_cast<mp_integer>(index);
1350 
1351  if(!i.has_value() || *i < 0)
1352  {
1353  exprt effective_offset=ode.offset();
1354 
1355  if(ode.root_object().id()==ID_dereference)
1356  {
1357  exprt p_offset=pointer_offset(
1359  assert(p_offset.type()==effective_offset.type());
1360 
1361  effective_offset=plus_exprt(p_offset, effective_offset);
1362  }
1363 
1364  exprt zero=from_integer(0, ode.offset().type());
1365 
1366  // the final offset must not be negative
1367  binary_relation_exprt inequality(
1368  effective_offset, ID_ge, std::move(zero));
1369 
1371  inequality,
1372  name + " lower bound",
1373  "array bounds",
1374  expr.find_source_location(),
1375  expr,
1376  guard);
1377  }
1378  }
1379  }
1380 
1381  exprt type_matches_size=true_exprt();
1382 
1383  if(ode.root_object().id()==ID_dereference)
1384  {
1385  const exprt &pointer=
1387 
1388  const if_exprt size(
1389  dynamic_object(pointer),
1390  typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
1391  object_size(pointer));
1392 
1393  const plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
1394 
1395  assert(effective_offset.op0().type()==effective_offset.op1().type());
1396 
1397  const auto size_casted =
1398  typecast_exprt::conditional_cast(size, effective_offset.type());
1399 
1400  binary_relation_exprt inequality(effective_offset, ID_lt, size_casted);
1401 
1402  exprt in_bounds_of_some_explicit_allocation =
1404  pointer,
1405  plus_exprt{ode.offset(), from_integer(1, ode.offset().type())});
1406 
1407  or_exprt precond(
1408  std::move(in_bounds_of_some_explicit_allocation),
1409  and_exprt(dynamic_object(pointer), not_exprt(malloc_object(pointer, ns))),
1410  inequality);
1411 
1413  precond,
1414  name + " dynamic object upper bound",
1415  "array bounds",
1416  expr.find_source_location(),
1417  expr,
1418  guard);
1419 
1420  auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
1421 
1422  if(type_size_opt.has_value())
1423  {
1424  // Build a predicate that evaluates to true iff the size reported by
1425  // sizeof (i.e., compile-time size) matches the actual run-time size. The
1426  // run-time size for a dynamic (i.e., heap-allocated) object is determined
1427  // by the dynamic_size(ns) expression, which can only be used when
1428  // malloc_object(pointer, ns) evaluates to true for a given pointer.
1429  type_matches_size = if_exprt{
1430  dynamic_object(pointer),
1431  and_exprt{malloc_object(pointer, ns),
1433  dynamic_size(ns), type_size_opt->type()),
1434  *type_size_opt}},
1436  object_size(pointer), type_size_opt->type()),
1437  *type_size_opt}};
1438  }
1439  }
1440 
1441  const exprt &size=array_type.id()==ID_array ?
1442  to_array_type(array_type).size() :
1443  to_vector_type(array_type).size();
1444 
1445  if(size.is_nil())
1446  {
1447  // Linking didn't complete, we don't have a size.
1448  // Not clear what to do.
1449  }
1450  else if(size.id()==ID_infinity)
1451  {
1452  }
1453  else if(size.is_zero() &&
1454  expr.array().id()==ID_member)
1455  {
1456  // a variable sized struct member
1457  //
1458  // Excerpt from the C standard on flexible array members:
1459  // However, when a . (or ->) operator has a left operand that is (a pointer
1460  // to) a structure with a flexible array member and the right operand names
1461  // that member, it behaves as if that member were replaced with the longest
1462  // array (with the same element type) that would not make the structure
1463  // larger than the object being accessed; [...]
1464  const auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
1465  CHECK_RETURN(type_size_opt.has_value());
1466 
1467  binary_relation_exprt inequality(
1469  ode.offset(), type_size_opt.value().type()),
1470  ID_lt,
1471  type_size_opt.value());
1472 
1474  implies_exprt(type_matches_size, inequality),
1475  name + " upper bound",
1476  "array bounds",
1477  expr.find_source_location(),
1478  expr,
1479  guard);
1480  }
1481  else
1482  {
1483  binary_relation_exprt inequality(index, ID_lt, size);
1484 
1485  // typecast size
1486  inequality.op1() = typecast_exprt::conditional_cast(
1487  inequality.op1(), inequality.op0().type());
1488 
1490  implies_exprt(type_matches_size, inequality),
1491  name + " upper bound",
1492  "array bounds",
1493  expr.find_source_location(),
1494  expr,
1495  guard);
1496  }
1497 }
1498 
1500  const exprt &asserted_expr,
1501  const std::string &comment,
1502  const std::string &property_class,
1503  const source_locationt &source_location,
1504  const exprt &src_expr,
1505  const guardt &guard)
1506 {
1507  // first try simplifier on it
1508  exprt simplified_expr =
1509  enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
1510 
1511  // throw away trivial properties?
1512  if(!retain_trivial && simplified_expr.is_true())
1513  return;
1514 
1515  // add the guard
1516  exprt guarded_expr =
1517  guard.is_true()
1518  ? std::move(simplified_expr)
1519  : implies_exprt{guard.as_expr(), std::move(simplified_expr)};
1520 
1521  if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1522  {
1523  auto t = new_code.add(
1525  std::move(guarded_expr), source_location)
1527  std::move(guarded_expr), source_location));
1528 
1529  std::string source_expr_string;
1530  get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
1531 
1532  t->source_location.set_comment(comment + " in " + source_expr_string);
1533  t->source_location.set_property_class(property_class);
1534  }
1535 }
1536 
1538 {
1539  // we don't look into quantifiers
1540  if(expr.id() == ID_exists || expr.id() == ID_forall)
1541  return;
1542 
1543  if(expr.id() == ID_dereference)
1544  {
1545  check_rec(to_dereference_expr(expr).pointer(), guard);
1546  }
1547  else if(expr.id() == ID_index)
1548  {
1549  const index_exprt &index_expr = to_index_expr(expr);
1550  check_rec_address(index_expr.array(), guard);
1551  check_rec(index_expr.index(), guard);
1552  }
1553  else
1554  {
1555  for(const auto &operand : expr.operands())
1556  check_rec_address(operand, guard);
1557  }
1558 }
1559 
1561 {
1562  INVARIANT(
1563  expr.is_boolean(),
1564  "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
1565 
1566  guardt old_guard = guard;
1567 
1568  for(const auto &op : expr.operands())
1569  {
1570  INVARIANT(
1571  op.is_boolean(),
1572  "'" + expr.id_string() + "' takes Boolean operands only, but got " +
1573  op.pretty());
1574 
1575  check_rec(op, guard);
1576  guard.add(expr.id() == ID_or ? boolean_negate(op) : op);
1577  }
1578 
1579  guard = std::move(old_guard);
1580 }
1581 
1582 void goto_checkt::check_rec_if(const if_exprt &if_expr, guardt &guard)
1583 {
1584  INVARIANT(
1585  if_expr.cond().is_boolean(),
1586  "first argument of if must be boolean, but got " + if_expr.cond().pretty());
1587 
1588  check_rec(if_expr.cond(), guard);
1589 
1590  {
1591  guardt old_guard = guard;
1592  guard.add(if_expr.cond());
1593  check_rec(if_expr.true_case(), guard);
1594  guard = std::move(old_guard);
1595  }
1596 
1597  {
1598  guardt old_guard = guard;
1599  guard.add(not_exprt{if_expr.cond()});
1600  check_rec(if_expr.false_case(), guard);
1601  guard = std::move(old_guard);
1602  }
1603 }
1604 
1606 {
1607  const dereference_exprt &deref = to_dereference_expr(member.struct_op());
1608 
1609  check_rec(deref.pointer(), guard);
1610 
1611  // avoid building the following expressions when pointer_validity_check
1612  // would return immediately anyway
1614  return true;
1615 
1616  // we rewrite s->member into *(s+member_offset)
1617  // to avoid requiring memory safety of the entire struct
1618  auto member_offset_opt = member_offset_expr(member, ns);
1619 
1620  if(member_offset_opt.has_value())
1621  {
1622  pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1623  new_pointer_type.subtype() = member.type();
1624 
1625  const exprt char_pointer = typecast_exprt::conditional_cast(
1626  deref.pointer(), pointer_type(char_type()));
1627 
1628  const exprt new_address_casted = typecast_exprt::conditional_cast(
1629  plus_exprt{char_pointer,
1631  member_offset_opt.value(), pointer_diff_type())},
1632  new_pointer_type);
1633 
1634  dereference_exprt new_deref{new_address_casted};
1635  new_deref.add_source_location() = deref.source_location();
1636  pointer_validity_check(new_deref, member, guard);
1637 
1638  return true;
1639  }
1640  return false;
1641 }
1642 
1643 void goto_checkt::check_rec_div(const div_exprt &div_expr, guardt &guard)
1644 {
1645  div_by_zero_check(to_div_expr(div_expr), guard);
1646 
1647  if(div_expr.type().id() == ID_signedbv)
1648  integer_overflow_check(div_expr, guard);
1649  else if(div_expr.type().id() == ID_floatbv)
1650  {
1651  nan_check(div_expr, guard);
1652  float_overflow_check(div_expr, guard);
1653  }
1654 }
1655 
1657 {
1658  if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1659  {
1660  integer_overflow_check(expr, guard);
1661 
1662  if(
1663  expr.operands().size() == 2 && expr.id() == ID_minus &&
1664  expr.operands()[0].type().id() == ID_pointer &&
1665  expr.operands()[1].type().id() == ID_pointer)
1666  {
1667  pointer_rel_check(to_binary_expr(expr), guard);
1668  }
1669  }
1670  else if(expr.type().id() == ID_floatbv)
1671  {
1672  nan_check(expr, guard);
1673  float_overflow_check(expr, guard);
1674  }
1675  else if(expr.type().id() == ID_pointer)
1676  {
1677  pointer_overflow_check(expr, guard);
1678  }
1679 }
1680 
1681 void goto_checkt::check_rec(const exprt &expr, guardt &guard)
1682 {
1683  // we don't look into quantifiers
1684  if(expr.id() == ID_exists || expr.id() == ID_forall)
1685  return;
1686 
1687  if(expr.id() == ID_address_of)
1688  {
1689  check_rec_address(to_address_of_expr(expr).object(), guard);
1690  return;
1691  }
1692  else if(expr.id() == ID_and || expr.id() == ID_or)
1693  {
1694  check_rec_logical_op(expr, guard);
1695  return;
1696  }
1697  else if(expr.id() == ID_if)
1698  {
1699  check_rec_if(to_if_expr(expr), guard);
1700  return;
1701  }
1702  else if(
1703  expr.id() == ID_member &&
1704  to_member_expr(expr).struct_op().id() == ID_dereference)
1705  {
1706  if(check_rec_member(to_member_expr(expr), guard))
1707  return;
1708  }
1709 
1710  forall_operands(it, expr)
1711  check_rec(*it, guard);
1712 
1713  if(expr.type().id() == ID_c_enum_tag)
1714  enum_range_check(expr, guard);
1715 
1716  if(expr.id()==ID_index)
1717  {
1718  bounds_check(to_index_expr(expr), guard);
1719  }
1720  else if(expr.id()==ID_div)
1721  {
1722  check_rec_div(to_div_expr(expr), guard);
1723  }
1724  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
1725  {
1726  undefined_shift_check(to_shift_expr(expr), guard);
1727 
1728  if(expr.id()==ID_shl && expr.type().id()==ID_signedbv)
1729  integer_overflow_check(expr, guard);
1730  }
1731  else if(expr.id()==ID_mod)
1732  {
1733  mod_by_zero_check(to_mod_expr(expr), guard);
1734  mod_overflow_check(to_mod_expr(expr), guard);
1735  }
1736  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
1737  expr.id()==ID_mult ||
1738  expr.id()==ID_unary_minus)
1739  {
1740  check_rec_arithmetic_op(expr, guard);
1741  }
1742  else if(expr.id()==ID_typecast)
1743  conversion_check(expr, guard);
1744  else if(expr.id()==ID_le || expr.id()==ID_lt ||
1745  expr.id()==ID_ge || expr.id()==ID_gt)
1747  else if(expr.id()==ID_dereference)
1748  {
1749  pointer_validity_check(to_dereference_expr(expr), expr, guard);
1750  }
1751  else if(is_pointer_primitive(expr))
1752  {
1753  pointer_primitive_check(expr, guard);
1754  }
1755 }
1756 
1757 void goto_checkt::check(const exprt &expr)
1758 {
1759  guardt guard{true_exprt{}, guard_manager};
1760  check_rec(expr, guard);
1761 }
1762 
1765 {
1766  bool modified = false;
1767 
1768  for(auto &op : expr.operands())
1769  {
1770  auto op_result = rw_ok_check(op);
1771  if(op_result.has_value())
1772  {
1773  op = *op_result;
1774  modified = true;
1775  }
1776  }
1777 
1778  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok)
1779  {
1780  // these get an address as first argument and a size as second
1782  expr.operands().size() == 2, "r/w_ok must have two operands");
1783 
1784  const auto conditions = get_pointer_dereferenceable_conditions(
1785  to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
1786 
1787  exprt::operandst conjuncts;
1788 
1789  for(const auto &c : conditions)
1790  conjuncts.push_back(c.assertion);
1791 
1792  return conjunction(conjuncts);
1793  }
1794  else if(modified)
1795  return std::move(expr);
1796  else
1797  return {};
1798 }
1799 
1803 {
1804 public:
1806  void set_flag(bool &flag, bool new_value)
1807  {
1808  if(flag != new_value)
1809  {
1810  flags_to_reset.emplace_back(&flag, flag);
1811  flag = new_value;
1812  }
1813  }
1814 
1817  {
1818  for(const auto &flag_pair : flags_to_reset)
1819  *flag_pair.first = flag_pair.second;
1820  }
1821 
1822 private:
1823  std::list<std::pair<bool *, bool>> flags_to_reset;
1824 };
1825 
1827  const irep_idt &function_identifier,
1828  goto_functiont &goto_function)
1829 {
1830  assertions.clear();
1831 
1832  const auto &function_symbol = ns.lookup(function_identifier);
1833  mode = function_symbol.mode;
1834 
1835  bool did_something = false;
1836 
1838  util_make_unique<local_bitvector_analysist>(goto_function, ns);
1839 
1840  goto_programt &goto_program=goto_function.body;
1841 
1842  Forall_goto_program_instructions(it, goto_program)
1843  {
1844  current_target = it;
1846 
1847  flag_resett flag_resetter;
1848  const auto &pragmas = i.source_location.get_pragmas();
1849  for(const auto &d : pragmas)
1850  {
1851  if(d.first == "disable:bounds-check")
1852  flag_resetter.set_flag(enable_bounds_check, false);
1853  else if(d.first == "disable:pointer-check")
1854  flag_resetter.set_flag(enable_pointer_check, false);
1855  else if(d.first == "disable:memory-leak-check")
1856  flag_resetter.set_flag(enable_memory_leak_check, false);
1857  else if(d.first == "disable:div-by-zero-check")
1858  flag_resetter.set_flag(enable_div_by_zero_check, false);
1859  else if(d.first == "disable:enum-range-check")
1860  flag_resetter.set_flag(enable_enum_range_check, false);
1861  else if(d.first == "disable:signed-overflow-check")
1862  flag_resetter.set_flag(enable_signed_overflow_check, false);
1863  else if(d.first == "disable:unsigned-overflow-check")
1864  flag_resetter.set_flag(enable_unsigned_overflow_check, false);
1865  else if(d.first == "disable:pointer-overflow-check")
1866  flag_resetter.set_flag(enable_pointer_overflow_check, false);
1867  else if(d.first == "disable:float-overflow-check")
1868  flag_resetter.set_flag(enable_float_overflow_check, false);
1869  else if(d.first == "disable:conversion-check")
1870  flag_resetter.set_flag(enable_conversion_check, false);
1871  else if(d.first == "disable:undefined-shift-check")
1872  flag_resetter.set_flag(enable_undefined_shift_check, false);
1873  else if(d.first == "disable:nan-check")
1874  flag_resetter.set_flag(enable_nan_check, false);
1875  else if(d.first == "disable:pointer-primitive-check")
1876  flag_resetter.set_flag(enable_pointer_primitive_check, false);
1877  }
1878 
1879  new_code.clear();
1880 
1881  // we clear all recorded assertions if
1882  // 1) we want to generate all assertions or
1883  // 2) the instruction is a branch target
1884  if(retain_trivial ||
1885  i.is_target())
1886  assertions.clear();
1887 
1888  if(i.has_condition())
1889  {
1890  check(i.get_condition());
1891 
1892  if(has_subexpr(i.get_condition(), [](const exprt &expr) {
1893  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1894  }))
1895  {
1896  auto rw_ok_cond = rw_ok_check(i.get_condition());
1897  if(rw_ok_cond.has_value())
1898  i.set_condition(*rw_ok_cond);
1899  }
1900  }
1901 
1902  // magic ERROR label?
1903  for(const auto &label : error_labels)
1904  {
1905  if(std::find(i.labels.begin(), i.labels.end(), label)!=i.labels.end())
1906  {
1907  auto t = new_code.add(
1911 
1912  t->source_location.set_property_class("error label");
1913  t->source_location.set_comment("error label "+label);
1914  t->source_location.set("user-provided", true);
1915  }
1916  }
1917 
1918  if(i.is_other())
1919  {
1920  const auto &code = i.get_other();
1921  const irep_idt &statement = code.get_statement();
1922 
1923  if(statement==ID_expression)
1924  {
1925  check(code);
1926  }
1927  else if(statement==ID_printf)
1928  {
1929  for(const auto &op : code.operands())
1930  check(op);
1931  }
1932  }
1933  else if(i.is_assign())
1934  {
1935  const code_assignt &code_assign=to_code_assign(i.code);
1936 
1937  // Reset the no_enum_check with the flag reset for exception
1938  // safety
1939  {
1940  flag_resett no_enum_check_flag_resetter;
1941  no_enum_check_flag_resetter.set_flag(no_enum_check, true);
1942  check(code_assign.lhs());
1943  }
1944  check(code_assign.rhs());
1945 
1946  // the LHS might invalidate any assertion
1947  invalidate(code_assign.lhs());
1948 
1949  if(has_subexpr(code_assign.rhs(), [](const exprt &expr) {
1950  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1951  }))
1952  {
1953  exprt &rhs = to_code_assign(i.code).rhs();
1954  auto rw_ok_cond = rw_ok_check(rhs);
1955  if(rw_ok_cond.has_value())
1956  rhs = *rw_ok_cond;
1957  }
1958  }
1959  else if(i.is_function_call())
1960  {
1961  const code_function_callt &code_function_call=
1963 
1964  // for Java, need to check whether 'this' is null
1965  // on non-static method invocations
1966  if(mode==ID_java &&
1968  !code_function_call.arguments().empty() &&
1969  code_function_call.function().type().id()==ID_code &&
1970  to_code_type(code_function_call.function().type()).has_this())
1971  {
1972  exprt pointer=code_function_call.arguments()[0];
1973 
1976 
1977  if(flags.is_unknown() || flags.is_null())
1978  {
1979  notequal_exprt not_eq_null(
1980  pointer,
1982 
1984  not_eq_null,
1985  "this is null on method invocation",
1986  "pointer dereference",
1987  i.source_location,
1988  pointer,
1990  }
1991  }
1992 
1993  for(const auto &op : code_function_call.operands())
1994  check(op);
1995 
1996  // the call might invalidate any assertion
1997  assertions.clear();
1998  }
1999  else if(i.is_return())
2000  {
2001  check(i.return_value());
2002  // the return value invalidate any assertion
2003  invalidate(i.return_value());
2004 
2005  if(has_subexpr(i.return_value(), [](const exprt &expr) {
2006  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2007  }))
2008  {
2009  exprt &return_value = i.return_value();
2010  auto rw_ok_cond = rw_ok_check(return_value);
2011  if(rw_ok_cond.has_value())
2012  return_value = *rw_ok_cond;
2013  }
2014  }
2015  else if(i.is_throw())
2016  {
2017  if(i.code.get_statement()==ID_expression &&
2018  i.code.operands().size()==1 &&
2019  i.code.op0().operands().size()==1)
2020  {
2021  // must not throw NULL
2022 
2023  exprt pointer = to_unary_expr(i.code.op0()).op();
2024 
2025  const notequal_exprt not_eq_null(
2026  pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
2027 
2029  not_eq_null,
2030  "throwing null",
2031  "pointer dereference",
2032  i.source_location,
2033  pointer,
2035  }
2036 
2037  // this has no successor
2038  assertions.clear();
2039  }
2040  else if(i.is_assert())
2041  {
2042  bool is_user_provided=i.source_location.get_bool("user-provided");
2043 
2044  if((is_user_provided && !enable_assertions &&
2045  i.source_location.get_property_class()!="error label") ||
2046  (!is_user_provided && !enable_built_in_assertions))
2047  {
2048  i.turn_into_skip();
2049  did_something = true;
2050  }
2051  }
2052  else if(i.is_assume())
2053  {
2054  if(!enable_assumptions)
2055  {
2056  i.turn_into_skip();
2057  did_something = true;
2058  }
2059  }
2060  else if(i.is_dead())
2061  {
2063  {
2064  assert(i.code.operands().size()==1);
2065  const symbol_exprt &variable=to_symbol_expr(i.code.op0());
2066 
2067  // is it dirty?
2068  if(local_bitvector_analysis->dirty(variable))
2069  {
2070  // need to mark the dead variable as dead
2071  exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2072  exprt address_of_expr = typecast_exprt::conditional_cast(
2073  address_of_exprt(variable), lhs.type());
2074  if_exprt rhs(
2076  std::move(address_of_expr),
2077  lhs);
2080  std::move(lhs), std::move(rhs), i.source_location));
2081  t->code.add_source_location()=i.source_location;
2082  }
2083  }
2084  }
2085  else if(i.is_end_function())
2086  {
2087  if(
2088  function_identifier == goto_functionst::entry_point() &&
2090  {
2091  const symbolt &leak=ns.lookup(CPROVER_PREFIX "memory_leak");
2092  const symbol_exprt leak_expr=leak.symbol_expr();
2093 
2094  // add self-assignment to get helpful counterexample output
2095  new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
2096 
2097  source_locationt source_location;
2098  source_location.set_function(function_identifier);
2099 
2100  equal_exprt eq(
2101  leak_expr,
2104  eq,
2105  "dynamically allocated memory never freed",
2106  "memory-leak",
2107  source_location,
2108  eq,
2110  }
2111  }
2112 
2113  for(auto &instruction : new_code.instructions)
2114  {
2115  if(instruction.source_location.is_nil())
2116  {
2117  instruction.source_location.id(irep_idt());
2118 
2119  if(!it->source_location.get_file().empty())
2120  instruction.source_location.set_file(it->source_location.get_file());
2121 
2122  if(!it->source_location.get_line().empty())
2123  instruction.source_location.set_line(it->source_location.get_line());
2124 
2125  if(!it->source_location.get_function().empty())
2126  instruction.source_location.set_function(
2127  it->source_location.get_function());
2128 
2129  if(!it->source_location.get_column().empty())
2130  {
2131  instruction.source_location.set_column(
2132  it->source_location.get_column());
2133  }
2134 
2135  if(!it->source_location.get_java_bytecode_index().empty())
2136  {
2137  instruction.source_location.set_java_bytecode_index(
2138  it->source_location.get_java_bytecode_index());
2139  }
2140  }
2141  }
2142 
2143  // insert new instructions -- make sure targets are not moved
2144  did_something |= !new_code.instructions.empty();
2145 
2146  while(!new_code.instructions.empty())
2147  {
2148  goto_program.insert_before_swap(it, new_code.instructions.front());
2149  new_code.instructions.pop_front();
2150  it++;
2151  }
2152  }
2153 
2154  if(did_something)
2155  remove_skip(goto_program);
2156 }
2157 
2160  const exprt &address,
2161  const exprt &size)
2162 {
2164  PRECONDITION(address.type().id() == ID_pointer);
2167 
2168  conditionst conditions;
2169 
2170  if(mode == ID_java)
2171  {
2172  // The following conditions don’t apply to Java
2173  return conditions;
2174  }
2175 
2176  const exprt in_bounds_of_some_explicit_allocation =
2178 
2179  const bool unknown = flags.is_unknown() || flags.is_uninitialized();
2180 
2181  if(unknown)
2182  {
2183  conditions.push_back(conditiont{
2184  not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
2185  }
2186 
2187  if(unknown || flags.is_dynamic_heap())
2188  {
2189  conditions.push_back(conditiont(
2190  or_exprt(
2191  in_bounds_of_some_explicit_allocation,
2192  not_exprt(deallocated(address, ns))),
2193  "deallocated dynamic object"));
2194  }
2195 
2196  if(unknown || flags.is_dynamic_local())
2197  {
2198  conditions.push_back(conditiont(
2199  or_exprt(
2200  in_bounds_of_some_explicit_allocation,
2201  not_exprt(dead_object(address, ns))),
2202  "dead object"));
2203  }
2204 
2205  if(unknown || flags.is_dynamic_heap())
2206  {
2207  const or_exprt object_bounds_violation(
2208  object_lower_bound(address, nil_exprt()),
2209  object_upper_bound(address, size));
2210 
2211  conditions.push_back(conditiont(
2212  or_exprt(
2213  in_bounds_of_some_explicit_allocation,
2214  implies_exprt(
2215  dynamic_object(address), not_exprt(object_bounds_violation))),
2216  "pointer outside dynamic object bounds"));
2217  }
2218 
2219  if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
2220  {
2221  const or_exprt object_bounds_violation(
2222  object_lower_bound(address, nil_exprt()),
2223  object_upper_bound(address, size));
2224 
2225  conditions.push_back(conditiont(
2226  or_exprt(
2227  in_bounds_of_some_explicit_allocation,
2228  implies_exprt(
2229  not_exprt(dynamic_object(address)),
2230  not_exprt(object_bounds_violation))),
2231  "pointer outside object bounds"));
2232  }
2233 
2234  if(unknown || flags.is_integer_address())
2235  {
2236  conditions.push_back(conditiont(
2237  implies_exprt(
2238  integer_address(address), in_bounds_of_some_explicit_allocation),
2239  "invalid integer address"));
2240  }
2241 
2242  return conditions;
2243 }
2244 
2246  const exprt &address,
2247  const exprt &size)
2248 {
2250  PRECONDITION(address.type().id() == ID_pointer);
2251  const auto &pointer_type = to_pointer_type(address.type());
2254  if(mode == ID_java)
2255  {
2256  if(flags.is_unknown() || flags.is_null())
2257  {
2258  notequal_exprt not_eq_null(address, null_pointer_exprt{pointer_type});
2259  return {conditiont{not_eq_null, "reference is null"}};
2260  }
2261  }
2262  else if(flags.is_unknown() || flags.is_uninitialized() || flags.is_null())
2263  {
2264  return {conditiont{
2266  not_exprt(null_pointer(address))},
2267  "pointer NULL"}};
2268  }
2269  return {};
2270 }
2271 
2273  const exprt &pointer,
2274  const exprt &size)
2275 {
2276  exprt::operandst alloc_disjuncts;
2277  for(const auto &a : allocations)
2278  {
2279  typecast_exprt int_ptr(pointer, a.first.type());
2280 
2281  binary_relation_exprt lb_check(a.first, ID_le, int_ptr);
2282 
2283  plus_exprt upper_bound{
2284  int_ptr, typecast_exprt::conditional_cast(size, int_ptr.type())};
2285 
2286  binary_relation_exprt ub_check{
2287  std::move(upper_bound), ID_le, plus_exprt{a.first, a.second}};
2288 
2289  alloc_disjuncts.push_back(
2290  and_exprt{std::move(lb_check), std::move(ub_check)});
2291  }
2292  return disjunction(alloc_disjuncts);
2293 }
2294 
2296  const irep_idt &function_identifier,
2297  goto_functionst::goto_functiont &goto_function,
2298  const namespacet &ns,
2299  const optionst &options)
2300 {
2301  goto_checkt goto_check(ns, options);
2302  goto_check.goto_check(function_identifier, goto_function);
2303 }
2304 
2306  const namespacet &ns,
2307  const optionst &options,
2308  goto_functionst &goto_functions)
2309 {
2310  goto_checkt goto_check(ns, options);
2311 
2312  goto_check.collect_allocations(goto_functions);
2313 
2314  for(auto &gf_entry : goto_functions.function_map)
2315  {
2316  goto_check.goto_check(gf_entry.first, gf_entry.second);
2317  }
2318 }
2319 
2321  const optionst &options,
2322  goto_modelt &goto_model)
2323 {
2324  const namespacet ns(goto_model.symbol_table);
2325  goto_check(ns, options, goto_model.goto_functions);
2326 }
goto_checkt::allocationt
std::pair< exprt, exprt > allocationt
Definition: goto_check.cpp:279
goto_checkt::allocationst
std::list< allocationt > allocationst
Definition: goto_check.cpp:280
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:459
guard_exprt
Definition: guard_expr.h:27
goto_checkt::array_name
std::string array_name(const exprt &)
Definition: goto_check.cpp:1308
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:729
goto_functiont::body
goto_programt body
Definition: goto_function.h:29
array_name
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:20
ieee_floatt
Definition: ieee_float.h:120
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
goto_programt::instructiont::is_throw
bool is_throw() const
Definition: goto_program.h:433
goto_checkt::current_target
goto_programt::const_targett current_target
Definition: goto_check.cpp:99
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:741
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:66
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:334
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_enum_typet
The type of C enums.
Definition: std_types.h:628
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:140
conjunction
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:41
goto_checkt::bounds_check
void bounds_check(const index_exprt &, const guardt &)
Definition: goto_check.cpp:1313
goto_checkt::conditiont::assertion
exprt assertion
Definition: goto_check.cpp:169
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1030
goto_checkt::enable_div_by_zero_check
bool enable_div_by_zero_check
Definition: goto_check.cpp:257
local_bitvector_analysis.h
Field-insensitive, location-sensitive bitvector analysis.
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:103
goto_checkt::enable_undefined_shift_check
bool enable_undefined_shift_check
Definition: goto_check.cpp:263
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: pointer_expr.cpp:108
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
goto_checkt::guard_manager
guard_managert guard_manager
Definition: goto_check.cpp:100
null_pointer
exprt null_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:136
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:437
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
goto_checkt::enable_assumptions
bool enable_assumptions
Definition: goto_check.cpp:271
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
goto_checkt::enable_simplify
bool enable_simplify
Definition: goto_check.cpp:265
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:689
typet
The type of an expression, extends irept.
Definition: type.h:28
source_locationt::get_pragmas
const irept::named_subt & get_pragmas() const
Definition: source_location.h:200
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
goto_checkt::enable_nan_check
bool enable_nan_check
Definition: goto_check.cpp:266
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:256
local_bitvector_analysist::flagst::is_dynamic_heap
bool is_dynamic_heap() const
Definition: local_bitvector_analysis.h:131
goto_checkt::new_code
goto_programt new_code
Definition: goto_check.cpp:244
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
goto_checkt::enable_built_in_assertions
bool enable_built_in_assertions
Definition: goto_check.cpp:270
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: std_types.h:652
goto_checkt::check_rec_address
void check_rec_address(const exprt &expr, guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
Definition: goto_check.cpp:1537
pointer_predicates.h
Various predicates over pointers in programs.
goto_programt::instructiont::is_dead
bool is_dead() const
Definition: goto_program.h:439
goto_checkt::enable_assert_to_assume
bool enable_assert_to_assume
Definition: goto_check.cpp:268
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:21
goto_checkt::retain_trivial
bool retain_trivial
Definition: goto_check.cpp:267
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
invariant.h
and_exprt
Boolean AND.
Definition: std_expr.h:1835
goto_checkt::enable_pointer_primitive_check
bool enable_pointer_primitive_check
Definition: goto_check.cpp:272
goto_checkt::allocations
allocationst allocations
Definition: goto_check.cpp:281
flag_resett::~flag_resett
~flag_resett()
Restore the values of all flags that have been modified via set_flag.
Definition: goto_check.cpp:1816
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:831
flag_resett
Set a Boolean flag to a new value (via set_flag) and restore the previous value when the entire objec...
Definition: goto_check.cpp:1803
goto_checkt::pointer_validity_check
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.
Definition: goto_check.cpp:1200
exprt
Base class for all expressions.
Definition: expr.h:54
goto_checkt::enable_conversion_check
bool enable_conversion_check
Definition: goto_check.cpp:262
goto_checkt::check_rec_div
void check_rec_div(const div_exprt &div_expr, guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
Definition: goto_check.cpp:1643
goto_modelt
Definition: goto_model.h:26
guard_exprt::is_true
bool is_true() const
Definition: guard_expr.h:63
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:581
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
mode.h
options.h
Options.
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2295
irep_idt
dstringt irep_idt
Definition: irep.h:37
goto_checkt::no_enum_check
bool no_enum_check
Definition: goto_check.cpp:101
bool_typet
The Boolean type.
Definition: std_types.h:37
goto_checkt::conditionst
std::list< conditiont > conditionst
Definition: goto_check.cpp:173
optionst::value_listt
std::list< std::string > value_listt
Definition: options.h:25
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:71
guardt
guard_exprt guardt
Definition: guard.h:27
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
configt::ansi_c
struct configt::ansi_ct ansi_c
make_binary
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:37
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
div_exprt
Division.
Definition: std_expr.h:981
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
shift_exprt::op
exprt & op()
Definition: bitvector_expr.h:239
equal_exprt
Equality.
Definition: std_expr.h:1140
goto_checkt::nan_check
void nan_check(const exprt &, const guardt &)
Definition: goto_check.cpp:1016
goto_checkt::enable_memory_leak_check
bool enable_memory_leak_check
Definition: goto_check.cpp:256
goto_checkt::enum_range_check
void enum_range_check(const exprt &, const guardt &)
Definition: goto_check.cpp:374
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:915
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
goto_checkt::get_pointer_dereferenceable_conditions
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
Definition: goto_check.cpp:1295
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2124
goto_checkt::pointer_primitive_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.
Definition: goto_check.cpp:1241
notequal_exprt
Disequality.
Definition: std_expr.h:1198
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:320
ieee_float_spect
Definition: ieee_float.h:26
goto_checkt::enable_unsigned_overflow_check
bool enable_unsigned_overflow_check
Definition: goto_check.cpp:260
goto_checkt::enable_float_overflow_check
bool enable_float_overflow_check
Definition: goto_check.cpp:264
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
goto_checkt::mod_by_zero_check
void mod_by_zero_check(const mod_exprt &, const guardt &)
Definition: goto_check.cpp:470
array_typet::size
const exprt & size() const
Definition: std_types.h:976
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
guard.h
Guard Data Structure.
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
goto_checkt::pointer_overflow_check
void pointer_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:1170
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
goto_checkt::check_rec_logical_op
void check_rec_logical_op(const exprt &expr, guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
Definition: goto_check.cpp:1560
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
disjunction
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:29
goto_programt::instructiont::turn_into_skip
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:416
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:864
make_unique.h
find_symbols.h
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
goto_checkt::check
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
Definition: goto_check.cpp:1757
or_exprt
Boolean OR.
Definition: std_expr.h:1943
goto_checkt::check_rec
void check_rec(const exprt &expr, guardt &guard)
Recursively descend into expr and run the appropriate check for each sub-expression,...
Definition: goto_check.cpp:1681
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1075
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1255
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:961
goto_checkt::get_pointer_points_to_valid_memory_conditions
conditionst get_pointer_points_to_valid_memory_conditions(const exprt &address, const exprt &size)
Definition: goto_check.cpp:2159
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:2751
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
goto_checkt::float_overflow_check
void float_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:906
goto_checkt::conditiont
Definition: goto_check.cpp:163
goto_checkt::enable_pointer_check
bool enable_pointer_check
Definition: goto_check.cpp:255
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2558
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:644
guard_exprt::add
void add(const exprt &expr)
Definition: guard_expr.cpp:40
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:767
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:179
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
goto_checkt::ns
const namespacet & ns
Definition: goto_check.cpp:97
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:269
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:128
object_upper_bound
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
Definition: pointer_predicates.cpp:178
std_types.h
Pre-defined types.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
local_bitvector_analysist::flagst::is_integer_address
bool is_integer_address() const
Definition: local_bitvector_analysis.h:161
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:870
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:396
deallocated
exprt deallocated(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:50
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
dead_object
exprt dead_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:58
goto_checkt::enable_enum_range_check
bool enable_enum_range_check
Definition: goto_check.cpp:258
language.h
Abstract interface to support a programming language.
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2529
integer_address
exprt integer_address(const exprt &pointer)
Definition: pointer_predicates.cpp:129
index_exprt::index
exprt & index()
Definition: std_expr.h:1269
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:344
goto_checkt::local_bitvector_analysis
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
Definition: goto_check.cpp:98
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:421
goto_checkt::get_pointer_is_null_condition
optionalt< goto_checkt::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
Definition: goto_check.cpp:2245
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
local_bitvector_analysist::flagst::is_null
bool is_null() const
Definition: local_bitvector_analysis.h:141
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
goto_checkt::enable_assertions
bool enable_assertions
Definition: goto_check.cpp:269
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:32
local_bitvector_analysist::flagst::is_static_lifetime
bool is_static_lifetime() const
Definition: local_bitvector_analysis.h:151
irept::is_nil
bool is_nil() const
Definition: irep.h:387
goto_checkt::check_rec_member
bool check_rec_member(const member_exprt &member, guardt &guard)
Check that a member expression is valid:
Definition: goto_check.cpp:1605
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_programt::instructiont::is_end_function
bool is_end_function() const
Definition: goto_program.h:446
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
floatbv_expr.h
API to expression classes for floating-point arithmetic.
goto_check.h
Program Transformation.
goto_checkt::rw_ok_check
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok and w_ok predicates
Definition: goto_check.cpp:1764
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: bitvector_expr.h:314
goto_checkt::pointer_rel_check
void pointer_rel_check(const binary_exprt &, const guardt &)
Definition: goto_check.cpp:1127
goto_checkt::collect_allocations
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
Definition: goto_check.cpp:286
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
cprover_prefix.h
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: pointer_expr.cpp:125
local_bitvector_analysist::flagst::is_dynamic_local
bool is_dynamic_local() const
Definition: local_bitvector_analysis.h:121
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
goto_checkt::undefined_shift_check
void undefined_shift_check(const shift_exprt &, const guardt &)
Definition: goto_check.cpp:403
object_lower_bound
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:208
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:282
goto_checkt::div_by_zero_check
void div_by_zero_check(const div_exprt &, const guardt &)
Definition: goto_check.cpp:353
goto_checkt::is_in_bounds_of_some_explicit_allocation
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
Definition: goto_check.cpp:2272
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:37
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: bitvector_expr.h:278
goto_checkt::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: goto_check.cpp:83
null_object
exprt null_object(const exprt &pointer)
Definition: pointer_predicates.cpp:123
goto_checkt::error_labels
error_labelst error_labels
Definition: goto_check.cpp:275
code_typet::has_this
bool has_this() const
Definition: std_types.h:821
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:754
ieee_floatt::plus_infinity
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
flag_resett::set_flag
void set_flag(bool &flag, bool new_value)
Store the current value of flag and then set its value to new_value.
Definition: goto_check.cpp:1806
goto_programt::instructiont::return_value
const exprt & return_value() const
Get the return value of a RETURN instruction.
Definition: goto_program.h:284
config
configt config
Definition: config.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
source_locationt
Definition: source_location.h:20
configt::ansi_ct::c_standardt::C99
@ C99
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1048
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_checkt
Definition: goto_check.cpp:46
malloc_object
exprt malloc_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:42
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
has_symbol
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
Definition: find_symbols.cpp:37
goto_checkt::enable_bounds_check
bool enable_bounds_check
Definition: goto_check.cpp:254
local_bitvector_analysist::flagst::is_unknown
bool is_unknown() const
Definition: local_bitvector_analysis.h:91
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2528
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
expr_util.h
Deprecated expression utility functions.
configt::ansi_ct::c_standardt::C11
@ C11
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
shift_exprt
A base class for shift and rotate operators.
Definition: bitvector_expr.h:230
goto_programt::instructiont::is_assert
bool is_assert() const
Definition: goto_program.h:441
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:704
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2114
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
goto_checkt::goto_check
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
Definition: goto_check.cpp:1826
goto_checkt::mod_overflow_check
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
Definition: goto_check.cpp:492
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
shift_exprt::distance
exprt & distance()
Definition: bitvector_expr.h:249
local_bitvector_analysist::flagst
Definition: local_bitvector_analysis.h:50
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
goto_checkt::invalidate
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
Definition: goto_check.cpp:323
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
ieee_float.h
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
goto_checkt::enable_signed_overflow_check
bool enable_signed_overflow_check
Definition: goto_check.cpp:259
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2104
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1305
goto_checkt::assertionst
std::set< std::pair< exprt, exprt > > assertionst
Definition: goto_check.cpp:245
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
goto_checkt::add_guarded_property
void add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
Include the asserted_expr in the code conditioned by the guard.
Definition: goto_check.cpp:1499
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:431
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_checkt::integer_overflow_check
void integer_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:688
local_bitvector_analysist::flagst::is_uninitialized
bool is_uninitialized() const
Definition: local_bitvector_analysis.h:101
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:27
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
goto_checkt::conditiont::description
std::string description
Definition: goto_check.cpp:170
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
configt::cppt::cpp_standardt::CPP14
@ CPP14
config.h
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1789
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:357
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
implies_exprt
Boolean implication.
Definition: std_expr.h:1898
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
goto_checkt::error_labelst
optionst::value_listt error_labelst
Definition: goto_check.cpp:274
configt::cppt::cpp_standardt::CPP11
@ CPP11
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:876
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
exprt::operands
operandst & operands()
Definition: expr.h:96
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
index_exprt
Array index operator.
Definition: std_expr.h:1243
is_invalid_pointer_exprt
Definition: pointer_predicates.h:48
goto_programt::instructiont::is_assume
bool is_assume() const
Definition: goto_program.h:440
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
goto_checkt::mode
irep_idt mode
Definition: goto_check.cpp:283
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:577
configt::cpp
struct configt::cppt cpp
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
pointer_diff_type
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
remove_skip.h
Program Transformation.
goto_checkt::enable_pointer_overflow_check
bool enable_pointer_overflow_check
Definition: goto_check.cpp:261
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
goto_checkt::check_rec_if
void check_rec_if(const if_exprt &if_expr, guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
Definition: goto_check.cpp:1582
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:350
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
goto_checkt::assertions
assertionst assertions
Definition: goto_check.cpp:246
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:432
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:65
source_locationt::is_built_in
static bool is_built_in(const std::string &s)
Definition: source_location.cpp:16
goto_checkt::is_pointer_primitive
bool is_pointer_primitive(const exprt &expr)
Returns true if the given expression is a pointer primitive such as __CPROVER_r_ok()
Definition: goto_check.cpp:1285
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:761
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:219
array_name.h
Misc Utilities.
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:816
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:724
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:402
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2676
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
goto_checkt::conditiont::conditiont
conditiont(const exprt &_assertion, const std::string &_description)
Definition: goto_check.cpp:164
dynamic_size
exprt dynamic_size(const namespacet &ns)
Definition: pointer_predicates.cpp:66
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
goto_checkt::check_rec_arithmetic_op
void check_rec_arithmetic_op(const exprt &expr, guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
Definition: goto_check.cpp:1656
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
ieee_floatt::minus_infinity
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:203
goto_checkt::goto_checkt
goto_checkt(const namespacet &_ns, const optionst &_options)
Definition: goto_check.cpp:48
goto_checkt::conversion_check
void conversion_check(const exprt &, const guardt &)
Definition: goto_check.cpp:522
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:550
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
bitvector_expr.h
API to expression classes for bitvectors.
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
mod_exprt
Modulo.
Definition: std_expr.h:1050
c_enum_typet::members
const memberst & members() const
Definition: std_types.h:654
flag_resett::flags_to_reset
std::list< std::pair< bool *, bool > > flags_to_reset
Definition: goto_check.cpp:1823
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:430
shl_exprt
Left shift.
Definition: bitvector_expr.h:295
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
not_exprt
Boolean negation.
Definition: std_expr.h:2042
object_descriptor_exprt::offset
exprt & offset()
Definition: pointer_expr.h:59