From 6f5eec9f5f1ad4567186172a4519e598af801b94 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 23 Apr 2018 10:47:10 +0200 Subject: Record value of constant expression in C.Scase constructor The Elab pass checks that the argument of 'case' is a compile-time constant expression. This commit records the value of this expression in the C.Scase AST generated by Elab, so that it can be used for further diagnostics, i.e. checking (in Elab) for duplicate cases. Note that C2C ignores the recorded value and recomputes the value of the expression using Ceval.integer_expr. This is intentional: Ceval.integer_expr is more trustworthy, as it is formally verified against the CompCert C semantics. --- cparser/Cprint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser/Cprint.ml') diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index c2253c8f..9aeec421 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -478,7 +478,7 @@ let rec stmt pp s = and slabel pp = function | Slabel s -> fprintf pp "%s" s - | Scase e -> + | Scase(e, _) -> fprintf pp "case %a" exp (0, e) | Sdefault -> fprintf pp "default" -- cgit