Merge branch 'model-proof-test' into model-proof-test-updated

vellvm · Jun 28, 2023 · ac6e445 · ac6e445
2 parents 4ee8797 + 2ea62f5
commit ac6e445
Show file tree

Hide file tree

Showing 3 changed files with 473 additions and 84 deletions.
diff --git a/src/coq/Handlers/MemoryModel.v b/src/coq/Handlers/MemoryModel.v
@@ -5791,12 +5791,10 @@ Module MemoryModelTheory (LP : LLVMParams) (MP : MemoryParams LP) (MMEP : Memory
   Lemma allocate_bytes_spec_MemPropT_no_err :
     forall (ms_init : MemState)
       dt num_elements bytes
-      (BYTES_SIZE : (sizeof_dtyp dt * num_elements)%N = N.of_nat (length bytes))
-      (NON_VOID : dt <> DTYPE_Void)
       (err_msg : string),
       ~ allocate_bytes_spec_MemPropT dt num_elements bytes ms_init (raise_error err_msg).
   Proof.
-    intros ms_init dt num_elements bytes BYTES_SIZE NON_VOID err_msg CONTRA.
+    intros ms_init dt num_elements bytes err_msg CONTRA.
 
     unfold allocate_bytes_spec_MemPropT in CONTRA.
     cbn in CONTRA.