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