From 578cc2a54897e0c89425a56df7a173bebeee2382 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 5 Jan 2013 09:59:26 +0000 Subject: 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 --- exportclight/Clightdefs.v | 53 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 exportclight/Clightdefs.v (limited to 'exportclight/Clightdefs.v') diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v new file mode 100644 index 0000000..4c3c942 --- /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. -- cgit v1.2.3