diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-10-13 09:00:12 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-10-13 09:00:12 +0200 |
| commit | 1915258c8b2cd2e171bbce93658047a765232bc9 (patch) | |
| tree | 2f4e5d6acf77a0bc30c9816394a65f868c39a6c0 /cfrontend/Csyntax.v | |
| parent | 8d2a0c12b27e82c67acc2693ecd6f1e2fede3b88 (diff) | |
| download | compcert-kvx-1915258c8b2cd2e171bbce93658047a765232bc9.tar.gz compcert-kvx-1915258c8b2cd2e171bbce93658047a765232bc9.zip | |
Revised translation of '&&' and '||' to Clight.
The previous translation (in SimplExpr) produced references to the
same temporary variable with two different types (bool and int),
which is not nice if we want to typecheck the generated Clight.
The new translation avoids this and also gets rid of the double
cast to bool then to int. The trick is to change Eparen
(in CompCert C expressions) to take two types: the type to which the
argument must be converted, and the type with which the resulting
expression is seen.
Diffstat (limited to 'cfrontend/Csyntax.v')
| -rw-r--r-- | cfrontend/Csyntax.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index a926bc3b..fa74f11c 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -61,7 +61,7 @@ Inductive expr : Type := (**r builtin function call *) | Eloc (b: block) (ofs: int) (ty: type) (**r memory location, result of evaluating a l-value *) - | Eparen (r: expr) (ty: type) (**r marked subexpression *) + | Eparen (r: expr) (tycast: type) (ty: type) (**r marked subexpression *) with exprlist : Type := | Enil @@ -87,7 +87,8 @@ but appear during reduction. These forms are: - [Eval v] where [v] is a pointer or [Vundef]. ([Eval] of an integer or float value can occur in a source term and represents a numeric literal.) - [Eloc b ofs], which appears during reduction of l-values. -- [Eparen r], which appears during reduction of conditionals [r1 ? r2 : r3]. +- [Eparen r tycast ty], which appears during reduction of conditionals + [r1 ? r2 : r3] as well as sequential `and' / `or'. Some C expressions are derived forms. Array access [r1[r2]] is expressed as [*(r1 + r2)]. @@ -128,7 +129,7 @@ Definition typeof (a: expr) : type := | Ecomma _ _ ty => ty | Ecall _ _ ty => ty | Ebuiltin _ _ _ ty => ty - | Eparen _ ty => ty + | Eparen _ _ ty => ty end. (** ** Statements *) |