Library OSQCreateProof

Require Import ucert.
Require Import OSQCreatePure.
Open Scope code_scope.

Lemma OSQCreateProof:
    forall vl p r,
      Some p =
      BuildPreA´ os_api OSQCreate
                 (qcre, (Tptr os_ucos_h.OS_EVENT, Tint16 :: nil)) vl ->
      Some r =
      BuildRetA´ os_api OSQCreate
                 (qcre, (Tptr os_ucos_h.OS_EVENT, Tint16 :: nil)) vl ->
      exists t d1 d2 s,
        os_api OSQCreate = Some (t, d1, d2, s) /\
        {|OSQ_spec, GetHPrio, I, r, Afalse|}|- {{p}}s {{Afalse}}.