X_ok(ς, p) --> p!=0

Author: kroening

regression/cprover/cstrings/cstring_is_not_null.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 cstring_is_not_null.c
 
 ^EXIT=0$

regression/cprover/safety/r_ok4.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 r_ok4.c
 
 ^EXIT=0$

src/cprover/axioms.cpp

@@ -209,26 +209,36 @@ void axiomst::node(const exprt &src, decision_proceduret &dest)
     const auto &pointer = ok_expr.op1();
     const auto &size = ok_expr.op2();
 
-    // X_ok(p, s)
-    //  --> live_object(p) ∧ offset(p)≥0 ∧ offset(p)+s≤object_size(p)
-    auto live_object =
-      binary_predicate_exprt(state, ID_state_live_object, pointer);
-    auto ssize_type = signed_size_type();
-    auto offset = pointer_offset_exprt(pointer, ssize_type);
-    auto offset_simplified =
-      simplify_state_expr_node(offset, address_taken, ns);
-    auto lower = binary_relation_exprt(
-      offset_simplified, ID_ge, from_integer(0, ssize_type));
-    auto object_size =
-      binary_exprt(state, ID_state_object_size, pointer, ssize_type);
-    auto size_casted = typecast_exprt::conditional_cast(size, ssize_type);
-    auto upper = binary_relation_exprt(
-      plus_exprt(offset_simplified, size_casted), ID_le, object_size);
-
-    auto instance =
-      replace(implies_exprt(src, and_exprt(live_object, lower, upper)));
-    std::cout << "AXIOMd: " << format(instance) << "\n";
-    dest << instance;
+    {
+      // X_ok(p, s)
+      //  --> live_object(p) ∧ offset(p)≥0 ∧ offset(p)+s≤object_size(p)
+      auto live_object =
+        binary_predicate_exprt(state, ID_state_live_object, pointer);
+      auto ssize_type = signed_size_type();
+      auto offset = pointer_offset_exprt(pointer, ssize_type);
+      auto offset_simplified =
+        simplify_state_expr_node(offset, address_taken, ns);
+      auto lower = binary_relation_exprt(
+        offset_simplified, ID_ge, from_integer(0, ssize_type));
+      auto object_size =
+        binary_exprt(state, ID_state_object_size, pointer, ssize_type);
+      auto size_casted = typecast_exprt::conditional_cast(size, ssize_type);
+      auto upper = binary_relation_exprt(
+        plus_exprt(offset_simplified, size_casted), ID_le, object_size);
+
+      auto instance =
+        replace(implies_exprt(src, and_exprt(live_object, lower, upper)));
+      std::cout << "AXIOMd: " << format(instance) << "\n";
+      dest << instance;
+    }
+
+    {
+      // X_ok(ς, p) --> p!=0
+      auto instance =
+        replace(implies_exprt(src, not_exprt(null_pointer(pointer))));
+      std::cout << "AXIOMe: " << format(instance) << "\n";
+      dest << instance;
+    }
   }
 }