From 8539759095f95f2fbb680efc7633d868099114c8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 29 Dec 2012 16:55:38 +0000 Subject: Merge of the clightgen branch: - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgen.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index d3b99bbd..62df254b 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -319,7 +319,7 @@ Fixpoint add_vars (map: mapping) (names: list ident) Definition find_var (map: mapping) (name: ident) : mon reg := match PTree.get name map.(map_vars) with - | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTXL name :: nil) + | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTX name :: nil) | Some r => ret r end. @@ -598,7 +598,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) error (Errors.msg "RTLgen: wrong switch") | Sreturn opt_a => match opt_a, rret with - | None, None => ret nret + | None, _ => ret nret | Some a, Some r => transl_expr map a r nret | _, _ => error (Errors.msg "RTLgen: type mismatch on return") end -- cgit