Changeset 881 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (9 years ago)
Author:
campbell
Message:

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r880 r881  
    1010| Op1 : ∀t,t'. unary_operation → expr t → expr t'
    1111| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
    12 | Mem : ∀t. memory_chunk → expr (ASTptr Any) → expr t
     12| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
    1313| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1414| Ecost : ∀t. costlabel → expr t → expr t.
     
    1717| St_skip : stmt
    1818| St_assign : ∀t. ident → expr t → stmt
    19 | St_store : ∀t. memory_chunk → expr (ASTptr Any) → expr t → stmt
     19| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
    2020(* ident for returned value, expression to identify fn, args. *)
    2121| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
Note: See TracChangeset for help on using the changeset viewer.