source: Deliverables/D2.2/8051/cparser/Cabshelper.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

File size: 3.7 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
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.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16
17open Cabs
18
19let nextident = ref 0
20let getident () =
21    nextident := !nextident + 1;
22    !nextident
23
24let 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;
29    ident    = getident ();}
30
31let currentLoc () = 
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;
36    ident    = getident ();}
37
38let cabslu = {lineno = -10; 
39              filename = "cabs loc unknown"; 
40              byteno = -10;
41              ident = 0}
42
43(*********** HELPER FUNCTIONS **********)
44
45let missingFieldDecl = ("___missing_field_name", JUSTBASE, [], cabslu)
46
47let rec isStatic = function
48    [] -> false
49  | (SpecStorage STATIC) :: _ -> true
50  | _ :: rest -> isStatic rest
51
52let rec isExtern = function
53    [] -> false
54  | (SpecStorage EXTERN) :: _ -> true
55  | _ :: rest -> isExtern rest
56
57let rec isInline = function
58    [] -> false
59  | SpecInline :: _ -> true
60  | _ :: rest -> isInline rest
61
62let rec isTypedef = function
63    [] -> false
64  | SpecTypedef :: _ -> true
65  | _ :: rest -> isTypedef rest
66
67
68let get_definitionloc (d : definition) : cabsloc =
69  match d with
70  | FUNDEF(_, _, l, _) -> l
71  | DECDEF(_, l) -> l
72  | TYPEDEF(_, l) -> l
73  | ONLYTYPEDEF(_, l) -> l
74  | GLOBASM(_, l) -> l
75  | PRAGMA(_, l) -> l
76  | LINKAGE (_, l, _) -> l
77
78let get_statementloc (s : statement) : cabsloc =
79begin
80  match s with
81  | NOP(loc) -> loc
82  | COMPUTATION(_,loc) -> loc
83  | BLOCK(_,loc) -> loc
84(*  | SEQUENCE(_,_,loc) -> loc *)
85  | IF(_,_,_,loc) -> loc
86  | WHILE(_,_,loc) -> loc
87  | DOWHILE(_,_,loc) -> loc
88  | FOR(_,_,_,_,loc) -> loc
89  | BREAK(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
97  | GOTO(_,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
103end
104
105
106let explodeStringToInts (s: string) : int64 list = 
107  let rec allChars i acc = 
108    if i < 0 then acc
109    else allChars (i - 1) (Int64.of_int (Char.code (String.get s i)) :: acc)
110  in
111  allChars (-1 + String.length s) []
112
113let valueOfDigit chr =
114  let int_value = 
115    match chr with
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
121
122let string_of_cabsloc l =
123  Printf.sprintf "%s:%d" l.filename l.lineno
124
125let format_cabsloc pp l =
126  Format.fprintf pp "%s:%d" l.filename l.lineno
Note: See TracBrowser for help on using the repository browser.