From 6b7455ef21064e24dd46a0e08f41a0a77faaef06 Mon Sep 17 00:00:00 2001 From: project_18556810_bot Date: Fri, 3 Jan 2025 20:00:17 +0000 Subject: [PATCH] [github pages] BRiCk documentation created from 43759fa8 --- .../bedrock.lang.cpp.logic.new_delete.html | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.new_delete.html b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.new_delete.html index a29e1d03..f4d9018e 100644 --- a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.new_delete.html +++ b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.new_delete.html @@ -304,7 +304,7 @@

bedrock.lang.cpp.logic.new_delete


        Axiom wp_operand_new :
          forall (oinit : option Expr)
-            new_fn (pass_align : bool) new_args (_ : new_args <> nil) aty Q targs
+            new_fn (pass_align : bool) new_args aty Q targs
            (nfty := normalize_type new_fn.2)
            (_ : (args_for <$> as_function nfty) = Some targs)
            (alloc_sz alloc_al : N)
@@ -318,7 +318,7 @@

bedrock.lang.cpp.logic.new_delete

                Exists storage_ptr : ptr,
                  [| storage_val = Vptr storage_ptr |] **
                  if bool_decide (storage_ptr = nullptr) then
-                    Q (Vptr storage_ptr) free
+                    [| new_args <> nil |] ** Q (Vptr storage_ptr) free
                    (* ^^ new_args <> nil exists because the default <<operator new>>
                       is never allowed to return nullptr *)
                  else
@@ -364,7 +364,6 @@

bedrock.lang.cpp.logic.new_delete

          forall (oinit : option Expr)
            new_fn storage_expr aty Q
            (nfty := normalize_type new_fn.2)
-            (_ : type_of storage_expr = Tptr Tvoid)
            (_ : args_for <$> as_function nfty = Some ([Tsize_t; Tptr Tvoid], Ar_Definite)),
            (Exists alloc_sz alloc_al,
               [| size_of aty = Some alloc_sz |] **
@@ -420,7 +419,6 @@

bedrock.lang.cpp.logic.new_delete

        Axiom wp_operand_array_new :
          forall (array_size : Expr) (oinit : option Expr)
            new_fn (pass_align : bool) new_args aty Q targs
-            (_ : new_args <> nil) (* prevents default new which must be able to throw *)
            (nfty := normalize_type new_fn.2)
            (_ : args_for <$> as_function nfty = Some targs),
            (* <https://eel.is/c++draft/expr.new7> @@ -473,7 +471,9 @@

bedrock.lang.cpp.logic.new_delete

                     Exists (storage_base : ptr),
                     res |-> primR (Tptr Tvoid) (cQp.mut 1) (Vptr storage_base) **
                     if bool_decide (storage_base = nullptr) then
-                       Q (Vptr storage_base) free
+                       [| new_args <> nil |] ** Q (Vptr storage_base) free
+                       (* ^^ new_args <> nil exists because the default <<operator new>>
+                          is never allowed to return nullptr *)
                     else
                       (* blockR alloc_sz -|- tblockR (Tarray aty array_size) *)
                      storage_base |-> blockR (overhead_sz + alloc_sz) (cQp.m 1) **