diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-05 09:59:26 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-05 09:59:26 +0000 |
commit | 578cc2a54897e0c89425a56df7a173bebeee2382 (patch) | |
tree | 1ccb034fd4beebe618d4fad81abc5214677d8010 /exportclight/Clightdefs.v | |
parent | ba8ad207029d3121d602a23aeeedd55b4dfd192a (diff) | |
download | compcert-578cc2a54897e0c89425a56df7a173bebeee2382.tar.gz compcert-578cc2a54897e0c89425a56df7a173bebeee2382.zip |
Put clighgen files in exportclight/
Short doc in exportclight/README
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'exportclight/Clightdefs.v')
-rw-r--r-- | exportclight/Clightdefs.v | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v new file mode 100644 index 00000000..4c3c942a --- /dev/null +++ b/exportclight/Clightdefs.v @@ -0,0 +1,53 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** All imports and definitions used by .v Clight files generated by clightgen *) + +Require Export List. +Require Export ZArith. +Require Export Integers. +Require Export Floats. +Require Export AST. +Require Export Ctypes. +Require Export Cop. +Require Export Clight. + +Definition tvoid := Tvoid. +Definition tschar := Tint I8 Signed noattr. +Definition tuchar := Tint I8 Unsigned noattr. +Definition tshort := Tint I16 Signed noattr. +Definition tushort := Tint I16 Unsigned noattr. +Definition tint := Tint I32 Signed noattr. +Definition tuint := Tint I32 Unsigned noattr. +Definition tbool := Tint IBool Unsigned noattr. +Definition tfloat := Tfloat F32 noattr. +Definition tdouble := Tfloat F64 noattr. +Definition tptr (t: type) := Tpointer t noattr. +Definition tarray (t: type) (sz: Z) := Tarray t sz noattr. + +Definition volatile_attr := {| attr_volatile := true |}. + +Definition tvolatile (ty: type) := + match ty with + | Tvoid => Tvoid + | Tint sz si a => Tint sz si volatile_attr + | Tfloat sz a => Tfloat sz volatile_attr + | Tpointer elt a => Tpointer elt volatile_attr + | Tarray elt sz a => Tarray elt sz volatile_attr + | Tfunction args res => Tfunction args res + | Tstruct id fld a => Tstruct id fld volatile_attr + | Tunion id fld a => Tunion id fld volatile_attr + | Tcomp_ptr id a => Tcomp_ptr id volatile_attr + end. |