parsing des annotations dans les programmes

parent cdd7a8d1
......@@ -125,8 +125,8 @@ let rec report fmt = function
fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
| Driver.Error e ->
Driver.report fmt e
| Dynlink.Error e ->
fprintf fmt "Dynlink : %s" (Dynlink.error_message e)
(* | Dynlink.Error e -> *)
(* fprintf fmt "Dynlink : %s" (Dynlink.error_message e) *)
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
(*
......
......@@ -235,9 +235,10 @@ and string = parse
| Loc.Located _ as e -> raise e
| e -> raise (Loc.Located (loc lb, e))
let parse_logic_file = with_location (logic_file token)
let parse_lexpr = with_location (lexpr token)
let parse_list0_decl = with_location (list0_decl token)
let parse_logic_file = with_location (logic_file token)
}
......
......@@ -172,7 +172,7 @@ rule token = parse
| "{"
{ logic_start_loc := loc lexbuf;
let s = logic lexbuf in
LOGIC (snd !logic_start_loc, s) }
LOGIC (fst !logic_start_loc, s) }
| "{{"
{ LEFTBLEFTB }
| "}}"
......
......@@ -77,8 +77,16 @@
{ e with pdesc = Spost (e, (q, []), Transparent) }
***)
open Lexing
let reloc loc lb =
lb.lex_curr_p <- loc;
lb.lex_abs_pos <- loc.pos_cnum
let parse_string f loc s =
let lb = Lexing.from_string s in
reloc loc lb;
f lb
let logic_list0_decl = parse_string Lexer.parse_list0_decl
......
(* test file for ML-why *)
{ }
{ logic f(int) : int }
{ tagada }
{ }
(*
Local Variables:
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment