(* *********************************************************************)
(*                                                                     *)
(*              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 tlong := Tlong Signed noattr.
Definition tulong := Tlong 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
  | Tlong si a => Tlong 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.