fx

Author: Daniel Kroening

src/analyses/goto_check.cpp

@@ -113,7 +113,8 @@ class goto_checkt
     const exprt &access_ub);
   conditionst address_check(
     const exprt &address,
-    const exprt &size);
+    const exprt &access_lb,
+    const exprt &access_ub);
   void integer_overflow_check(const exprt &expr, const guardt &guard);
   void conversion_check(const exprt &expr, const guardt &guard);
   void float_overflow_check(const exprt &expr, const guardt &guard);
@@ -1098,7 +1099,8 @@ void goto_checkt::pointer_validity_check(
 
 goto_checkt::conditionst goto_checkt::address_check(
   const exprt &address,
-  const exprt &size)
+  const exprt &access_lb,
+  const exprt &access_ub)
 {
   if(!enable_pointer_check)
     return {};
@@ -1130,7 +1132,6 @@ goto_checkt::conditionst goto_checkt::address_check(
     {
       typecast_exprt int_ptr(address, a.first.type());
 
-    #if 0
       exprt lb(int_ptr);
       if(access_lb.is_not_nil())
       {
@@ -1155,7 +1156,6 @@ goto_checkt::conditionst goto_checkt::address_check(
         ub, ID_le, plus_exprt(a.first, a.second));
 
       alloc_disjuncts.push_back(and_exprt(lb_check, ub_check));
-    #endif
     }
 
     const exprt allocs=disjunction(alloc_disjuncts);
@@ -1187,42 +1187,30 @@ goto_checkt::conditionst goto_checkt::address_check(
 
     if(flags.is_unknown() || flags.is_dynamic_heap())
     {
-      #if 0
       const or_exprt dynamic_bounds(
         dynamic_object_lower_bound(address, ns, access_lb),
         dynamic_object_upper_bound(address, dereference_type, ns, access_ub));
 
-      add_guarded_claim(
+      conditions.push_back(conditiont(
         or_exprt(
           allocs,
           implies_exprt(
             malloc_object(address, ns),
             not_exprt(dynamic_bounds))),
-        "dereference failure: pointer outside dynamic object bounds",
-        "pointer dereference",
-        expr.find_source_location(),
-        expr,
-        guard);
-      #endif
+        "pointer outside dynamic object bounds"));
     }
 
     if(flags.is_unknown() ||
        flags.is_dynamic_local() ||
        flags.is_static_lifetime())
     {
-      #if 0
       const or_exprt object_bounds(
         object_lower_bound(address, ns, access_lb),
         object_upper_bound(address, dereference_type, ns, access_ub));
 
-      add_guarded_claim(
+      conditions.push_back(conditiont(
         or_exprt(allocs, dynamic_object(address), not_exprt(object_bounds)),
-        "dereference failure: pointer outside object bounds",
-        "pointer dereference",
-        expr.find_source_location(),
-        expr,
-        guard);
-      #endif
+        "dereference failure: pointer outside object bounds"));
     }
 
     return conditions;
@@ -1659,7 +1647,7 @@ void goto_checkt::rw_ok_check(exprt &expr)
     DATA_INVARIANT(expr.operands().size()==2,
                    "r/w_ok must have two operands");
 
-    const auto conditions=address_check(expr.op0(), expr.op1());
+    const auto conditions=address_check(expr.op0(), nil_exprt(), expr.op1());
     exprt::operandst conjuncts;
     for(const auto &c : conditions)
       conjuncts.push_back(c.assertion);