analyze: treat 0 as *const _ like ptr::null() in dataflow

immunant · Apr 12, 2024 · e95e9e9 · e95e9e9
1 parent 787919a
commit e95e9e9
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
@@ -123,6 +123,9 @@ impl<'tcx> TypeChecker<'tcx, '_> {
                 if !op.constant().copied().map(is_null_const).unwrap_or(false) {
                     panic!("Creating non-null pointers from exposed addresses not supported");
                 }
+                // The target type of the cast must not have `NON_NULL` permission.
+                self.constraints
+                    .add_no_perms(to_lty.label, PermissionSet::NON_NULL);
             }
             CastKind::PointerExposeAddress => {
                 // Allow, as [`CastKind::PointerFromExposedAddress`] is the dangerous one,

diff --git a/c2rust-analyze/tests/filecheck/non_null.rs b/c2rust-analyze/tests/filecheck/non_null.rs
@@ -32,3 +32,15 @@ fn h(cond: bool) {
         ptr::null()
     };
 }
+
+
+// Like `f`, but uses `0 as *const _` instead of `ptr::null()`.
+// CHECK-LABEL: final labeling for "f_zero"
+fn f_zero(cond: bool) {
+    let x = 1_i32;
+    // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = UNIQUE#
+    let mut y = ptr::addr_of!(x);
+    if cond {
+        y = 0 as *const _;
+    }
+}