Module Clightdefs


All imports and definitions used by .v Clight files generated by clightgen

From Coq Require Import String List ZArith.
From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop 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; attr_alignas := None |}.

Definition tattr (a: attr) (ty: type) :=
  match ty with
  | Tvoid => Tvoid
  | Tint sz si _ => Tint sz si a
  | Tlong si _ => Tlong si a
  | Tfloat sz _ => Tfloat sz a
  | Tpointer elt _ => Tpointer elt a
  | Tarray elt sz _ => Tarray elt sz a
  | Tfunction args res cc => Tfunction args res cc
  | Tstruct id _ => Tstruct id a
  | Tunion id _ => Tunion id a
  end.

Definition tvolatile (ty: type) := tattr volatile_attr ty.

Definition talignas (n: N) (ty: type) :=
  tattr {| attr_volatile := false; attr_alignas := Some n |} ty.

Definition tvolatile_alignas (n: N) (ty: type) :=
  tattr {| attr_volatile := true; attr_alignas := Some n |} ty.

Definition wf_composites (types: list composite_definition) : Prop :=
  match build_composite_env types with OK _ => True | Error _ => False end.

Definition build_composite_env' (types: list composite_definition)
                                (WF: wf_composites types)
                             : { ce | build_composite_env types = OK ce }.
Proof.
  revert WF. unfold wf_composites. case (build_composite_env types); intros.
- exists c; reflexivity.
- contradiction.
Defined.

Definition mkprogram (types: list composite_definition)
                     (defs: list (ident * globdef fundef type))
                     (public: list ident)
                     (main: ident)
                     (WF: wf_composites types) : Clight.program :=
  let (ce, EQ) := build_composite_env' types WF in
  {| prog_defs := defs;
     prog_public := public;
     prog_main := main;
     prog_types := types;
     prog_comp_env := ce;
     prog_comp_env_eq := EQ |}.