Changeset 2287


Ignore:
Timestamp:
Aug 2, 2012, 5:04:35 PM (7 years ago)
Author:
campbell
Message:

RTLabs typing for loads and stores.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2253 r2287  
    368368| 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
    369369| 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
     370| 6,7: #t' #r1 #r2 #l * /3/
    370371| *: //
    371372] qed.
     
    563564[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
    564565| #l @(pi2 … dst)
    565 | 3,8,9: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     566| 3,8,10: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    566567| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
    567568| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
    568569| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
    569570| #l % [ % [ @(fn_con_env … (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
     571| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
    570572| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
    571573| @(π1 (π1 Env))
     
    787789| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
    788790| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
     791| #l % [ @(fn_con_env … (pi2 ?? val_reg)) | @(pi2 ?? addr_reg) ] repeat @fn_contains_step @I
    789792| @sym_eq @(All2_length … (pi2 ?? args_regs))
    790793| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
  • src/RTLabs/syntax.ma

    r1878 r2287  
    3636| St_op1 t' t _ r' r _ ⇒ env_has e r' t' ∧ env_has e r t
    3737| St_op2 t' t1 t2 _ r' r1 r2 _ ⇒ env_has e r1 t1 ∧ env_has e r2 t2 ∧ env_has e r' t'
     38| St_load t' addr dst _ ⇒ env_has e dst t' ∧ env_has e addr ASTptr
     39| St_store t' addr src _ ⇒ env_has e src t' ∧ env_has e addr ASTptr
    3840| _ ⇒ True
    3941].
Note: See TracChangeset for help on using the changeset viewer.