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 | |
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')
-rw-r--r-- | caml/CMparser.mly | 2 | ||||
-rw-r--r-- | caml/CMtypecheck.ml | 17 |
2 files changed, 9 insertions, 10 deletions
diff --git a/caml/CMparser.mly b/caml/CMparser.mly index 2df44fb3..d9a81874 100644 --- a/caml/CMparser.mly +++ b/caml/CMparser.mly @@ -216,6 +216,7 @@ var_declaration: stmt: expr SEMICOLON { Sexpr $1 } + | IDENT EQUAL expr SEMICOLON { Sassign($1, $3) } | IF LPAREN expr RPAREN stmts ELSE stmts { Cmconstr.ifthenelse $3 $5 $7 } | IF LPAREN expr RPAREN stmts { Cmconstr.ifthenelse $3 $5 Sskip } | LOOP stmts { Sloop($2) } @@ -241,7 +242,6 @@ stmt_list: expr: LPAREN expr RPAREN { $2 } | IDENT { Evar $1 } - | IDENT EQUAL expr { Eassign($1, $3) } | INTLIT { intconst $1 } | FLOATLIT { Eop(Ofloatconst $1, Enil) } | STRINGLIT { Eop(Oaddrsymbol($1, Int.zero), Enil) } 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 |