Library OSQGetMsgProof

Require Import ucert.
Require Import OSQGetMsgPure.
Open Scope code_scope.

Lemma OSQGetMsgProof:
  forall vl p r,
    Some p = BuildPreA´ os_api OSQGetMsg (getmsg, (Tptr Tvoid, nil)) vl->
    Some r = BuildRetA´ os_api OSQGetMsg (getmsg, (Tptr Tvoid, nil)) vl->
    exists t d1 d2 s,
      os_api OSQGetMsg = Some (t, d1, d2, s) /\
      {|OSQ_spec, GetHPrio, I, r, Afalse|}|- {{p}}s {{Afalse}}.

Close Scope code_scope.