Library OSTimeGetProof

INT32U OSTimeGet (void) { 1 OS_ENTER_CRITICAL(); 2 ticks = OSTime; 3 OS_EXIT_CRITICAL(); 4 return (ticks); }

Require Import ucert.

Open Scope code_scope.

Lemma OSTimeGetRight:
  forall r p ,
    Some r = BuildRetA´ os_api OSTimeGet tmgetapi nil ->
    Some p = BuildPreA´ os_api OSTimeGet tmgetapi nil ->
    exists t decl1 decl2 s,
      os_api OSTimeGet = Some (t,decl1,decl2,s) /\
      {|OSQ_spec , GetHPrio , I , r , Afalse |} |- {{p }} s {{Afalse }}.

Lemma OSTimeGetRight´:
  forall r p ,
    Some r = BuildRetA´ os_api OSTimeGet tmgetapi nil ->
    Some p = BuildPreA´ os_api OSTimeGet tmgetapi nil ->
    exists t decl1 decl2 s,
      os_api OSTimeGet = Some (t,decl1,decl2,s) /\
      {|OSQ_spec , GetHPrio , I , r , Afalse |} |- {{p }} s {{Afalse }}.

Close Scope code_scope.