Changeset 2251 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Jul 24, 2012, 7:40:21 PM (9 years ago)
Author:
campbell
Message:

Add new invariant to Cminor that return typs should be respected.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r2249 r2251  
    128128].
    129129
    130 record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (s:stmt) : Prop ≝ {
     130inductive rettyp_match : option typ → option (𝚺t.expr t) → Prop ≝
     131| rettyp_none : rettyp_match (None ?) (None ?)
     132| rettyp_some : ∀t,e. rettyp_match (Some ? t) (Some ? ❬t,e❭).
     133
     134record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (rettyp:option typ) (s:stmt) : Prop ≝ {
    131135  cm_inv_var : stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) env) s;
    132   cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s
     136  cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s;
     137  cm_inv_return : match s with [ St_return oe ⇒ rettyp_match rettyp oe
     138                               | _ ⇒ True ]
    133139}.
    134140
     
    142148     (* Ensure that variables appear in the params and vars list with the
    143149        correct typ; and that all goto labels used are declared. *)
    144 ; f_inv       : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body)) f_body
     150; f_inv       : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body) f_return) f_body
    145151}.
    146152
Note: See TracChangeset for help on using the changeset viewer.