diff --git a/c2rust-analyze/tests/filecheck.rs b/c2rust-analyze/tests/filecheck.rs index 849f602d6a..d228c8c0f6 100644 --- a/c2rust-analyze/tests/filecheck.rs +++ b/c2rust-analyze/tests/filecheck.rs @@ -55,6 +55,7 @@ define_tests! { insertion_sort_driver, insertion_sort_rewrites, known_fn, + non_null, offset1, offset2, pointee, diff --git a/c2rust-analyze/tests/filecheck/non_null.rs b/c2rust-analyze/tests/filecheck/non_null.rs new file mode 100644 index 0000000000..c05fbdc11e --- /dev/null +++ b/c2rust-analyze/tests/filecheck/non_null.rs @@ -0,0 +1,34 @@ +use std::ptr; + +// CHECK-LABEL: final labeling for "f" +fn f(cond: bool) { + let x = 1_i32; + // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = UNIQUE# + let mut y = ptr::addr_of!(x); + if cond { + y = ptr::null(); + } +} + +// CHECK-LABEL: final labeling for "g" +fn g(cond: bool) { + let x = 1_i32; + // CHECK: ([[@LINE+1]]: y): {{.*}}, type = UNIQUE | NON_NULL# + let y = ptr::addr_of!(x); + if cond { + let z = ptr::null::(); + } +} + +// CHECK-LABEL: final labeling for "h" +fn h(cond: bool) { + let x = 1_i32; + // CHECK: ([[@LINE+1]]: y): {{.*}}, type = UNIQUE | NON_NULL# + let y = ptr::addr_of!(x); + // CHECK: ([[@LINE+1]]: z): {{.*}}, type = UNIQUE# + let z = if cond { + y + } else { + ptr::null() + }; +}