Library OSSemAcceptProof

Require Import sem_common.
Require Import semacc_pure.


Open Scope code_scope.

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