Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r891 r961  
    158158lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
    159159exec_from ge s (se_interact o k i (se_stop tr r m)) →
    160 step ge s tr (Returnstate (Vint r) Kstop m).
     160step ge s tr (Returnstate (Vint I32 r) Kstop m).
    161161#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
    162162[ #tr #r #m #E1 #E2 destruct
     
    278278lemma final_step: ∀ge,tr,r,m,s.
    279279  exec_from ge s (se_stop tr r m) →
    280   step ge s tr (Returnstate (Vint r) Kstop m).
     280  step ge s tr (Returnstate (Vint I32 r) Kstop m).
    281281#ge #tr #r #m #s #EXEC
    282282whd in EXEC;
     
    302302lemma e_stop_inv: ∀ge,x,tr,r,m.
    303303  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r m →
    304   x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
     304  x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop m〉.
    305305#ge #x #tr #r #m
    306306>(exec_inf_aux_unfold …) cases x;
     
    317317  execution_terminates tr s (se_step E0 s e) r m →
    318318  exec_from ge s e →
    319   star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
     319  star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m).
    320320#ge #tr0 #s0 #r #m #e0 #H inversion H;
    321321[ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC
Note: See TracChangeset for help on using the changeset viewer.