Switching to the new C parser/elaborator/simplifier

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 231 insertions, 0 deletions

diff --git a/cparser/C.mli b/cparser/C.mli
new file mode 100644
index 0000000..6744b38
--- /dev/null
+++ b/cparser/C.mli
@@ -0,0 +1,231 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* C abstract syntax after elaboration *)
+
+(* Locations *)
+
+type location = string * int            (* filename, line number *)
+
+(* Identifiers *)
+
+type ident =
+  { name: string;                       (* name as in the source *)
+    stamp: int }                        (* unique ID *)
+
+(* kinds of integers *)
+
+type ikind = 
+  | IBool       (** [_Bool] *)
+  | IChar       (** [char] *)
+  | ISChar      (** [signed char] *)
+  | IUChar      (** [unsigned char] *)
+  | IInt        (** [int] *)
+  | IUInt       (** [unsigned int] *)
+  | IShort      (** [short] *)
+  | IUShort     (** [unsigned short] *)
+  | ILong       (** [long] *)
+  | IULong      (** [unsigned long] *)
+  | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
+  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on Microsoft 
+                    Visual C) *)
+
+(** Kinds of floating-point numbers*)
+
+type fkind = 
+    FFloat      (** [float] *)
+  | FDouble     (** [double] *)
+  | FLongDouble (** [long double] *)
+
+
+(** Constants *)
+
+type constant =
+  | CInt of int64 * ikind * string      (* as it appeared in the source *)
+  | CFloat of float * fkind * string    (* as it appeared in the source *)
+  | CStr of string
+  | CWStr of int64 list
+  | CEnum of ident * int64              (* enum tag, integer value *)
+
+(** Attributes *)
+
+type attribute = AConst | AVolatile | ARestrict
+
+type attributes = attribute list
+
+(** Storage classes *)
+
+type storage =
+  | Storage_default
+  | Storage_extern
+  | Storage_static
+  | Storage_register
+
+(** Unary operators *)
+
+type unary_operator =
+  | Ominus	(* unary "-" *)
+  | Oplus	(* unary "+" *)
+  | Olognot	(* "!" *)
+  | Onot        (* "~" *)
+  | Oderef      (* unary "*" *)
+  | Oaddrof     (* "&" *)
+  | Opreincr    (* "++" prefix *)
+  | Opredecr    (* "--" prefix *)
+  | Opostincr   (* "++" postfix *)
+  | Opostdecr   (* "--" postfix *)
+  | Odot of string (* ".field" *)
+  | Oarrow of string (* "->field" *)
+
+type binary_operator =
+  | Oadd        (* binary "+" *)
+  | Osub        (* binary "-" *)
+  | Omul        (* binary "*" *)
+  | Odiv        (* "/" *)
+  | Omod        (* "%" *)
+  | Oand        (* "&" *)
+  | Oor         (* "|" *)
+  | Oxor        (* "^" *)
+  | Oshl        (* "<<" *)
+  | Oshr        (* ">>" *)
+  | Oeq         (* "==" *)
+  | One         (* "!=" *)
+  | Olt         (* "<" *)
+  | Ogt         (* ">" *)
+  | Ole         (* "<=" *)
+  | Oge         (* ">=" *)
+  | Oindex      (* "a[i]" *)
+  | Oassign     (* "=" *)
+  | Oadd_assign (* "+=" *)
+  | Osub_assign (* "-=" *)
+  | Omul_assign (* "*=" *)
+  | Odiv_assign (* "/=" *)
+  | Omod_assign (* "%=" *)
+  | Oand_assign (* "&=" *)
+  | Oor_assign  (* "|=" *)
+  | Oxor_assign (* "^=" *)
+  | Oshl_assign (* "<<=" *)
+  | Oshr_assign (* ">>=" *)
+  | Ocomma      (* "," *)
+  | Ologand     (* "&&" *)
+  | Ologor      (* "||" *)
+
+(** Types *)
+
+type typ =
+  | TVoid of attributes
+  | TInt of ikind * attributes
+  | TFloat of fkind * attributes
+  | TPtr of typ * attributes
+  | TArray of typ * int64 option * attributes
+  | TFun of typ * (ident * typ) list option * bool * attributes
+  | TNamed of ident * attributes
+  | TStruct of ident * attributes
+  | TUnion of ident * attributes
+
+(** Expressions *)
+
+type exp = { edesc: exp_desc; etyp: typ }
+
+and exp_desc =
+  | EConst of constant
+  | ESizeof of typ
+  | EVar of ident
+  | EUnop of unary_operator * exp
+  | EBinop of binary_operator * exp * exp * typ
+                           (* the type at which the operation is performed *)
+  | EConditional of exp * exp * exp
+  | ECast of typ * exp
+  | ECall of exp * exp list
+
+(** Statements *)
+
+type stmt = { sdesc: stmt_desc; sloc: location }
+
+and stmt_desc =
+  | Sskip
+  | Sdo of exp
+  | Sseq of stmt * stmt
+  | Sif of exp * stmt * stmt
+  | Swhile of exp * stmt
+  | Sdowhile of stmt * exp
+  | Sfor of stmt * exp * stmt * stmt
+  | Sbreak
+  | Scontinue
+  | Sswitch of exp * stmt
+  | Slabeled of slabel * stmt
+  | Sgoto of string
+  | Sreturn of exp option
+  | Sblock of stmt list
+  | Sdecl of decl
+
+and slabel = 
+  | Slabel of string
+  | Scase of exp
+  | Sdefault
+
+(** Declarations *)
+
+and decl =
+  storage * ident * typ * init option
+
+(** Initializers *)
+
+and init =
+  | Init_single of exp
+  | Init_array of init list
+  | Init_struct of ident * (field * init) list
+  | Init_union of ident * field * init
+
+(** Struct or union field *)
+
+and field = {
+    fld_name: string;
+    fld_typ: typ;
+    fld_bitfield: int option
+}
+
+type struct_or_union =
+  | Struct
+  | Union
+
+(** Function definitions *)
+
+type fundef = {
+    fd_storage: storage;
+    fd_name: ident;
+    fd_ret: typ; (* return type *)
+    fd_params: (ident * typ) list; (* formal parameters *)
+    fd_vararg: bool;               (* variable arguments? *)
+    fd_locals: decl list;          (* local variables *)
+    fd_body: stmt
+}
+
+(** Global declarations *)
+
+type globdecl =
+  { gdesc: globdecl_desc; gloc: location }
+
+and globdecl_desc =
+  | Gdecl of decl           (* variable declaration, function prototype *)
+  | Gfundef of fundef                   (* function definition *)
+  | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
+  | Gcompositedef of struct_or_union * ident * field list
+                                        (* struct/union definition *)
+  | Gtypedef of ident * typ             (* typedef *)
+  | Genumdef of ident * (ident * exp option) list  (* enum definition *)
+  | Gpragma of string                   (* #pragma directive *)
+
+type program = globdecl list