1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
21 nextident := !nextident + 1;
24 let currentLoc_lexbuf lb =
25 let p = Lexing.lexeme_start_p lb in
26 { lineno = p.Lexing.pos_lnum;
27 filename = p.Lexing.pos_fname;
28 byteno = p.Lexing.pos_cnum;
32 let p = Parsing.symbol_start_pos() in
33 { lineno = p.Lexing.pos_lnum;
34 filename = p.Lexing.pos_fname;
35 byteno = p.Lexing.pos_cnum;
38 let cabslu = {lineno = -10;
39 filename = "cabs loc unknown";
43 (*********** HELPER FUNCTIONS **********)
45 let missingFieldDecl = ("___missing_field_name", JUSTBASE, [], cabslu)
47 let rec isStatic = function
49 | (SpecStorage STATIC) :: _ -> true
50 | _ :: rest -> isStatic rest
52 let rec isExtern = function
54 | (SpecStorage EXTERN) :: _ -> true
55 | _ :: rest -> isExtern rest
57 let rec isInline = function
59 | SpecInline :: _ -> true
60 | _ :: rest -> isInline rest
62 let rec isTypedef = function
64 | SpecTypedef :: _ -> true
65 | _ :: rest -> isTypedef rest
68 let get_definitionloc (d : definition) : cabsloc =
70 | FUNDEF(_, _, l, _) -> l
73 | ONLYTYPEDEF(_, l) -> l
76 | LINKAGE (_, l, _) -> l
78 let get_statementloc (s : statement) : cabsloc =
82 | COMPUTATION(_,loc) -> loc
84 (* | SEQUENCE(_,_,loc) -> loc *)
85 | IF(_,_,_,loc) -> loc
86 | WHILE(_,_,loc) -> loc
87 | DOWHILE(_,_,loc) -> loc
88 | FOR(_,_,_,_,loc) -> loc
90 | CONTINUE(loc) -> loc
91 | RETURN(_,loc) -> loc
92 | SWITCH(_,_,loc) -> loc
93 | CASE(_,_,loc) -> loc
94 | CASERANGE(_,_,_,loc) -> loc
95 | DEFAULT(_,loc) -> loc
96 | LABEL(_,_,loc) -> loc
98 | COMPGOTO (_, loc) -> loc
99 | DEFINITION d -> get_definitionloc d
100 | ASM(_,_,_,loc) -> loc
101 | TRY_EXCEPT(_, _, _, loc) -> loc
102 | TRY_FINALLY(_, _, loc) -> loc
106 let explodeStringToInts (s: string) : int64 list =
107 let rec allChars i acc =
109 else allChars (i - 1) (Int64.of_int (Char.code (String.get s i)) :: acc)
111 allChars (-1 + String.length s) []
113 let valueOfDigit chr =
116 '0'..'9' -> (Char.code chr) - (Char.code '0')
117 | 'a'..'z' -> (Char.code chr) - (Char.code 'a') + 10
118 | 'A'..'Z' -> (Char.code chr) - (Char.code 'A') + 10
119 | _ -> assert false in
120 Int64.of_int int_value
122 let string_of_cabsloc l =
123 Printf.sprintf "%s:%d" l.filename l.lineno
125 let format_cabsloc pp l =
126 Format.fprintf pp "%s:%d" l.filename l.lineno