Integration of Jacques-Henri Jourdan's verified parser.

(Merge of branch newparser.)


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

1 files changed, 4 insertions, 51 deletions

diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml
index 8f89b91..aa7a117 100644
--- a/cparser/Cabshelper.ml
+++ b/cparser/Cabshelper.ml
@@ -16,25 +16,6 @@
 
 open Cabs
 
-let nextident = ref 0
-let getident () =
-    nextident := !nextident + 1;
-    !nextident
-
-let currentLoc_lexbuf lb =
-  let p = Lexing.lexeme_start_p lb in
-  { lineno   = p.Lexing.pos_lnum;
-    filename = p.Lexing.pos_fname;
-    byteno   = p.Lexing.pos_cnum;
-    ident    = getident ();}
-
-let currentLoc () = 
-  let p = Parsing.symbol_start_pos() in
-  { lineno   = p.Lexing.pos_lnum;
-    filename = p.Lexing.pos_fname;
-    byteno   = p.Lexing.pos_cnum;
-    ident    = getident ();}
-
 let cabslu = {lineno = -10; 
 	      filename = "cabs loc unknown"; 
 	      byteno = -10;
@@ -42,8 +23,6 @@ let cabslu = {lineno = -10;
 
 (*********** HELPER FUNCTIONS **********)
 
-let missingFieldDecl = ("", JUSTBASE, [], cabslu)
-
 let rec isStatic = function
     [] -> false
   | (SpecStorage STATIC) :: _ -> true
@@ -61,19 +40,15 @@ let rec isInline = function
 
 let rec isTypedef = function
     [] -> false
-  | SpecTypedef :: _ -> true
+  | SpecStorage TYPEDEF :: _ -> true
   | _ :: rest -> isTypedef rest
 
 
 let get_definitionloc (d : definition) : cabsloc =
   match d with
-  | FUNDEF(_, _, l, _) -> l
+  | FUNDEF(_, _, _, l) -> l
   | DECDEF(_, l) -> l
-  | TYPEDEF(_, l) -> l
-  | ONLYTYPEDEF(_, l) -> l
-  | GLOBASM(_, l) -> l
   | PRAGMA(_, l) -> l
-  | LINKAGE (_, l, _) -> l
 
 let get_statementloc (s : statement) : cabsloc =
 begin
@@ -81,8 +56,7 @@ begin
   | NOP(loc) -> loc
   | COMPUTATION(_,loc) -> loc
   | BLOCK(_,loc) -> loc
-(*  | SEQUENCE(_,_,loc) -> loc *)
-  | IF(_,_,_,loc) -> loc
+  | If(_,_,_,loc) -> loc
   | WHILE(_,_,loc) -> loc
   | DOWHILE(_,_,loc) -> loc
   | FOR(_,_,_,_,loc) -> loc
@@ -91,34 +65,13 @@ begin
   | RETURN(_,loc) -> loc
   | SWITCH(_,_,loc) -> loc
   | CASE(_,_,loc) -> loc
-  | CASERANGE(_,_,_,loc) -> loc
   | DEFAULT(_,loc) -> loc
   | LABEL(_,_,loc) -> loc
   | GOTO(_,loc) -> loc
-  | COMPGOTO (_, loc) -> loc
   | DEFINITION d -> get_definitionloc d
-  | ASM(_,_,_,loc) -> loc
-  | TRY_EXCEPT(_, _, _, loc) -> loc
-  | TRY_FINALLY(_, _, loc) -> loc
+  | ASM(_,loc) -> loc
 end
 
-
-let explodeStringToInts (s: string) : int64 list =  
-  let rec allChars i acc = 
-    if i < 0 then acc
-    else allChars (i - 1) (Int64.of_int (Char.code (String.get s i)) :: acc)
-  in
-  allChars (-1 + String.length s) []
-
-let valueOfDigit chr =
-  let int_value = 
-    match chr with
-      '0'..'9' -> (Char.code chr) - (Char.code '0')
-    | 'a'..'z' -> (Char.code chr) - (Char.code 'a') + 10
-    | 'A'..'Z' -> (Char.code chr) - (Char.code 'A') + 10
-    | _ -> assert false in
-  Int64.of_int int_value
-
 let string_of_cabsloc l =
   Printf.sprintf "%s:%d" l.filename l.lineno