diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-18 15:52:24 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-18 15:52:24 +0000 |
| commit | 165407527b1be7df6a376791719321c788e55149 (patch) | |
| tree | 35c2eb9603f007b033fced56f21fa49fd105562f /caml/CMtypecheck.ml | |
| parent | 1346309fd03e19da52156a700d037c348f27af0d (diff) | |
| download | compcert-165407527b1be7df6a376791719321c788e55149.tar.gz compcert-165407527b1be7df6a376791719321c788e55149.zip | |
Simplification de Cminor: les affectations de variables locales ne sont
plus des expressions mais des statements (Eassign -> Sassign).
Cela simplifie les preuves et ameliore la qualite du RTL produit.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/CMtypecheck.ml')
| -rw-r--r-- | caml/CMtypecheck.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml index 4e700d7a..a926039d 100644 --- a/caml/CMtypecheck.ml +++ b/caml/CMtypecheck.ml @@ -219,15 +219,6 @@ let rec type_expr env lenv e = match e with | Evar id -> type_var env id - | Eassign(id, e1) -> - let tid = type_var env id in - let te1 = type_expr env lenv e1 in - begin try - unify tid te1 - with Error s -> - raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s)) - end; - tid | Eop(op, el) -> let tel = type_exprlist env lenv el in let (targs, tres) = type_operation op in @@ -325,6 +316,14 @@ let rec type_stmt env blk ret s = | Sskip -> () | Sexpr e -> ignore (type_expr env [] e) + | Sassign(id, e1) -> + let tid = type_var env id in + let te1 = type_expr env [] e1 in + begin try + unify tid te1 + with Error s -> + raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s)) + end | Sseq(s1, s2) -> type_stmt env blk ret s1; type_stmt env blk ret s2 |