summaryrefslogtreecommitdiff
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-12-29 16:55:38 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-12-29 16:55:38 +0000
commit8539759095f95f2fbb680efc7633d868099114c8 (patch)
tree3401d7cd91686026090a21f600cf70ea4372ebf3 /cfrontend/C2C.ml
parent7e9c6fc9a51adc5e488c590d83c1e8ef5a256c9f (diff)
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
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index aa9eca0..d425693 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -752,7 +752,7 @@ let string_of_errmsg msg =
let string_of_err = function
| Errors.MSG s -> camlstring_of_coqstring s
| Errors.CTX i -> extern_atom i
- | Errors.CTXL i -> "" (* should not happen *)
+ | Errors.POS i -> sprintf "%ld" (camlint_of_positive i)
in String.concat "" (List.map string_of_err msg)
let rec convertInit env init =