diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
| commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
| tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /cfrontend/Csyntax.v | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'cfrontend/Csyntax.v')
| -rw-r--r-- | cfrontend/Csyntax.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index db059791..89d0b2bf 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -74,18 +74,18 @@ ranged over by [l] and [r], respectively, in the grammar above. L-values are those expressions that can occur to the left of an assignment. They denote memory locations. (Indeed, the reduction semantics for expression reduces them to [Eloc b ofs] expressions.) L-values are -variables ([Evar]), pointer dereferences ([Ederef]), field accesses ([Efield]). +variables ([Evar]), pointer dereferences ([Ederef]), field accesses ([Efield]). R-values are all other expressions. They denote values, and the reduction -semantics reduces them to [Eval v] expressions. +semantics reduces them to [Eval v] expressions. A l-value can be used in a r-value context, but this use must be marked -explicitly with the [Evalof] operator, which is not materialized in the +explicitly with the [Evalof] operator, which is not materialized in the concrete syntax of C but denotes a read from the location corresponding to the l-value [l] argument of [Evalof l]. The grammar above contains some forms that cannot appear in source terms but appear during reduction. These forms are: -- [Eval v] where [v] is a pointer or [Vundef]. ([Eval] of an integer or +- [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 tycast ty], which appears during reduction of conditionals @@ -102,7 +102,7 @@ Definition Eindex (r1 r2: expr) (ty: type) := [l += 1] and [l -= 1], respectively. *) Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) := - Eassignop (match id with Incr => Oadd | Decr => Osub end) + Eassignop (match id with Incr => Oadd | Decr => Osub end) l (Eval (Vint Int.one) type_int32s) (typeconv ty) ty. (** Extract the type part of a type-annotated expression. *) |