Changeset 2292 for src/RTLabs


Ignore:
Timestamp:
Aug 2, 2012, 6:40:15 PM (7 years ago)
Author:
campbell
Message:

More RTLabs invariants.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

    r2288 r2292  
    3737| St_load t' addr dst _ ⇒ env_has e dst t' ∧ env_has e addr ASTptr
    3838| St_store t' addr src _ ⇒ env_has e src t' ∧ env_has e addr ASTptr
     39| St_call_id id args dst _ ⇒ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True])
     40| St_call_ptr fnptr args dst _ ⇒ env_has e fnptr ASTptr ∧ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True])
     41| St_cond r _ _ ⇒ ∃t. env_has e r t
    3942| _ ⇒ True
    4043].
Note: See TracChangeset for help on using the changeset viewer.