summaryrefslogtreecommitdiff
path: root/src/reporting_basic.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-10-31 15:43:56 +0000
committerAlasdair Armstrong2018-10-31 15:43:56 +0000
commit001e28b487c8a4cb2a25519a3acc8ac8c1aaabf5 (patch)
treec50d5a7bb026e875db96af53fd44d58387d7a7c6 /src/reporting_basic.ml
parent5298e209f0ae12e51f3050888e18ad9be09543e4 (diff)
Rename Reporting_basic to Reporting
There is no Reporting_complex, so it's not clear what the basic is intended to signify anyway. Add a GitHub issue link to any err_unreachable errors (as they are all bugs)
Diffstat (limited to 'src/reporting_basic.ml')
-rw-r--r--src/reporting_basic.ml293
1 files changed, 0 insertions, 293 deletions
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
deleted file mode 100644
index a90c2bcd..00000000
--- a/src/reporting_basic.ml
+++ /dev/null
@@ -1,293 +0,0 @@
-(**************************************************************************)
-(* Sail *)
-(* *)
-(* Copyright (c) 2013-2017 *)
-(* Kathyrn Gray *)
-(* Shaked Flur *)
-(* Stephen Kell *)
-(* Gabriel Kerneis *)
-(* Robert Norton-Wright *)
-(* Christopher Pulte *)
-(* Peter Sewell *)
-(* Alasdair Armstrong *)
-(* Brian Campbell *)
-(* Thomas Bauereiss *)
-(* Anthony Fox *)
-(* Jon French *)
-(* Dominic Mulligan *)
-(* Stephen Kell *)
-(* Mark Wassell *)
-(* *)
-(* All rights reserved. *)
-(* *)
-(* This software was developed by the University of Cambridge Computer *)
-(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
-(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
-(* *)
-(* Redistribution and use in source and binary forms, with or without *)
-(* modification, are permitted provided that the following conditions *)
-(* are met: *)
-(* 1. Redistributions of source code must retain the above copyright *)
-(* notice, this list of conditions and the following disclaimer. *)
-(* 2. Redistributions in binary form must reproduce the above copyright *)
-(* notice, this list of conditions and the following disclaimer in *)
-(* the documentation and/or other materials provided with the *)
-(* distribution. *)
-(* *)
-(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
-(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
-(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
-(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
-(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
-(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
-(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
-(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
-(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
-(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
-(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
-(* SUCH DAMAGE. *)
-(**************************************************************************)
-
-
-(**************************************************************************)
-(* Lem *)
-(* *)
-(* Dominic Mulligan, University of Cambridge *)
-(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *)
-(* Gabriel Kerneis, University of Cambridge *)
-(* Kathy Gray, University of Cambridge *)
-(* Peter Boehm, University of Cambridge (while working on Lem) *)
-(* Peter Sewell, University of Cambridge *)
-(* Scott Owens, University of Kent *)
-(* Thomas Tuerk, University of Cambridge *)
-(* *)
-(* The Lem sources are copyright 2010-2013 *)
-(* by the UK authors above and Institut National de Recherche en *)
-(* Informatique et en Automatique (INRIA). *)
-(* *)
-(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *)
-(* are distributed under the license below. The former are distributed *)
-(* under the LGPLv2, as in the LICENSE file. *)
-(* *)
-(* *)
-(* Redistribution and use in source and binary forms, with or without *)
-(* modification, are permitted provided that the following conditions *)
-(* are met: *)
-(* 1. Redistributions of source code must retain the above copyright *)
-(* notice, this list of conditions and the following disclaimer. *)
-(* 2. Redistributions in binary form must reproduce the above copyright *)
-(* notice, this list of conditions and the following disclaimer in the *)
-(* documentation and/or other materials provided with the distribution. *)
-(* 3. The names of the authors may not be used to endorse or promote *)
-(* products derived from this software without specific prior written *)
-(* permission. *)
-(* *)
-(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *)
-(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *)
-(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *)
-(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *)
-(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *)
-(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *)
-(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *)
-(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *)
-(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *)
-(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *)
-(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
-(**************************************************************************)
-
-let rec skip_lines in_chan = function
- | n when n <= 0 -> ()
- | n -> ignore (input_line in_chan); skip_lines in_chan (n - 1)
-
-let rec read_lines in_chan = function
- | n when n <= 0 -> []
- | n ->
- let l = input_line in_chan in
- let ls = read_lines in_chan (n - 1) in
- l :: ls
-
-let termcode n = "\x1B[" ^ string_of_int n ^ "m"
-
-let print_code1 ff fname lnum1 cnum1 cnum2 =
- try
- let in_chan = open_in fname in
- begin
- try
- skip_lines in_chan (lnum1 - 1);
- let line = input_line in_chan in
- Format.fprintf ff "%s%s%s"
- (Str.string_before line cnum1)
- Util.(Str.string_before (Str.string_after line cnum1) (cnum2 - cnum1) |> red_bg |> clear)
- (Str.string_after line cnum2);
- close_in in_chan
- with e -> (close_in_noerr in_chan;
- prerr_endline (Printf.sprintf "print_code1: %s %d %d %d %s" fname lnum1 cnum1 cnum2 (Printexc.to_string e)))
- end
- with _ -> ()
-
-let format_pos ff p =
- let open Lexing in
- begin
- Format.fprintf ff "file \"%s\", line %d, character %d:\n\n"
- p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol);
- print_code1 ff p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (p.pos_cnum - p.pos_bol + 1);
- Format.fprintf ff "\n\n";
- Format.pp_print_flush ff ()
- end
-
-let print_code2 ff fname lnum1 cnum1 lnum2 cnum2 =
- try
- let in_chan = open_in fname in
- begin
- try
- skip_lines in_chan (lnum1 - 1);
- let line = input_line in_chan in
- Format.fprintf ff "%s%s\n"
- (Str.string_before line cnum1)
- Util.(Str.string_after line cnum1 |> red_bg |> clear);
- let lines = read_lines in_chan (lnum2 - lnum1 - 1) in
- List.iter (fun l -> Format.fprintf ff "%s\n" Util.(l |> red_bg |> clear)) lines;
- let line = input_line in_chan in
- Format.fprintf ff "%s%s"
- Util.(Str.string_before line cnum2 |> red_bg |> clear)
- (Str.string_after line cnum2);
- close_in in_chan
- with e -> (close_in_noerr in_chan; prerr_endline (Printexc.to_string e))
- end
- with _ -> ()
-
-let format_pos2 ff p1 p2 =
- let open Lexing in
- begin
- Format.fprintf ff "file \"%s\", line %d, character %d to line %d, character %d\n\n"
- p1.pos_fname
- p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1)
- p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
- if p1.pos_lnum == p2.pos_lnum
- then print_code1 ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol)
- else print_code2 ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
- Format.pp_print_flush ff ()
- end
-
-(* reads the part between p1 and p2 from the file *)
-
-let read_from_file_pos2 p1 p2 =
- let (s, e, multi) = if p1.Lexing.pos_lnum = p2.Lexing.pos_lnum then
- (* everything in the same line, so really only read this small part*)
- (p1.Lexing.pos_cnum, p2.Lexing.pos_cnum, None)
- else (*multiline, so start reading at beginning of line *)
- (p1.Lexing.pos_bol, p2.Lexing.pos_cnum, Some (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) in
-
- let ic = open_in p1.Lexing.pos_fname in
- let _ = seek_in ic s in
- let l = (e - s) in
- let buf = Bytes.create l in
- let _ = input ic buf 0 l in
- let _ = match multi with None -> () | Some sk -> Bytes.fill buf 0 sk ' ' in
- let _ = close_in ic in
- (buf, not (multi = None))
-
-(* Destruct a location by splitting all the Internal strings except possibly the
- last one into a string list and keeping only the last location *)
-let dest_loc (l : Parse_ast.l) : (Parse_ast.l * string list) =
- let rec aux acc l = match l with
- | Parse_ast.Int(s, Some l') -> aux (s::acc) l'
- | _ -> (l, acc)
- in
- aux [] l
-
-let rec format_loc_aux ff l =
- let (l_org, mod_s) = dest_loc l in
- let _ = match l_org with
- | Parse_ast.Unknown -> Format.fprintf ff "no location information available"
- | Parse_ast.Generated l -> Format.fprintf ff "code generated: original nearby source is "; (format_loc_aux ff l)
- | Parse_ast.Range(p1,p2) -> format_pos2 ff p1 p2
- | Parse_ast.Int(s,_) -> Format.fprintf ff "code in lib from: %s" s
- | Parse_ast.Documented(_, l) -> format_loc_aux ff l
- in
- ()
-
-let format_loc_source ff l =
- match dest_loc l with
- | (Parse_ast.Range (p1, p2), _) ->
- begin
- let (s, multi_line) = read_from_file_pos2 p1 p2 in
- if multi_line then
- Format.fprintf ff " original input:\n%s\n" (Bytes.to_string s)
- else
- Format.fprintf ff " original input: \"%s\"\n" (Bytes.to_string s)
- end
- | _ -> ()
-
-let format_loc ff l =
- (format_loc_aux ff l;
- Format.pp_print_newline ff ();
- Format.pp_print_flush ff ()
-);;
-
-let print_err_loc l =
- (format_loc Format.err_formatter l)
-
-let print_pos p = format_pos Format.std_formatter p
-let print_err_pos p = format_pos Format.err_formatter p
-
-let loc_to_string l =
- let _ = Format.flush_str_formatter () in
- let _ = format_loc_aux Format.str_formatter l in
- let s = Format.flush_str_formatter () in
- s
-
-type pos_or_loc = Loc of Parse_ast.l | LocD of Parse_ast.l * Parse_ast.l | Pos of Lexing.position
-
-let print_err_internal fatal verb_loc p_l m1 m2 =
- Format.eprintf "%s at " m1;
- let _ = (match p_l with Pos p -> print_err_pos p
- | Loc l -> print_err_loc l
- | LocD (l1,l2) ->
- print_err_loc l1; Format.fprintf Format.err_formatter " and "; print_err_loc l2) in
- Format.eprintf "%s\n" m2;
- if verb_loc then (match p_l with Loc l ->
- format_loc_source Format.err_formatter l;
- Format.pp_print_newline Format.err_formatter (); | _ -> ());
- Format.pp_print_flush Format.err_formatter ();
- if fatal then (exit 1) else ()
-
-let print_err fatal verb_loc l m1 m2 =
- print_err_internal fatal verb_loc (Loc l) m1 m2
-
-type error =
- | Err_general of Parse_ast.l * string
- | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
- | Err_todo of Parse_ast.l * string
- | Err_syntax of Lexing.position * string
- | Err_syntax_locn of Parse_ast.l * string
- | Err_lex of Lexing.position * string
- | Err_type of Parse_ast.l * string
- | Err_type_dual of Parse_ast.l * Parse_ast.l * string
-
-let dest_err = function
- | Err_general (l, m) -> ("Error", false, Loc l, m)
- | Err_unreachable (l, (file, line, _, _), m) -> ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line), false, Loc l, m)
- | Err_todo (l, m) -> ("Todo" ^ m, false, Loc l, "")
- | Err_syntax (p, m) -> ("Syntax error", false, Pos p, m)
- | Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
- | Err_lex (p, s) -> ("Lexical error", false, Pos p, s)
- | Err_type (l, m) -> ("Type error", false, Loc l, m)
- | Err_type_dual(l1,l2,m) -> ("Type error", false, LocD (l1,l2), m)
-
-exception Fatal_error of error
-
-(* Abbreviations for the very common cases *)
-let err_todo l m = Fatal_error (Err_todo (l, m))
-let err_unreachable l ocaml_pos m = Fatal_error (Err_unreachable (l, ocaml_pos, m))
-let err_general l m = Fatal_error (Err_general (l, m))
-let err_typ l m = Fatal_error (Err_type (l,m))
-let err_typ_dual l1 l2 m = Fatal_error (Err_type_dual (l1,l2,m))
-
-let report_error e =
- let (m1, verb_pos, pos_l, m2) = dest_err e in
- (print_err_internal verb_pos false pos_l m1 m2; exit 1)
-
-let print_error e =
- let (m1, verb_pos, pos_l, m2) = dest_err e in
- print_err_internal verb_pos false pos_l m1 m2