Merge tag 'upstream/0.1'

[pkg-cerco/acc-trusted.git] / cparser / Cabshelper.ml

diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml
new file mode 100644 (file)
index 0000000..2dc1a91
--- /dev/null
+++ b/cparser/Cabshelper.ml
@@ -0,0 +1,126 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+
+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;
+              ident = 0}
+
+(*********** HELPER FUNCTIONS **********)
+
+let missingFieldDecl = ("___missing_field_name", JUSTBASE, [], cabslu)
+
+let rec isStatic = function
+    [] -> false
+  | (SpecStorage STATIC) :: _ -> true
+  | _ :: rest -> isStatic rest
+
+let rec isExtern = function
+    [] -> false
+  | (SpecStorage EXTERN) :: _ -> true
+  | _ :: rest -> isExtern rest
+
+let rec isInline = function
+    [] -> false
+  | SpecInline :: _ -> true
+  | _ :: rest -> isInline rest
+
+let rec isTypedef = function
+    [] -> false
+  | SpecTypedef :: _ -> true
+  | _ :: rest -> isTypedef rest
+
+
+let get_definitionloc (d : definition) : cabsloc =
+  match d with
+  | 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
+  match s with
+  | NOP(loc) -> loc
+  | COMPUTATION(_,loc) -> loc
+  | BLOCK(_,loc) -> loc
+(*  | SEQUENCE(_,_,loc) -> loc *)
+  | IF(_,_,_,loc) -> loc
+  | WHILE(_,_,loc) -> loc
+  | DOWHILE(_,_,loc) -> loc
+  | FOR(_,_,_,_,loc) -> loc
+  | BREAK(loc) -> loc
+  | CONTINUE(loc) -> loc
+  | 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
+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
+
+let format_cabsloc pp l =
+  Format.fprintf pp "%s:%d" l.filename l.lineno