Library OSQPostProof

Require Import ucert.
Require Import OSQPostPure.
Require Import gen_lemmas.
Require Import lab.

Open Scope code_scope.



Lemma OSQPostProofPart1 : gen_OSQPostProofPart1.

Lemma OSQPostProofPart2: gen_OSQPostProofPart2.

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

Close Scope code_scope.