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 /cparser/Cprint.ml | |
| 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.
Diffstat (limited to 'cparser/Cprint.ml')
| -rw-r--r-- | cparser/Cprint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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" |