Tell Pulse that a local's address is not NULL - #230
Draft
nikswamy wants to merge 1 commit into
Draft
Conversation
A local has an address, and in C that address is never NULL. Pulse does not get that for free: the cell a local becomes is an ordinary `ref`, and `ref` includes `null`. So a callee whose contract says its out-parameter is non-null -- which is what an out-parameter annotation usually means -- was uncallable on the address of a local. The caller had to establish the non-nullness itself, at every call, for every local, even though the fact is immediate from the declaration. Say it once, at the declaration, where the cell is created. The conclusion is pure, so it stays in scope for the rest of the body and every later `&local` argument is discharged without the caller saying anything. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 0e09975)
Contributor
|
!diff |
Generated F* output diffEffect of this pull request on the F* code SummaryFull diff: full diff artifact Diffdiff --git base/addr_global/Func_addr_of_global_is_not_null.fst head/addr_global/Func_addr_of_global_is_not_null.fst
index 4673637..3f1d262 100644
--- base/addr_global/Func_addr_of_global_is_not_null.fst
+++ head/addr_global/Func_addr_of_global_is_not_null.fst
@@ -9,6 +9,7 @@ divergent fn func_addr_of_global_is_not_null ()
{
Global_g_const.acquire_var_g_const ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_g_const.addr_var_g_const;
let return_1 = (not (Pulse.Lib.Reference.is_null (!var_p)));
drop_ (exists* q. pts_to Global_g_const.addr_var_g_const #q _);
diff --git base/addr_global/Func_call_via_addr_of_global_struct.fst head/addr_global/Func_call_via_addr_of_global_struct.fst
index 3f21c5d..837342b 100644
--- base/addr_global/Func_call_via_addr_of_global_struct.fst
+++ head/addr_global/Func_call_via_addr_of_global_struct.fst
@@ -11,6 +11,7 @@ divergent fn func_call_via_addr_of_global_struct ()
Pulse.Lib.C.FuncPtr.of_fn_div_valid _ _ Funcptr_add.func_add__fp;
Global_g_ops.acquire_var_g_ops ();
let mut var_p : (ref Typedef_ops.ty_ops);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_g_ops.addr_var_g_ops;
let return_1 = ((Pulse.Lib.C.FuncPtr.call_div
_
diff --git base/addr_global/Func_read_via_addr_of_const_global.fst head/addr_global/Func_read_via_addr_of_const_global.fst
index 4a8d42f..bd3d2b0 100644
--- base/addr_global/Func_read_via_addr_of_const_global.fst
+++ head/addr_global/Func_read_via_addr_of_const_global.fst
@@ -10,6 +10,7 @@ divergent fn func_read_via_addr_of_const_global ()
{
Global_g_implicit.acquire_var_g_implicit ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_g_implicit.addr_var_g_implicit;
let return_1 = (!(!var_p));
drop_ (exists* q. pts_to Global_g_implicit.addr_var_g_implicit #q _);
diff --git base/addr_global/Func_read_via_addr_of_global.fst head/addr_global/Func_read_via_addr_of_global.fst
index 7c9339d..0d533e3 100644
--- base/addr_global/Func_read_via_addr_of_global.fst
+++ head/addr_global/Func_read_via_addr_of_global.fst
@@ -10,6 +10,7 @@ divergent fn func_read_via_addr_of_global ()
{
Global_g_const.acquire_var_g_const ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_g_const.addr_var_g_const;
let return_1 = (!(!var_p));
drop_ (exists* q. pts_to Global_g_const.addr_var_g_const #q _);
diff --git base/antiquot/Func_test_union.fst head/antiquot/Func_test_union.fst
index f8d7293..1d75c0a 100644
--- base/antiquot/Func_test_union.fst
+++ head/antiquot/Func_test_union.fst
@@ -7,6 +7,7 @@ divergent fn func_test_union ()
returns return_1 : unit
{
let mut var_x : Typedef_my_union.ty_my_union;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_x);
var_x :=
(Union_my_union_anon_1.Field_my_union_anon_1__b (id #Int64.t (Int.Cast.int32_to_int64 1l)));
assert (with_pure (not (Union_my_union_anon_1.Field_my_union_anon_1__a? (!var_x))));
diff --git base/array_ptr_arith/Func_post_decr.fst head/array_ptr_arith/Func_post_decr.fst
index fbb3433..df6c2d1 100644
--- base/array_ptr_arith/Func_post_decr.fst
+++ head/array_ptr_arith/Func_post_decr.fst
@@ -18,10 +18,13 @@ divergent fn func_post_decr (var_a: (array Typedef_int32_t.ty_int32_t))
{
let mut var_a = var_a;
let mut var_p : (array Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := ((array_to_arrayptr (!var_a) 1sz));
let mut var_q : (array Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_q);
var_q := (Pulse.Lib.C.Array.arrayptr_post_decr var_p);
let mut var_result : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_result);
if (((!var_p) `Pulse.Lib.C.Array.arrayptr_lt` (!var_q))) {
var_result := 1l;
} else {
diff --git base/array_ptr_arith/Func_post_incr.fst head/array_ptr_arith/Func_post_incr.fst
index 9618a8f..b136e87 100644
--- base/array_ptr_arith/Func_post_incr.fst
+++ head/array_ptr_arith/Func_post_incr.fst
@@ -18,10 +18,13 @@ divergent fn func_post_incr (var_a: (array Typedef_int32_t.ty_int32_t))
{
let mut var_a = var_a;
let mut var_p : (array Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := ((array_to_arrayptr (!var_a) 0sz));
let mut var_q : (array Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_q);
var_q := (Pulse.Lib.C.Array.arrayptr_post_incr var_p);
let mut var_result : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_result);
if (((!var_q) `Pulse.Lib.C.Array.arrayptr_lt` (!var_p))) {
var_result := 1l;
} else {
diff --git base/array_ptr_arith/Func_pre_decr.fst head/array_ptr_arith/Func_pre_decr.fst
index 9375913..06cc94e 100644
--- base/array_ptr_arith/Func_pre_decr.fst
+++ head/array_ptr_arith/Func_pre_decr.fst
@@ -18,10 +18,13 @@ divergent fn func_pre_decr (var_a: (array Typedef_int32_t.ty_int32_t))
{
let mut var_a = var_a;
let mut var_p : (array Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := ((array_to_arrayptr (!var_a) 1sz));
let mut var_q : (array Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_q);
var_q := (Pulse.Lib.C.Array.arrayptr_pre_decr var_p);
let mut var_result : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_result);
if (((!var_q) `Pulse.Lib.C.Array.arrayptr_eq` (!var_p))) {
var_result := 1l;
} else {
diff --git base/array_ptr_arith/Func_pre_incr.fst head/array_ptr_arith/Func_pre_incr.fst
index 4f901db..1162543 100644
--- base/array_ptr_arith/Func_pre_incr.fst
+++ head/array_ptr_arith/Func_pre_incr.fst
@@ -18,10 +18,13 @@ divergent fn func_pre_incr (var_a: (array Typedef_int32_t.ty_int32_t))
{
let mut var_a = var_a;
let mut var_p : (array Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := ((array_to_arrayptr (!var_a) 0sz));
let mut var_q : (array Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_q);
var_q := (Pulse.Lib.C.Array.arrayptr_pre_incr var_p);
let mut var_result : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_result);
if (((!var_q) `Pulse.Lib.C.Array.arrayptr_eq` (!var_p))) {
var_result := 1l;
} else {
diff --git base/array_test/Func_test_two_arrays.fst head/array_test/Func_test_two_arrays.fst
index 7a18d9e..698cb3e 100644
--- base/array_test/Func_test_two_arrays.fst
+++ head/array_test/Func_test_two_arrays.fst
@@ -7,6 +7,7 @@ divergent fn func_test_two_arrays ()
returns return_1 : unit
{
let mut var_p : Typedef_two_arrays.ty_two_arrays;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p :=
{
Struct_two_arrays_anon_1.struct_two_arrays_anon_1__x=(Pulse.Lib.C.Array.calloc_array
diff --git base/array_to_ref/Func_caller.fst head/array_to_ref/Func_caller.fst
index 25df099..e423f1a 100644
--- base/array_to_ref/Func_caller.fst
+++ head/array_to_ref/Func_caller.fst
@@ -12,6 +12,7 @@ divergent fn func_caller (var_a: (array Int32.t)) (var_i: SizeT.t)
let mut var_a = var_a;
let mut var_i = var_i;
let mut var_p : (ref Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := (array_borrow_cell (!var_a) (!var_i));
array_cell_read (!var_a) (!var_i);
(Func_write_to.func_write_to (!var_p));
diff --git base/array_to_ref/Func_caller_out.fst head/array_to_ref/Func_caller_out.fst
index b5b50f3..494de89 100644
--- base/array_to_ref/Func_caller_out.fst
+++ head/array_to_ref/Func_caller_out.fst
@@ -12,6 +12,7 @@ divergent fn func_caller_out (var_a: (array Int32.t)) (var_i: SizeT.t)
let mut var_a = var_a;
let mut var_i = var_i;
let mut var_p : (ref Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := (array_borrow_cell (!var_a) (!var_i));
Pulse.Lib.C.MaybeUninit.forget_maybe (!var_p);
(Func_init_cell.func_init_cell (!var_p));
diff --git base/array_to_ref/Func_fill_first.fst head/array_to_ref/Func_fill_first.fst
index c1735bf..3560f8f 100644
--- base/array_to_ref/Func_fill_first.fst
+++ head/array_to_ref/Func_fill_first.fst
@@ -11,6 +11,7 @@ divergent fn func_fill_first (var_a: (array Int32.t))
{
let mut var_a = var_a;
let mut var_p : (ref Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := (array_borrow_cell (!var_a) 0sz);
Pulse.Lib.C.MaybeUninit.forget_maybe (!var_p);
(Func_init_cell.func_init_cell (!var_p));
diff --git base/arrayptr_compare/Func_less.fst head/arrayptr_compare/Func_less.fst
index eb1522e..7fe40d7 100644
--- base/arrayptr_compare/Func_less.fst
+++ head/arrayptr_compare/Func_less.fst
@@ -12,8 +12,10 @@ divergent fn func_less (var_a: (array Int32.t))
{
let mut var_a = var_a;
let mut var_p : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := ((array_to_arrayptr (!var_a) 2sz));
let mut var_q : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_q);
var_q := ((array_to_arrayptr (!var_a) 5sz));
if (((!var_p) `Pulse.Lib.C.Array.arrayptr_lt` (!var_q))) {
return 1l;
diff --git base/arrayptr_diff/Func_same_object_diff.fst head/arrayptr_diff/Func_same_object_diff.fst
index c0504d1..3f0f48b 100644
--- base/arrayptr_diff/Func_same_object_diff.fst
+++ head/arrayptr_diff/Func_same_object_diff.fst
@@ -12,10 +12,13 @@ divergent fn func_same_object_diff (var_a: (array Int32.t))
{
let mut var_a = var_a;
let mut var_p : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := ((array_to_arrayptr (!var_a) 7sz));
let mut var_q : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_q);
var_q := ((array_to_arrayptr (!var_a) 2sz));
let mut var_d : Typedef_ptrdiff_t.ty_ptrdiff_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_d);
var_d := (Int64.int_to_t (Pulse.Lib.C.PtrdiffT.v ((arrayptr_diff (!var_p) (!var_q)))));
arrayptr_drop (!var_p);
arrayptr_drop (!var_q);
diff --git base/arrayptr_ref/Func_assign_cell_address_to_ref.fst head/arrayptr_ref/Func_assign_cell_address_to_ref.fst
index 1dea4a2..cce2713 100644
--- base/arrayptr_ref/Func_assign_cell_address_to_ref.fst
+++ head/arrayptr_ref/Func_assign_cell_address_to_ref.fst
@@ -15,6 +15,7 @@ divergent fn func_assign_cell_address_to_ref (var_a: (array Typedef_SUBRANGE.ty_
{
let mut var_a = var_a;
let mut var_sub : (ref Typedef_SUBRANGE.ty_subrange);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_sub);
var_sub := (array_borrow_cell (!var_a) 0sz);
Pulse.Lib.C.MaybeUninit.forget_maybe (!var_sub);
Struct_SUBRANGE_anon_1.struct_subrange_anon_1__aux_raw_unfold_uninit (!var_sub);
diff --git base/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst head/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
index 9717eb2..772b901 100644
--- base/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
+++ head/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
@@ -15,6 +15,7 @@ divergent fn func_consume_returned_arrayptr_as_ref (var_a: (array Typedef_SUBRAN
{
let mut var_a = var_a;
let mut var_sub : (ref Typedef_SUBRANGE.ty_subrange);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_sub);
var_sub := (arrayptr_borrow_cell (Func_get_uninit.func_get_uninit (!var_a)));
Pulse.Lib.C.MaybeUninit.forget_maybe (!var_sub);
Struct_SUBRANGE_anon_1.struct_subrange_anon_1__aux_raw_unfold_uninit (!var_sub);
diff --git base/arrayptr_ref/Func_pass_arrayptr_as_ref.fst head/arrayptr_ref/Func_pass_arrayptr_as_ref.fst
index 0311e53..b35f974 100644
--- base/arrayptr_ref/Func_pass_arrayptr_as_ref.fst
+++ head/arrayptr_ref/Func_pass_arrayptr_as_ref.fst
@@ -11,8 +11,10 @@ divergent fn func_pass_arrayptr_as_ref (var_a: (array Int32.t))
{
let mut var_a = var_a;
let mut var_p : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := ((array_to_arrayptr (!var_a) 1sz));
let mut var_c : (ref Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_c);
var_c := (arrayptr_borrow_cell (!var_p));
(Func_fill.func_fill (!var_c));
array_return_cell (!var_a);
diff --git base/arrayptrs/Func_binary_search.fst head/arrayptrs/Func_binary_search.fst
index 05c0b94..dd47164 100644
--- base/arrayptrs/Func_binary_search.fst
+++ head/arrayptrs/Func_binary_search.fst
@@ -29,6 +29,7 @@ pure (offset_of var_lo <= offset_of return_1 /\ offset_of return_1 < offset_of v
(old (offset_of (!var_lo)) <= offset_of (!var_lo) && offset_of (!var_hi) <= old (offset_of (!var_hi))))
{
let mut var_mid : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_mid);
var_mid :=
((arrayptr_shift
(!var_lo)
diff --git base/arrayptrs/Func_use_binary_search.fst head/arrayptrs/Func_use_binary_search.fst
index 92f6f1c..17d524f 100644
--- base/arrayptrs/Func_use_binary_search.fst
+++ head/arrayptrs/Func_use_binary_search.fst
@@ -17,16 +17,20 @@ divergent fn func_use_binary_search
let mut var_target = var_target;
let mut var_length = var_length;
let mut var_lo : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_lo);
var_lo := ((array_to_arrayptr (!var_arr) 0sz));
let mut var_hi : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_hi);
var_hi := ((array_to_arrayptr (!var_arr) (!var_length)));
let mut var_result : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_result);
var_result := (Func_binary_search.func_binary_search (!var_lo) (!var_hi) (!var_target));
if ((array_is_null (!var_result))) {
Arrayptrs_include1.elim_unless_null_null _ _;
} else {
Arrayptrs_include1.elim_unless_null_nonnull _ _;
let mut var_val : Int32.t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_val);
var_val := ((arrayptr_read (!var_result) 0sz));
};
}
\ No newline at end of file
diff --git base/arrayptrs/Func_write_via_ptr.fst head/arrayptrs/Func_write_via_ptr.fst
index 150785e..3e016fd 100644
--- base/arrayptrs/Func_write_via_ptr.fst
+++ head/arrayptrs/Func_write_via_ptr.fst
@@ -12,6 +12,7 @@ divergent fn func_write_via_ptr (var_a: (array Int32.t))
{
let mut var_a = var_a;
let mut var_p : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := ((array_to_arrayptr (!var_a) 3sz));
(arrayptr_write (!var_p) 0sz 42l);
arrayptr_drop (!var_p);
diff --git base/assign_expr/Func_chain_assign.fst head/assign_expr/Func_chain_assign.fst
index 6285a37..2dcb4ad 100644
--- base/assign_expr/Func_chain_assign.fst
+++ head/assign_expr/Func_chain_assign.fst
@@ -13,7 +13,9 @@ divergent fn func_chain_assign (var_val: Typedef_int32_t.ty_int32_t)
{
let mut var_val = var_val;
let mut var_a : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_a);
let mut var_b : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_b);
var_a := (assign_ret var_b (!var_val));
return (!var_a);
}
\ No newline at end of file
diff --git base/assign_expr/Func_compound_assign_rvalue.fst head/assign_expr/Func_compound_assign_rvalue.fst
index f0d43bc..88d735c 100644
--- base/assign_expr/Func_compound_assign_rvalue.fst
+++ head/assign_expr/Func_compound_assign_rvalue.fst
@@ -13,8 +13,10 @@ divergent fn func_compound_assign_rvalue (var_x: Typedef_int32_t.ty_int32_t)
{
let mut var_x = var_x;
let mut var_y : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_y);
var_y := (!var_x);
let mut var_z : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_z);
var_z := (assign_ret var_y ((!var_y) `Int32.add` (!var_x)));
return (!var_z);
}
\ No newline at end of file
diff --git base/assign_in_condition_dropped/Func_if_assign_pure_inlined.fst head/assign_in_condition_dropped/Func_if_assign_pure_inlined.fst
index 6fa7dc1..53e39f7 100644
--- base/assign_in_condition_dropped/Func_if_assign_pure_inlined.fst
+++ head/assign_in_condition_dropped/Func_if_assign_pure_inlined.fst
@@ -11,6 +11,7 @@ divergent fn func_if_assign_pure_inlined (var_n: Typedef_int32_t.ty_int32_t)
{
let mut var_n = var_n;
let mut var_half : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_half);
if ((not ((assign_ret var_half ((!var_n) `Int32.div` 2l)) = 0l))) {
return (!var_half);
} else {};
diff --git base/binary_ops/Func_test_chain.fst head/binary_ops/Func_test_chain.fst
index f37e13b..c65c29f 100644
--- base/binary_ops/Func_test_chain.fst
+++ head/binary_ops/Func_test_chain.fst
@@ -13,6 +13,7 @@ divergent fn func_test_chain (var_x: Typedef_int32_t.ty_int32_t)
{
let mut var_x = var_x;
let mut var_a : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_a);
var_a := (!var_x);
var_a := ((!var_a) `Int32.add` (!var_x));
var_a := ((!var_a) `Int32.add` (!var_x));
diff --git base/break_continue/Func_count_to_limit.fst head/break_continue/Func_count_to_limit.fst
index 2cee6e5..16a7b82 100644
--- base/break_continue/Func_count_to_limit.fst
+++ head/break_continue/Func_count_to_limit.fst
@@ -16,6 +16,7 @@ divergent fn func_count_to_limit
let mut var_n = var_n;
let mut var_limit = var_limit;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_i);
var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
while (((!var_i) `UInt32.lt` (!var_n)))
invariant (live var_i)
diff --git base/break_continue/Func_sum_evens.fst head/break_continue/Func_sum_evens.fst
index 3c496e0..e393e27 100644
--- base/break_continue/Func_sum_evens.fst
+++ head/break_continue/Func_sum_evens.fst
@@ -12,8 +12,10 @@ divergent fn func_sum_evens (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_i);
var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
let mut var_s : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_s);
var_s := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
while (((!var_i) `UInt32.lt` (!var_n)))
invariant ((live var_i) ** (live var_s))
diff --git base/c_assert/Func_checked_add.fst head/c_assert/Func_checked_add.fst
index 6c9356e..00ddd76 100644
--- base/c_assert/Func_checked_add.fst
+++ head/c_assert/Func_checked_add.fst
@@ -23,6 +23,7 @@ divergent fn func_checked_add
let mut var_a = var_a;
let mut var_b = var_b;
let mut var_result : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_result);
var_result := ((!var_a) `Int32.add` (!var_b));
if ((Func_pal_c_assert_enabled.func_pal_c_assert_enabled ())) {
assert (with_pure (0l `Int32.lte` (!var_result)));
diff --git base/calloc_alloc_size/Func_test_calloc_count_mul_size.fst head/calloc_alloc_size/Func_test_calloc_count_mul_size.fst
index 96c3908..ea6aeb2 100644
--- base/calloc_alloc_size/Func_test_calloc_count_mul_size.fst
+++ head/calloc_alloc_size/Func_test_calloc_count_mul_size.fst
@@ -7,6 +7,7 @@ divergent fn func_test_calloc_count_mul_size ()
returns return_1 : unit
{
let mut var_array : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_array);
var_array :=
(Pulse.Lib.C.Array.calloc_array
#Int32.t
diff --git base/calloc_alloc_size/Func_test_calloc_count_size_mul.fst head/calloc_alloc_size/Func_test_calloc_count_size_mul.fst
index 367339b..7f6c9eb 100644
--- base/calloc_alloc_size/Func_test_calloc_count_size_mul.fst
+++ head/calloc_alloc_size/Func_test_calloc_count_size_mul.fst
@@ -7,6 +7,7 @@ divergent fn func_test_calloc_count_size_mul ()
returns return_1 : unit
{
let mut var_array : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_array);
var_array :=
(Pulse.Lib.C.Array.calloc_array
#Int32.t
diff --git base/calloc_alloc_size/Func_test_calloc_var_size.fst head/calloc_alloc_size/Func_test_calloc_var_size.fst
index 9c63567..106c5e2 100644
--- base/calloc_alloc_size/Func_test_calloc_var_size.fst
+++ head/calloc_alloc_size/Func_test_calloc_var_size.fst
@@ -10,6 +10,7 @@ divergent fn func_test_calloc_var_size (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_array : (array Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_array);
var_array :=
(Pulse.Lib.C.Array.calloc_array
#Int32.t
diff --git base/character_literals/Func_classify_char.fst head/character_literals/Func_classify_char.fst
index 2cbc610..c7239fd 100644
--- base/character_literals/Func_classify_char.fst
+++ head/character_literals/Func_classify_char.fst
@@ -15,8 +15,10 @@ divergent fn func_classify_char (var_c: Typedef_int32_t.ty_int32_t)
let mut var_c = var_c;
let var___switch_scrut_0 : Typedef_int32_t.ty_int32_t = (!var_c);
let mut var___switch_hit_0 : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var___switch_hit_0);
var___switch_hit_0 := false;
let mut var___switch_brk_0 : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var___switch_brk_0);
var___switch_brk_0 := false;
if (((not (!var___switch_brk_0)) &&
((!var___switch_hit_0) || (false || (var___switch_scrut_0 = 65l))))) {
diff --git base/compare_elements/Func_compare_elems.fst head/compare_elements/Func_compare_elems.fst
index 20560d4..2480525 100644
--- base/compare_elements/Func_compare_elems.fst
+++ head/compare_elements/Func_compare_elems.fst
@@ -27,6 +27,7 @@ divergent fn func_compare_elems (var_a: (array Int32.t)) (var_b: (array Int32.t)
let mut var_b = var_b;
let mut var_len = var_len;
let mut var_i : SizeT.t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_i);
var_i := 0sz;
while (((!var_i) `SizeT.lt` (!var_len)))
invariant (live var_i)
diff --git base/compound_ops/Func_test_u16_post_incr_wrap.fst head/compound_ops/Func_test_u16_post_incr_wrap.fst
index 57eefac..cf88190 100644
--- base/compound_ops/Func_test_u16_post_incr_wrap.fst
+++ head/compound_ops/Func_test_u16_post_incr_wrap.fst
@@ -9,6 +9,7 @@ divergent fn func_test_u16_post_incr_wrap ()
ensures (with_pure ((id #int (UInt16.v return_1)) = 0))
{
let mut var_a : Typedef_uint16_t.ty_uint16_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_a);
var_a := (id #UInt16.t (Int.Cast.int32_to_uint16 65535l));
let _ = (Pulse.Lib.C.UnaryOps.pluspluspost_uint16 var_a);
return (!var_a);
diff --git base/compound_ops/Func_test_u32_pre_decr_wrap.fst head/compound_ops/Func_test_u32_pre_decr_wrap.fst
index 374f65d..e26288e 100644
--- base/compound_ops/Func_test_u32_pre_decr_wrap.fst
+++ head/compound_ops/Func_test_u32_pre_decr_wrap.fst
@@ -9,6 +9,7 @@ divergent fn func_test_u32_pre_decr_wrap ()
ensures (with_pure (return_1 = 4294967295ul))
{
let mut var_a : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_a);
var_a := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
let _ = (Pulse.Lib.C.UnaryOps.minusminuspre_uint32 var_a);
return (!var_a);
diff --git base/compound_ops/Func_test_u64_post_decr_wrap.fst head/compound_ops/Func_test_u64_post_decr_wrap.fst
index 195e076..c9c9591 100644
--- base/compound_ops/Func_test_u64_post_decr_wrap.fst
+++ head/compound_ops/Func_test_u64_post_decr_wrap.fst
@@ -9,6 +9,7 @@ divergent fn func_test_u64_post_decr_wrap ()
ensures (with_pure (return_1 = (UInt64.uint_to_t 18446744073709551615)))
{
let mut var_a : Typedef_uint64_t.ty_uint64_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_a);
var_a := (id #UInt64.t (Int.Cast.int32_to_uint64 0l));
let _ = (Pulse.Lib.C.UnaryOps.minusminuspost_uint64 var_a);
return (!var_a);
diff --git base/compound_ops/Func_test_u8_pre_incr_wrap.fst head/compound_ops/Func_test_u8_pre_incr_wrap.fst
index 24ff0d0..12accf7 100644
--- base/compound_ops/Func_test_u8_pre_incr_wrap.fst
+++ head/compound_ops/Func_test_u8_pre_incr_wrap.fst
@@ -9,6 +9,7 @@ divergent fn func_test_u8_pre_incr_wrap ()
ensures (with_pure ((id #int (UInt8.v return_1)) = 0))
{
let mut var_a : Typedef_uint8_t.ty_uint8_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_a);
var_a := (id #UInt8.t (Int.Cast.int32_to_uint8 255l));
let _ = (Pulse.Lib.C.UnaryOps.pluspluspre_uint8 var_a);
return (!var_a);
diff --git base/conditional_write/Func_caller.fst head/conditional_write/Func_caller.fst
index 020112d..3a48544 100644
--- base/conditional_write/Func_caller.fst
+++ head/conditional_write/Func_caller.fst
@@ -12,6 +12,7 @@ divergent fn func_caller (var_a: (array Int32.t)) (var_b: bool)
let mut var_a = var_a;
let mut var_b = var_b;
let mut var_p : (ref Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := (array_borrow_cell (!var_a) 0sz);
Pulse.Lib.C.MaybeUninit.forget_maybe (!var_p);
(Func_maybe_write.func_maybe_write (!var_p) (!var_b));
diff --git base/const_read/Func_call_read_val.fst head/const_read/Func_call_read_val.fst
index 1dab040..3da3400 100644
--- base/const_read/Func_call_read_val.fst
+++ head/const_read/Func_call_read_val.fst
@@ -7,8 +7,10 @@ divergent fn func_call_read_val ()
returns return_1 : Int32.t
{
let mut var_x : Int32.t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_x);
var_x := 67l;
let mut var_y : Int32.t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_y);
var_y := (Func_read_val.func_read_val var_x);
assert (with_pure (((!var_y) = (!var_x)) && ((id #int (Int32.v (!var_x))) = 67)));
return (!var_y);
diff --git base/container_field_read/Func_read_second_via_field.fst head/container_field_read/Func_read_second_via_field.fst
index 2ca6675..65db6da 100644
--- base/container_field_read/Func_read_second_via_field.fst
+++ head/container_field_read/Func_read_second_via_field.fst
@@ -23,9 +23,11 @@ Struct_pair.struct_pair__pred
{
let mut var_second = var_second;
let mut var_parent : (ref Struct_pair.struct_pair);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_parent);
var_parent := ((Struct_pair.struct_pair__second_container (!var_second)));
Container_field_read_include.expose_second (!var_second);
let mut var_s : Typedef_int32_t.ty_int32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_s);
var_s := (!(!var_second));
Container_field_read_include.hide_second (!var_second);
return (!var_s);
diff --git base/containing_record/Func_read_value_via_node.fst head/containing_record/Func_read_value_via_node.fst
index 489e72e..fd950ed 100644
--- base/containing_record/Func_read_value_via_node.fst
+++ head/containing_record/Func_read_value_via_node.fst
@@ -28,6 +28,7 @@ Struct_outer.struct_outer__pred
{
let mut var_node = var_node;
let mut var_parent : (ref Struct_outer.struct_outer);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_parent);
var_parent := ((Struct_outer.struct_outer__node_container (!var_node)));
return (!(Struct_outer.struct_outer__get_value (!var_parent)));
}
\ No newline at end of file
diff --git base/containing_record/Func_set_value_via_node.fst head/containing_record/Func_set_value_via_node.fst
index 946f6a1..86b547e 100644
--- base/containing_record/Func_set_value_via_node.fst
+++ head/containing_record/Func_set_value_via_node.fst
@@ -28,6 +28,7 @@ pure (ov.Struct_outer.struct_outer__value == var_v))
let mut var_node = var_node;
let mut var_v = var_v;
let mut var_parent : (ref Struct_outer.struct_outer);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_parent);
var_parent := ((Struct_outer.struct_outer__node_container (!var_node)));
(Struct_outer.struct_outer__get_value (!var_parent)) := (!var_v);
}
\ No newline at end of file
diff --git base/containing_record/Func_value_container_null_fires.fst head/containing_record/Func_value_container_null_fires.fst
index 2271e03..730a65b 100644
--- base/containing_record/Func_value_container_null_fires.fst
+++ head/containing_record/Func_value_container_null_fires.fst
@@ -7,8 +7,10 @@ divergent fn func_value_container_null_fires ()
returns return_1 : unit
{
let mut var_x : (ref Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_x);
var_x := null;
let mut var_y : (ref Struct_outer.struct_outer);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_y);
var_y := null;
if ((Func_pal_c_assert_enabled.func_pal_c_assert_enabled ())) {
assert
diff --git base/containing_record/Func_value_proj_null_fires.fst head/containing_record/Func_value_proj_null_fires.fst
index 16eb066..f0c039e 100644
--- base/containing_record/Func_value_proj_null_fires.fst
+++ head/containing_record/Func_value_proj_null_fires.fst
@@ -7,8 +7,10 @@ divergent fn func_value_proj_null_fires ()
returns return_1 : unit
{
let mut var_x : (ref Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_x);
var_x := null;
let mut var_y : (ref Struct_outer.struct_outer);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_y);
var_y := null;
if ((Func_pal_c_assert_enabled.func_pal_c_assert_enabled ())) {
assert
diff --git base/core_ref_chain/Func_via_local.fst head/core_ref_chain/Func_via_local.fst
index 80fc06d..e08362f 100644
--- base/core_ref_chain/Func_via_local.fst
+++ head/core_ref_chain/Func_via_local.fst
@@ -21,6 +21,7 @@ divergent fn func_via_local (var_o: Typedef_a_owned.ty_a_owned)
{
let mut var_o = var_o;
let mut var_q : (ref Struct_b.struct_b);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_q);
var_q :=
((Pulse.Lib.C.CoreRef.core_to_ref Struct_b.struct_b (!(Struct_a.struct_a__get_pb (!var_o)))));
return (!(Struct_b.struct_b__get_y (!var_q)));
diff --git base/core_ref_use/Func_store.fst head/core_ref_use/Func_store.fst
index 41eeb79..852cc02 100644
--- base/core_ref_use/Func_store.fst
+++ head/core_ref_use/Func_store.fst
@@ -16,5 +16,6 @@ divergent fn func_store (var_b: (ref Struct_bar.struct_bar))
{
let mut var_b = var_b;
let mut var_c : core_ref;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_c);
var_c := (Pulse.Lib.C.CoreRef.ref_to_core (!var_b));
}
\ No newline at end of file
diff --git base/core_ref_use/Func_via_back.fst head/core_ref_use/Func_via_back.fst
index 7942298..a034722 100644
--- base/core_ref_use/Func_via_back.fst
+++ head/core_ref_use/Func_via_back.fst
@@ -24,10 +24,12 @@ pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_bar.struct_bar
{
let mut var_p = var_p;
let mut var_b : (ref Struct_bar.struct_bar);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_b);
var_b :=
((Pulse.Lib.C.CoreRef.core_to_ref
Struct_bar.struct_bar
(!(Struct_inner.struct_inner__get_back (!var_p)))));
let mut var_o : (ref Int64.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_o);
var_o := (!(Struct_bar.struct_bar__get_other (!var_b)));
}
\ No newline at end of file
diff --git base/core_ref_use_ptr/Func_store.fst head/core_ref_use_ptr/Func_store.fst
index 41eeb79..852cc02 100644
--- base/core_ref_use_ptr/Func_store.fst
+++ head/core_ref_use_ptr/Func_store.fst
@@ -16,5 +16,6 @@ divergent fn func_store (var_b: (ref Struct_bar.struct_bar))
{
let mut var_b = var_b;
let mut var_c : core_ref;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_c);
var_c := (Pulse.Lib.C.CoreRef.ref_to_core (!var_b));
}
\ No newline at end of file
diff --git base/core_ref_use_ptr/Func_via_inner.fst head/core_ref_use_ptr/Func_via_inner.fst
index ad412ee..670229d 100644
--- base/core_ref_use_ptr/Func_via_inner.fst
+++ head/core_ref_use_ptr/Func_via_inner.fst
@@ -26,12 +26,15 @@ pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_bar.struct_bar
{
let mut var_b = var_b;
let mut var_p : (ref Struct_inner.struct_inner);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := (!(Struct_bar.struct_bar__get_myinner (!var_b)));
let mut var_b2 : (ref Struct_bar.struct_bar);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_b2);
var_b2 :=
((Pulse.Lib.C.CoreRef.core_to_ref
Struct_bar.struct_bar
(!(Struct_inner.struct_inner__get_back (!var_p)))));
let mut var_o : (ref Int64.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_o);
var_o := (!(Struct_bar.struct_bar__get_other (!var_b2)));
}
\ No newline at end of file
diff --git base/default_test/Func_test_calloc_array.fst head/default_test/Func_test_calloc_array.fst
index e704002..f6c63f4 100644
--- base/default_test/Func_test_calloc_array.fst
+++ head/default_test/Func_test_calloc_array.fst
@@ -7,6 +7,7 @@ divergent fn func_test_calloc_array ()
returns return_1 : unit
{
let mut var_array : (array Typedef_point.ty_point);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_array);
var_array :=
(Pulse.Lib.C.Array.calloc_array
#Typedef_point.ty_point
diff --git base/default_test/Func_test_calloc_ref.fst head/default_test/Func_test_calloc_ref.fst
index 24a30b1..84d292c 100644
--- base/default_test/Func_test_calloc_ref.fst
+++ head/default_test/Func_test_calloc_ref.fst
@@ -7,6 +7,7 @@ divergent fn func_test_calloc_ref ()
returns return_1 : unit
{
let mut var_p : (ref Int32.t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := (Pulse.Lib.C.Ref.calloc_ref #Int32.t ());
assert (with_pure ((id #int (Int32.v (!(!var_p)))) = 0));
(Pulse.Lib.C.Ref.free_ref (!var_p));
diff --git base/do_while/Func_count_odd.fst head/do_while/Func_count_odd.fst
index d888b93..d565365 100644
--- base/do_while/Func_count_odd.fst
+++ head/do_while/Func_count_odd.fst
@@ -12,10 +12,13 @@ divergent fn func_count_odd (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_i);
var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
let mut var_count : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_count);
var_count := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
let mut var_first : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_first);
var_first := true;
while (((!var_first) || ((!var_i) `UInt32.lt` (!var_n))))
invariant ((((live var_i) ** (live var_count)) ** (live var_n)) ** (live var_first))
diff --git base/do_while/Func_find_limit.fst head/do_while/Func_find_limit.fst
index cba1cf5..a2ba9bf 100644
--- base/do_while/Func_find_limit.fst
+++ head/do_while/Func_find_limit.fst
@@ -20,10 +20,13 @@ divergent fn func_find_limit
let mut var_n = var_n;
let mut var_limit = var_limit;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_i);
var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
let mut var___do_cont_2 : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var___do_cont_2);
var___do_cont_2 := true;
let mut var_first : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_first);
var_first := true;
while ((!var___do_cont_2))
invariant ((((live var_i) ** (live var_n)) ** (live var_limit)) ** (live var_first))
diff --git base/do_while/Func_g_loop.fst head/do_while/Func_g_loop.fst
index 3044e7b..b25f0c8 100644
--- base/do_while/Func_g_loop.fst
+++ head/do_while/Func_g_loop.fst
@@ -8,10 +8,13 @@ divergent fn func_g_loop ()
ensures (with_pure ((id #int (Int32.v return_1)) = 10))
{
let mut var_s : Struct_counter.struct_counter;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_s);
var_s := { Struct_counter.struct_counter__x=0l; };
let mut var_cont : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_cont);
var_cont := true;
let mut var_first : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_first);
var_first := true;
while ((!var_cont))
invariant (((live (Struct_counter.struct_counter__get_x var_s)) ** (live var_cont)) **
diff --git base/do_while/Func_nested_continue.fst head/do_while/Func_nested_continue.fst
index 04a0385..aeeaac9 100644
--- base/do_while/Func_nested_continue.fst
+++ head/do_while/Func_nested_continue.fst
@@ -12,10 +12,13 @@ divergent fn func_nested_continue (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_i);
var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
let mut var___do_cont_4 : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var___do_cont_4);
var___do_cont_4 := true;
let mut var_first : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_first);
var_first := true;
while ((!var___do_cont_4))
invariant (((live var_i) ** (live var_n)) ** (live var_first))
@@ -26,6 +29,7 @@ divergent fn func_nested_continue (var_n: Typedef_uint32_t.ty_uint32_t)
invariant (with_pure ((!var___do_cont_4) = ((!var_first) || ((!var_i) `UInt32.lt` (!var_n)))))
{
let mut var_j : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_j);
var_j := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
while (((!var_j) `UInt32.lt` (id #UInt32.t (Int.Cast.int32_to_uint32 3l))))
invariant (live var_j)
diff --git base/do_while/Func_run_once.fst head/do_while/Func_run_once.fst
index 3cb327b..9f17d61 100644
--- base/do_while/Func_run_once.fst
+++ head/do_while/Func_run_once.fst
@@ -12,10 +12,13 @@ divergent fn func_run_once (var_x: Typedef_uint32_t.ty_uint32_t)
{
let mut var_x = var_x;
let mut var_r : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_r);
var_r := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
let mut var___do_cont_1 : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var___do_cont_1);
var___do_cont_1 := true;
let mut var___do_first_0 : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var___do_first_0);
var___do_first_0 := true;
while ((!var___do_cont_1))
invariant (live var_r)
diff --git base/do_while/Func_simple_do.fst head/do_while/Func_simple_do.fst
index 1b37d0b..8ced99f 100644
--- base/do_while/Func_simple_do.fst
+++ head/do_while/Func_simple_do.fst
@@ -12,10 +12,13 @@ divergent fn func_simple_do (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_i);
var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
let mut var___do_cont_0 : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var___do_cont_0);
var___do_cont_0 := true;
let mut var_first : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_first);
var_first := true;
while ((!var___do_cont_0))
invariant (((live var_i) ** (live var_n)) ** (live var_first))
diff --git base/dpe/Func_authenticate_l0_image.fst head/dpe/Func_authenticate_l0_image.fst
index dc62cbe..379c365 100644
--- base/dpe/Func_authenticate_l0_image.fst
+++ head/dpe/Func_authenticate_l0_image.fst
@@ -12,6 +12,7 @@ divergent fn func_authenticate_l0_image
{
let mut var_record = var_record;
let mut var_valid_header_sig : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_valid_header_sig);
var_valid_header_sig :=
(Func_ed25519_verify.func_ed25519_verify
(!(Struct__engine_record_t.struct__engine_record_t__get_l0_image_auth_pubkey (!var_record)))
diff --git base/dpe/Func_derive_child_from_context.fst head/dpe/Func_derive_child_from_context.fst
index 81b3644..852e5b5 100644
--- base/dpe/Func_derive_child_from_context.fst
+++ head/dpe/Func_derive_child_from_context.fst
@@ -36,9 +36,11 @@ divergent fn func_derive_child_from_context
let mut var_record = var_record;
DPE_predicates.elim_context_full_pred_uds (!(!var_ctx));
let mut var_cdi_buf : (array Typedef_uint8_t.ty_uint8_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_cdi_buf);
var_cdi_buf := (Pulse.Lib.C.Array.calloc_array #Typedef_uint8_t.ty_uint8_t 64sz);
assert (with_pure ((reveal (length_of (!var_cdi_buf))) = 64));
let mut var_ok : bool;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_ok);
var_ok :=
(Func_engine_main.func_engine_main
(!var_cdi_buf)
diff --git base/dpe/Func_destroy_uds_context.fst head/dpe/Func_destroy_uds_context.fst
index 1ca70a1..dd3cddb 100644
--- base/dpe/Func_destroy_uds_context.fst
+++ head/dpe/Func_destroy_uds_context.fst
@@ -19,6 +19,7 @@ divergent fn func_destroy_uds_context (var_ctx: Typedef_context_obj.ty_context_o
let mut var_ctx = var_ctx;
DPE_predicates.elim_context_full_pred_uds (!(!var_ctx));
let mut var_uds_buf : (array Typedef_uint8_t.ty_uint8_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_uds_buf);
var_uds_buf :=
(!(Union__u_context_t.union__u_context_t__get_uds
(Struct_context_t_anon_1.struct_context_t_anon_1__get_payload (!var_ctx))));
diff --git base/dpe/Func_init_engine_context.fst head/dpe/Func_init_engine_context.fst
index e6ab3a6..02cd283 100644
--- base/dpe/Func_init_engine_context.fst
+++ head/dpe/Func_init_engine_context.fst
@@ -18,12 +18,14 @@ divergent fn func_init_engine_context (var_uds: Typedef_uds_array.ty_uds_array)
{
let mut var_uds = var_uds;
let mut var_uds_buf : (array Typedef_uint8_t.ty_uint8_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_uds_buf);
var_uds_buf :=
(Pulse.Lib.C.Array.alloc_array
#Typedef_uint8_t.ty_uint8_t
(SizeT.uint_to_t (UInt64.v (id #UInt64.t (Int.Cast.int32_to_uint64 32l)))));
(Func_memcpy_.func_memcpy_ 32sz (!var_uds) (!var_uds_buf));
let mut var_ctx : (ref Typedef_context_t.ty_context_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_ctx);
var_ctx := (Pulse.Lib.C.Ref.alloc_ref #Typedef_context_t.ty_context_t ());
(!var_ctx) :=
{
diff --git base/dpe/Func_init_l0_context.fst head/dpe/Func_init_l0_context.fst
index 0821b35..e0d6273 100644
--- base/dpe/Func_init_l0_context.fst
+++ head/dpe/Func_init_l0_context.fst
@@ -27,6 +27,7 @@ divergent fn func_init_l0_context
let mut var_ctx = var_ctx;
let mut var_cdi = var_cdi;
let mut var_cdi_buf : (array Typedef_uint8_t.ty_uint8_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_cdi_buf);
var_cdi_buf :=
(Pulse.Lib.C.Array.alloc_array
#Typedef_uint8_t.ty_uint8_t
@@ -34,6 +35,7 @@ divergent fn func_init_l0_context
(Func_memcpy_.func_memcpy_ 64sz (!var_cdi) (!var_cdi_buf));
DPE_predicates.elim_context_full_pred_uds (!(!var_ctx));
let mut var_uds_buf : (array Typedef_uint8_t.ty_uint8_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_uds_buf);
var_uds_buf :=
(!(Union__u_context_t.union__u_context_t__get_uds
(Struct_context_t_anon_1.struct_context_t_anon_1__get_payload (!var_ctx))));
diff --git base/dpe/Func_mk_l0_context.fst head/dpe/Func_mk_l0_context.fst
index d6da3dd..f396194 100644
--- base/dpe/Func_mk_l0_context.fst
+++ head/dpe/Func_mk_l0_context.fst
@@ -33,6 +33,7 @@ divergent fn func_mk_l0_context
assert (with_pure ((reveal (length_of (!var_cdi))) = 64));
DPE_predicates.elim_context_full_pred_uds (!(!var_ctx));
let mut var_uds_buf : (array Typedef_uint8_t.ty_uint8_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_uds_buf);
var_uds_buf :=
(!(Union__u_context_t.union__u_context_t__get_uds
(Struct_context_t_anon_1.struct_context_t_anon_1__get_payload (!var_ctx))));
diff --git base/duplicate_decl/Func_bar.fst head/duplicate_decl/Func_bar.fst
index b2d0889..f85ed88 100644
--- base/duplicate_decl/Func_bar.fst
+++ head/duplicate_decl/Func_bar.fst
@@ -7,6 +7,7 @@ divergent fn func_bar ()
returns return_1 : unit
{
let mut var_x : Int32.t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_x);
var_x := 1l;
return;
}
\ No newline at end of file
diff --git base/enum_constant_in_contract/Func_next_color.fst head/enum_constant_in_contract/Func_next_color.fst
index 5c3af5f..294e523 100644
--- base/enum_constant_in_contract/Func_next_color.fst
+++ head/enum_constant_in_contract/Func_next_color.fst
@@ -18,6 +18,7 @@ divergent fn func_next_color (var_c: Typedef_COLOR.ty_color)
{
let mut var_c = var_c;
let mut var_result : Typedef_COLOR.ty_color;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_result);
if (((!var_c) = (id #UInt32.t (Int.Cast.int32_to_uint32 2l)))) {
var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
} else {
diff --git base/extern_func_ptr/Func_take_addr.fst head/extern_func_ptr/Func_take_addr.fst
index cc626a0..5315640 100644
--- base/extern_func_ptr/Func_take_addr.fst
+++ head/extern_func_ptr/Func_take_addr.fst
@@ -10,6 +10,7 @@ divergent fn func_take_addr ()
(Pulse.Lib.C.FuncPtr.func_ptr
(Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)
Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_fp);
var_fp :=
((Pulse.Lib.C.FuncPtr.of_fn_div
(Pulse.Lib.C.FuncPtr.pre_of Funcptr_ext_add.func_ext_add__fp)
diff --git base/extern_func_ptr/Func_use_extern_fp.fst head/extern_func_ptr/Func_use_extern_fp.fst
index c50a0c0..72eab6d 100644
--- base/extern_func_ptr/Func_use_extern_fp.fst
+++ head/extern_func_ptr/Func_use_extern_fp.fst
@@ -12,6 +12,7 @@ divergent fn func_use_extern_fp ()
(Pulse.Lib.C.FuncPtr.func_ptr
(Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)
Typedef_int32_t.ty_int32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_fp);
var_fp :=
((Pulse.Lib.C.FuncPtr.of_fn_div
(Pulse.Lib.C.FuncPtr.pre_of Funcptr_ext_add.func_ext_add__fp)
diff --git base/extern_globals/Func_e_stable_diff.fst head/extern_globals/Func_e_stable_diff.fst
index a14c058..3b304fb 100644
--- base/extern_globals/Func_e_stable_diff.fst
+++ head/extern_globals/Func_e_stable_diff.fst
@@ -10,10 +10,13 @@ divergent fn func_e_stable_diff ()
{
Global_e_stable.acquire_var_e_stable ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_e_stable.addr_var_e_stable;
let mut var_first : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_first);
var_first := (!(!var_p));
let mut var_second : Typedef_uint32_t.ty_uint32_t;
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_second);
var_second := (!(!var_p));
let return_1 = ((!var_first) `Pulse.Lib.C.UInt32.sub_wrap` (!var_second));
drop_ (exists* q. pts_to Global_e_stable.addr_var_e_stable #q _);
diff --git base/extern_globals/Func_read_d_early_const.fst head/extern_globals/Func_read_d_early_const.fst
index a5d051f..10cd4be 100644
--- base/extern_globals/Func_read_d_early_const.fst
+++ head/extern_globals/Func_read_d_early_const.fst
@@ -10,6 +10,7 @@ divergent fn func_read_d_early_const ()
{
Global_d_early_const.acquire_var_d_early_const ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_d_early_const.addr_var_d_early_const;
let return_1 = (!(!var_p));
drop_ (exists* q. pts_to Global_d_early_const.addr_var_d_early_const #q _);
diff --git base/extern_globals/Func_read_d_early_pure.fst head/extern_globals/Func_read_d_early_pure.fst
index 6f91057..4dc3870 100644
--- base/extern_globals/Func_read_d_early_pure.fst
+++ head/extern_globals/Func_read_d_early_pure.fst
@@ -10,6 +10,7 @@ divergent fn func_read_d_early_pure ()
{
Global_d_early_pure.acquire_var_d_early_pure ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_d_early_pure.addr_var_d_early_pure;
let return_1 = (!(!var_p));
drop_ (exists* q. pts_to Global_d_early_pure.addr_var_d_early_pure #q _);
diff --git base/extern_globals/Func_read_d_late_const.fst head/extern_globals/Func_read_d_late_const.fst
index 937d9ee..c97a11a 100644
--- base/extern_globals/Func_read_d_late_const.fst
+++ head/extern_globals/Func_read_d_late_const.fst
@@ -10,6 +10,7 @@ divergent fn func_read_d_late_const ()
{
Global_d_late_const.acquire_var_d_late_const ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_d_late_const.addr_var_d_late_const;
let return_1 = (!(!var_p));
drop_ (exists* q. pts_to Global_d_late_const.addr_var_d_late_const #q _);
diff --git base/extern_globals/Func_read_e_const.fst head/extern_globals/Func_read_e_const.fst
index c33cd63..86d6a77 100644
--- base/extern_globals/Func_read_e_const.fst
+++ head/extern_globals/Func_read_e_const.fst
@@ -10,6 +10,7 @@ divergent fn func_read_e_const ()
{
Global_e_const.acquire_var_e_const ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_e_const.addr_var_e_const;
let return_1 = (!(!var_p));
drop_ (exists* q. pts_to Global_e_const.addr_var_e_const #q _);
diff --git base/extern_globals/Func_read_e_pure.fst head/extern_globals/Func_read_e_pure.fst
index 4854813..9fbc8d1 100644
--- base/extern_globals/Func_read_e_pure.fst
+++ head/extern_globals/Func_read_e_pure.fst
@@ -10,6 +10,7 @@ divergent fn func_read_e_pure ()
{
Global_e_pure.acquire_var_e_pure ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_e_pure.addr_var_e_pure;
let return_1 = (!(!var_p));
drop_ (exists* q. pts_to Global_e_pure.addr_var_e_pure #q _);
diff --git base/extern_globals/Func_read_e_pure_const.fst head/extern_globals/Func_read_e_pure_const.fst
index cc6a116..d3d0e4c 100644
--- base/extern_globals/Func_read_e_pure_const.fst
+++ head/extern_globals/Func_read_e_pure_const.fst
@@ -10,6 +10,7 @@ divergent fn func_read_e_pure_const ()
{
Global_e_pure_const.acquire_var_e_pure_const ();
let mut var_p : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_p);
var_p := Global_e_pure_const.addr_var_e_pure_const;
let return_1 = (!(!var_p));
drop_ (exists* q. pts_to Global_e_pure_const.addr_var_e_pure_const #q _);
diff --git base/extern_globals/Func_read_p_to_d_early_addressed.fst head/extern_globals/Func_read_p_to_d_early_addressed.fst
index 5296cbb..9c9845d 100644
--- base/extern_globals/Func_read_p_to_d_early_addressed.fst
+++ head/extern_globals/Func_read_p_to_d_early_addressed.fst
@@ -10,8 +10,10 @@ divergent fn func_read_p_to_d_early_addressed ()
{
Global_p_to_d_early_addressed.acquire_var_p_to_d_early_addressed ();
let mut var_pp : (ref (ref Typedef_uint32_t.ty_uint32_t));
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_pp);
var_pp := Global_p_to_d_early_addressed.addr_var_p_to_d_early_addressed;
let mut var_v : (ref Typedef_uint32_t.ty_uint32_t);
+ (Pulse.Lib.Reference.pts_to_uninit_not_null var_v);
var_v := (!(!var_pp));
drop_ (exists* q. pts_to Global_p_to_d_early_addressed.addr_var_p_to_d_early_addressed #q _);
if ((Pulse.Lib.Reference.is_null (!var_v))) {
diff --git base/extern_globals/Func_read_p_to_e_addressed.fst head/extern_globals/Func_read_p_to_e_addressed.fst
index 446d8f1..6dc3ff9 100644
--- base/extern_globals/Func_read_p_to_e_addressed.fst
+++ head/extern_globals/Func_read_p_to_e_addressed.fst
@@ -10,8 +10,10 @@ divergent fn func_read_p_to_e_addressed ()
{
Global_p_to_e_addressed.acquire_var_p_to_e_addressed ();
let mut var_pp : (ref (ref Typedef_uint32_t.ty_uint32_t));
Diff truncated; see the links above for the full version. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of the upstreaming of
nswamy/pal-c-project-integration(PR16 of 35 PRs) — seePR_PLAN.mdon that branch for the whole plan and the dependency graph.Base:
main. Depends on nothing; reviewable on its own.A local's address is never NULL in C, but the cell a local becomes is an ordinary
ref,and
refincludesnull— so a callee whose contract says its out-parameter is non-nullwas uncallable on
&localunless the caller established it at every call. Said once, atthe declaration; the conclusion is pure, so it stays in scope for the rest of the body.
Commits
Testing
Verified:
make rust lib,test/check-template.sh,cargo fmt --check,clang-format --dry-run --Werror, and F* verification oftest/local_not_null.