CFEM.verif_alloc

From VST.floyd Require Import proofauto VSU.
From CFEM Require Import alloc spec_alloc.
Require Import VSTlib.spec_math VSTlib.spec_malloc.
Require Import Coq.Classes.RelationClasses.


Open Scope logic.

Require VST.floyd.library.

Parameter body_exit:
 ∀ {Espec: OracleKind},
  VST.floyd.library.body_lemma_of_funspec
    (EF_external "exit" (mksignature [Xint] Xvoid cc_default))
    (snd (exit_spec)).

Definition alloc_E : funspecs := [exit_spec].
Definition alloc_imported_specs : funspecs := MallocASI.
Definition alloc_internal_specs : funspecs := allocASI.
Definition Gprog := alloc_imported_specs ++ alloc_internal_specs.

Lemma body_surely_malloc: semax_body Vprog Gprog f_surely_malloc surely_malloc_spec'.

Lemma body_double_calloc: semax_body Vprog Gprog f_double_calloc double_calloc_spec.

Lemma body_int_calloc: semax_body Vprog Gprog f_int_calloc int_calloc_spec.

Lemma body_double_clear: semax_body Vprog Gprog f_double_clear double_clear_spec.

Definition allocVSU: @VSU NullExtension.Espec
         alloc_E alloc_imported_specs ltac:(QPprog prog) allocASI (fun gv ⇒ emp).