Module Cabs

Require Import BinPos.

Parameter string : Type.
Parameter char_code : Type.
Parameter cabsloc : Type.

Record floatInfo := {
  isHex_FI:bool;
  integer_FI:option string;
  fraction_FI:option string;
  exponent_FI:option string;
  suffix_FI:option string
}.

Inductive structOrUnion :=
  | STRUCT | UNION.

Inductive typeSpecifier :=
  | Tvoid
  | Tchar
  | Tshort
  | Tint
  | Tlong
  | Tfloat
  | Tdouble
  | Tsigned
  | Tunsigned
  | T_Bool
  | Tnamed : string -> typeSpecifier
  | Tstruct_union : structOrUnion -> option string -> option (list field_group) -> list attribute -> typeSpecifier
  | Tenum : option string -> option (list (string * option expression * cabsloc)) -> list attribute -> typeSpecifier

with storage :=
  AUTO | STATIC | EXTERN | REGISTER | TYPEDEF

with cvspec :=
| CV_CONST | CV_VOLATILE | CV_RESTRICT
| CV_ATTR : attribute -> cvspec

with funspec :=
 INLINE | NORETURN

with spec_elem :=
  | SpecCV : cvspec -> spec_elem
  | SpecStorage : storage -> spec_elem
  | SpecFunction: funspec -> spec_elem
  | SpecType : typeSpecifier -> spec_elem

with decl_type :=
 | JUSTBASE
 | ARRAY : decl_type -> list cvspec -> option expression -> decl_type
 | PTR : list cvspec -> decl_type -> decl_type
 | PROTO : decl_type -> list parameter * bool -> decl_type
 | PROTO_OLD : decl_type -> list string -> decl_type

with parameter :=
  | PARAM : list spec_elem -> option string -> decl_type -> list attribute -> cabsloc -> parameter

with field_group :=
  | Field_group : list spec_elem -> list (option name * option expression) -> cabsloc -> field_group

with name :=
  | Name : string -> decl_type -> list attribute -> cabsloc -> name

with init_name :=
  | Init_name : name -> init_expression -> init_name

with binary_operator :=
  | ADD | SUB | MUL | DIV | MOD
  | AND | OR
  | BAND | BOR | XOR | SHL | SHR
  | EQ | NE | LT | GT | LE | GE
  | ASSIGN
  | ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
  | BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
  | COMMA

with unary_operator :=
  | MINUS | PLUS | NOT | BNOT | MEMOF | ADDROF
  | PREINCR | PREDECR | POSINCR | POSDECR

with expression :=
  | UNARY : unary_operator -> expression -> expression
  | BINARY : binary_operator -> expression -> expression -> expression
  | QUESTION : expression -> expression -> expression -> expression

  | CAST : (list spec_elem * decl_type) -> init_expression -> expression

  | CALL : expression -> list expression -> expression
  | BUILTIN_VA_ARG : expression -> list spec_elem * decl_type -> expression
  | CONSTANT : constant -> expression
  | VARIABLE : string -> expression
  | EXPR_SIZEOF : expression -> expression
  | TYPE_SIZEOF : (list spec_elem * decl_type) -> expression
  | INDEX : expression -> expression -> expression
  | MEMBEROF : expression -> string -> expression
  | MEMBEROFPTR : expression -> string -> expression

  | EXPR_ALIGNOF : expression -> expression
  | TYPE_ALIGNOF : (list spec_elem * decl_type) -> expression
  | BUILTIN_OFFSETOF : (list spec_elem * decl_type) -> list initwhat -> expression

with constant :=
  | CONST_INT : string -> constant
  | CONST_FLOAT : floatInfo -> constant
  | CONST_CHAR : bool -> list char_code -> constant
  | CONST_STRING : bool -> list char_code -> constant

with init_expression :=
  | NO_INIT
  | SINGLE_INIT : expression -> init_expression
  | COMPOUND_INIT : list (list initwhat * init_expression) -> init_expression

with initwhat :=
  | INFIELD_INIT : string -> initwhat
  | ATINDEX_INIT : expression -> initwhat

with attribute :=
  | GCC_ATTR : list gcc_attribute -> cabsloc -> attribute
  | PACKED_ATTR : list expression -> cabsloc -> attribute
  | ALIGNAS_ATTR : list expression -> cabsloc -> attribute

with gcc_attribute :=
  | GCC_ATTR_EMPTY
  | GCC_ATTR_NOARGS : gcc_attribute_word -> gcc_attribute
  | GCC_ATTR_ARGS : gcc_attribute_word -> list expression -> gcc_attribute

with gcc_attribute_word :=
  | GCC_ATTR_IDENT : string -> gcc_attribute_word
  | GCC_ATTR_CONST
  | GCC_ATTR_PACKED.

Definition init_name_group := (list spec_elem * list init_name)%type.

Definition name_group := (list spec_elem * list name)%type.

Inductive asm_operand :=
| ASMOPERAND: option string -> bool -> list char_code -> expression -> asm_operand.

Definition asm_flag := (bool * list char_code)%type.

Inductive definition :=
 | FUNDEF : list spec_elem -> name -> list definition -> statement -> cabsloc -> definition
 | DECDEF : init_name_group -> cabsloc -> definition
 | PRAGMA : string -> cabsloc -> definition


with statement :=
 | NOP : cabsloc -> statement
 | COMPUTATION : expression -> cabsloc -> statement
 | BLOCK : list statement -> cabsloc -> statement
 | If : expression -> statement -> option statement -> cabsloc -> statement
 | WHILE : expression -> statement -> cabsloc -> statement
 | DOWHILE : expression -> statement -> cabsloc -> statement
 | FOR : option for_clause -> option expression -> option expression -> statement -> cabsloc -> statement
 | BREAK : cabsloc -> statement
 | CONTINUE : cabsloc -> statement
 | RETURN : option expression -> cabsloc -> statement
 | SWITCH : expression -> statement -> cabsloc -> statement
 | CASE : expression -> statement -> cabsloc -> statement
 | DEFAULT : statement -> cabsloc -> statement
 | LABEL : string -> statement -> cabsloc -> statement
 | GOTO : string -> cabsloc -> statement
 | ASM : list cvspec -> bool -> list char_code -> list asm_operand -> list asm_operand -> list asm_flag -> cabsloc -> statement
 | DEFINITION : definition -> statement

with for_clause :=
 | FC_EXP : expression -> for_clause
 | FC_DECL : definition -> for_clause.