diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-04-23 10:47:10 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-04-27 13:54:38 +0200 |
| commit | 6f5eec9f5f1ad4567186172a4519e598af801b94 (patch) | |
| tree | cf7a8249630fc2d130939c076598eef482851f7e | |
| parent | 2f9932b8c5ff116d417c1e5197cd8e51f8d59b5e (diff) | |
| download | compcert-kvx-6f5eec9f5f1ad4567186172a4519e598af801b94.tar.gz compcert-kvx-6f5eec9f5f1ad4567186172a4519e598af801b94.zip | |
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.
| -rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
| -rw-r--r-- | cparser/C.mli | 2 | ||||
| -rw-r--r-- | cparser/Cleanup.ml | 2 | ||||
| -rw-r--r-- | cparser/Cprint.ml | 2 | ||||
| -rw-r--r-- | cparser/Elab.ml | 10 | ||||
| -rw-r--r-- | cparser/Rename.ml | 2 |
6 files changed, 10 insertions, 10 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index e9a3ea92..5777eb96 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1005,7 +1005,7 @@ type switchbody = let rec flattenSwitch = function | {sdesc = C.Sseq(s1, s2)} -> flattenSwitch s1 @ flattenSwitch s2 - | {sdesc = C.Slabeled(C.Scase e, s1)} -> + | {sdesc = C.Slabeled(C.Scase(e, _), s1)} -> Label(Case e) :: flattenSwitch s1 | {sdesc = C.Slabeled(C.Sdefault, s1)} -> Label Default :: flattenSwitch s1 diff --git a/cparser/C.mli b/cparser/C.mli index d674afb8..cc8d4065 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -220,7 +220,7 @@ and stmt_desc = and slabel = | Slabel of string - | Scase of exp + | Scase of exp * int64 | Sdefault (** Declarations *) diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index 9568d8fe..63ac8ac1 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -93,7 +93,7 @@ let rec add_stmt s = | Scontinue -> () | Sswitch(e, s1) -> add_exp e; add_stmt s1 | Slabeled(lbl, s) -> - begin match lbl with Scase e -> add_exp e | _ -> () end; + begin match lbl with Scase(e, _) -> add_exp e | _ -> () end; add_stmt s | Sgoto lbl -> () | Sreturn None -> () 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" diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 0194a893..b8a4ebf6 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2585,13 +2585,13 @@ let rec elab_stmt env ctx s = if not ctx.ctx_in_switch then error loc "'case' statement not in switch statement"; let a',env = elab_expr ctx.ctx_vararg loc env a in - begin match Ceval.integer_expr env a' with + let n = + match Ceval.integer_expr env a' with | None -> - error loc "expression of 'case' label is not an integer constant expression" - | Some n -> () - end; + error loc "expression of 'case' label is not an integer constant expression"; 0L + | Some n -> n in let s1,env = elab_stmt env ctx s1 in - { sdesc = Slabeled(Scase a', s1); sloc = elab_loc loc },env + { sdesc = Slabeled(Scase(a', n), s1); sloc = elab_loc loc },env | DEFAULT(s1, loc) -> if not ctx.ctx_in_switch then diff --git a/cparser/Rename.ml b/cparser/Rename.ml index d63fa47d..eb31eaf0 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -188,7 +188,7 @@ and stmt_or_decl env s = (stmt env s, env) and slabel env = function - | Scase e -> Scase(exp env e) + | Scase(e, n) -> Scase(exp env e, n) | sl -> sl let fundef env f = |