Changeset 2287 for src/RTLabs


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

RTLabs typing for loads and stores.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.