diff --git a/infer/src/IR/Binop.ml b/infer/src/IR/Binop.ml index 620ef7b40..6901a51e1 100644 --- a/infer/src/IR/Binop.ml +++ b/infer/src/IR/Binop.ml @@ -130,8 +130,5 @@ let str pe binop = " >> " | _ -> text binop ) - | LATEX -> ( - match binop with Ge -> " \\geq " | Le -> " \\leq " | _ -> text binop ) | _ -> text binop - diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml index 45cdc0db4..67cd0e2d4 100644 --- a/infer/src/IR/Exp.ml +++ b/infer/src/IR/Exp.ml @@ -232,7 +232,7 @@ let rec pp_ pe pp_t f e = in match (e : t) with | Var id -> - Ident.pp pe f id + Ident.pp f id | Const c -> F.fprintf f "%a" (Const.pp pe) c | Cast (typ, e) -> @@ -277,4 +277,3 @@ let is_objc_block_closure = function Typ.Procname.is_objc_block name | _ -> false - diff --git a/infer/src/IR/Ident.ml b/infer/src/IR/Ident.ml index 3d70711ed..7ea309380 100644 --- a/infer/src/IR/Ident.ml +++ b/infer/src/IR/Ident.ml @@ -244,26 +244,11 @@ let to_string id = (** Pretty print a name. *) let pp_name f name = F.fprintf f "%s" (name_to_string name) -(** Pretty print a name in latex. *) -let pp_name_latex style f (name: name) = Latex.pp_string style f (name_to_string name) - (** Pretty print an identifier. *) -let pp pe f id = - match pe.Pp.kind with - | TEXT | HTML -> - F.fprintf f "%s" (to_string id) - | LATEX -> - let base_name = name_to_string id.name in - let style = - if has_kind id KFootprint then Latex.Boldface - else if has_kind id KNormal then Latex.Roman - else Latex.Roman - in - F.fprintf f "%a_{%s}" (Latex.pp_string style) base_name (string_of_int id.stamp) - +let pp f id = F.fprintf f "%s" (to_string id) (** pretty printer for lists of identifiers *) -let pp_list pe = Pp.comma_seq (pp pe) +let pp_list = Pp.comma_seq pp (** pretty printer for lists of names *) let pp_name_list = Pp.comma_seq pp_name diff --git a/infer/src/IR/Ident.mli b/infer/src/IR/Ident.mli index 14009471b..2dcd645c1 100644 --- a/infer/src/IR/Ident.mli +++ b/infer/src/IR/Ident.mli @@ -135,16 +135,13 @@ val set_stamp : t -> int -> t val pp_name : Format.formatter -> name -> unit (** Pretty print a name. *) -val pp_name_latex : Latex.style -> Format.formatter -> name -> unit -(** Pretty print a name in latex. *) - -val pp : Pp.env -> Format.formatter -> t -> unit +val pp : Format.formatter -> t -> unit (** Pretty print an identifier. *) val to_string : t -> string (** Convert an identifier to a string. *) -val pp_list : Pp.env -> Format.formatter -> t list -> unit +val pp_list : Format.formatter -> t list -> unit (** Pretty print a list of identifiers. *) val pp_name_list : Format.formatter -> name list -> unit diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index b83a3a79a..0bd883675 100644 --- a/infer/src/IR/Pvar.ml +++ b/infer/src/IR/Pvar.ml @@ -86,37 +86,13 @@ let pp_ f pv = F.fprintf f "old_%a" Mangled.pp name -(** Pretty print a program variable in latex. *) -let pp_latex f pv = - let name = pv.pv_name in - match pv.pv_kind with - | Local_var _ -> - Latex.pp_string Latex.Roman f (Mangled.to_string name) - | Callee_var _ -> - F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) - (Latex.pp_string Latex.Roman) "callee" - | Abduced_retvar _ -> - F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) - (Latex.pp_string Latex.Roman) "abducedRetvar" - | Abduced_ref_param _ -> - F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) - (Latex.pp_string Latex.Roman) "abducedRefParam" - | Global_var _ -> - Latex.pp_string Latex.Boldface f (Mangled.to_string name) - | Seed_var -> - F.fprintf f "%a^{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) - (Latex.pp_string Latex.Roman) "old" - - (** Pretty print a pvar which denotes a value, not an address *) -let pp_value pe f pv = - match pe.Pp.kind with TEXT -> pp_ f pv | HTML -> pp_ f pv | LATEX -> pp_latex f pv - +let pp_value f pv = pp_ f pv (** Pretty print a program variable. *) let pp pe f pv = - let ampersand = match pe.Pp.kind with TEXT -> "&" | HTML -> "&" | LATEX -> "\\&" in - F.fprintf f "%s%a" ampersand (pp_value pe) pv + let ampersand = match pe.Pp.kind with TEXT -> "&" | HTML -> "&" in + F.fprintf f "%s%a" ampersand pp_value pv (** Dump a program variable. *) @@ -291,4 +267,3 @@ let get_initializer_pname {pv_name; pv_kind} = else Some (Typ.Procname.from_string_c_fun name) | _ -> None - diff --git a/infer/src/IR/Pvar.mli b/infer/src/IR/Pvar.mli index d2d459a15..5d4d8d368 100644 --- a/infer/src/IR/Pvar.mli +++ b/infer/src/IR/Pvar.mli @@ -105,7 +105,7 @@ val pp : Pp.env -> F.formatter -> t -> unit val pp_list : Pp.env -> F.formatter -> t list -> unit (** Pretty print a list of program variables. *) -val pp_value : Pp.env -> F.formatter -> t -> unit +val pp_value : F.formatter -> t -> unit (** Pretty print a pvar which denotes a value, not an address *) val pp_translation_unit : F.formatter -> translation_unit -> unit diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 36e359900..37b516abc 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -262,9 +262,7 @@ let color_pre_wrapper pe f x = if Config.print_using_diff && pe.Pp.kind <> Pp.TEXT then let color = pe.Pp.cmap_norm (Obj.repr x) in if color <> pe.Pp.color then ( - ( if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Io_infer.Html.pp_start_color - else Latex.pp_color ) - f color ; + Io_infer.Html.pp_start_color f color ; if Pp.equal_color color Pp.Red then (* All subexpressions red *) (Pp.{pe with cmap_norm= colormap_red; color= Red}, true) @@ -274,11 +272,7 @@ let color_pre_wrapper pe f x = (** Close color annotation if changed *) -let color_post_wrapper changed pe f = - if changed then - if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Io_infer.Html.pp_end_color f () - else Latex.pp_color f pe.Pp.color - +let color_post_wrapper changed f = if changed then Io_infer.Html.pp_end_color f () (** Print a sequence with difference mode if enabled. *) let pp_seq_diff pp pe0 f = @@ -289,10 +283,10 @@ let pp_seq_diff pp pe0 f = () | [x] -> let _, changed = color_pre_wrapper pe0 f x in - F.fprintf f "%a" pp x ; color_post_wrapper changed pe0 f + F.fprintf f "%a" pp x ; color_post_wrapper changed f | x :: l -> let _, changed = color_pre_wrapper pe0 f x in - F.fprintf f "%a" pp x ; color_post_wrapper changed pe0 f ; F.fprintf f ", " ; doit l + F.fprintf f "%a" pp x ; color_post_wrapper changed f ; F.fprintf f ", " ; doit l in doit @@ -308,9 +302,9 @@ let pp_exp_printenv pe0 f e0 = e0 in if not (Exp.equal e0 e) then - match e with Exp.Lvar pvar -> Pvar.pp_value pe f pvar | _ -> assert false + match e with Exp.Lvar pvar -> Pvar.pp_value f pvar | _ -> assert false else Exp.pp_printenv pe Typ.pp f e ; - color_post_wrapper changed pe0 f + color_post_wrapper changed f (** dump an expression. *) @@ -413,15 +407,14 @@ let pp_instr pe0 f instr = let pe, changed = color_pre_wrapper pe0 f instr in ( match instr with | Load (id, e, t, loc) -> - F.fprintf f "%a=*%a:%a [%a]" (Ident.pp pe) id (pp_exp_printenv pe) e (Typ.pp pe) t - Location.pp loc + F.fprintf f "%a=*%a:%a [%a]" Ident.pp id (pp_exp_printenv pe) e (Typ.pp pe) t Location.pp loc | Store (e1, t, e2, loc) -> F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv pe) e1 (Typ.pp pe) t (pp_exp_printenv pe) e2 Location.pp loc | Prune (cond, loc, true_branch, _) -> F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv pe) cond true_branch Location.pp loc | Call (ret_id, e, arg_ts, loc, cf) -> - (match ret_id with None -> () | Some (id, _) -> F.fprintf f "%a=" (Ident.pp pe) id) ; + (match ret_id with None -> () | Some (id, _) -> F.fprintf f "%a=" Ident.pp id) ; F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv pe) e (Pp.comma_seq (pp_exp_typ pe)) arg_ts CallFlags.pp cf Location.pp loc @@ -430,11 +423,11 @@ let pp_instr pe0 f instr = | Abstract loc -> F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc | Remove_temps (temps, loc) -> - F.fprintf f "REMOVE_TEMPS(%a); [%a]" (Ident.pp_list pe) temps Location.pp loc + F.fprintf f "REMOVE_TEMPS(%a); [%a]" Ident.pp_list temps Location.pp loc | Declare_locals (ptl, loc) -> let pp_typ fmt (pvar, _) = Pvar.pp pe fmt pvar in F.fprintf f "DECLARE_LOCALS(%a); [%a]" (Pp.comma_seq pp_typ) ptl Location.pp loc ) ; - color_post_wrapper changed pe0 f + color_post_wrapper changed f let add_with_block_parameters_flag instr = @@ -470,29 +463,17 @@ let d_instr_list (il: instr list) = L.add_print_action (L.PTinstr_list, Obj.repr let pp_atom pe0 f a = let pe, changed = color_pre_wrapper pe0 f a in ( match a with - | Aeq (BinOp (op, e1, e2), Const Cint i) when IntLit.isone i -> ( - match pe.Pp.kind with - | TEXT | HTML -> - F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp (op, e1, e2)) - | LATEX -> - F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp (op, e1, e2)) ) - | Aeq (e1, e2) -> ( - match pe.Pp.kind with - | TEXT | HTML -> - F.fprintf f "%a = %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 - | LATEX -> - F.fprintf f "%a{=}%a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 ) - | Aneq (e1, e2) -> ( - match pe.Pp.kind with - | TEXT | HTML -> - F.fprintf f "%a != %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 - | LATEX -> - F.fprintf f "%a{\\neq}%a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 ) + | Aeq (BinOp (op, e1, e2), Const Cint i) when IntLit.isone i -> + F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp (op, e1, e2)) + | Aeq (e1, e2) -> + F.fprintf f "%a = %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 + | Aneq (e1, e2) -> + F.fprintf f "%a != %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 | Apred (a, es) -> F.fprintf f "%s(%a)" (PredSymb.to_string pe a) (Pp.comma_seq (pp_exp_printenv pe)) es | Anpred (a, es) -> F.fprintf f "!%s(%a)" (PredSymb.to_string pe a) (Pp.comma_seq (pp_exp_printenv pe)) es ) ; - color_post_wrapper changed pe0 f + color_post_wrapper changed f (** dump an atom *) @@ -862,31 +843,23 @@ let rec pp_sexp_env pe0 envo f se = ( match se with | Eexp (e, inst) -> F.fprintf f "%a%a" (pp_exp_printenv pe) e (pp_inst_if_trace pe) inst - | Estruct (fel, inst) -> ( - match pe.Pp.kind with - | TEXT | HTML -> - let pp_diff f (n, se) = F.fprintf f "%a:%a" Typ.Fieldname.pp n (pp_sexp_env pe envo) se in - F.fprintf f "{%a}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst - | LATEX -> - let pp_diff f (n, se) = - F.fprintf f "%a:%a" (Typ.Fieldname.pp_latex Latex.Boldface) n (pp_sexp_env pe envo) se - in - F.fprintf f "\\{%a\\}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst ) + | Estruct (fel, inst) -> + let pp_diff f (n, se) = F.fprintf f "%a:%a" Typ.Fieldname.pp n (pp_sexp_env pe envo) se in + F.fprintf f "{%a}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst | Earray (len, nel, inst) -> let pp_diff f (i, se) = F.fprintf f "%a:%a" (pp_exp_printenv pe) i (pp_sexp_env pe envo) se in F.fprintf f "[%a|%a]%a" (pp_exp_printenv pe) len (pp_seq_diff pp_diff pe) nel (pp_inst_if_trace pe) inst ) ; - color_post_wrapper changed pe0 f + color_post_wrapper changed f (** Pretty print an hpred with an optional predicate env *) let rec pp_hpred_env pe0 envo f hpred = let pe, changed = color_pre_wrapper pe0 f hpred in ( match hpred with - | Hpointsto (e, se, te) - -> ( + | Hpointsto (e, se, te) -> let pe' = match (e, se) with | Lvar pvar, Eexp (Var _, _) when not (Pvar.is_global pvar) -> @@ -894,49 +867,27 @@ let rec pp_hpred_env pe0 envo f hpred = | _ -> pe in - match pe'.Pp.kind with - | TEXT | HTML -> - F.fprintf f "%a|->%a:%a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se - (pp_texp_simple pe') te - | LATEX -> - F.fprintf f "%a\\mapsto %a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se ) - | Hlseg (k, hpara, e1, e2, elist) -> ( - match pe.Pp.kind with - | TEXT | HTML -> - F.fprintf f "lseg%a(%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) e1 - (pp_exp_printenv pe) e2 - (Pp.comma_seq (pp_exp_printenv pe)) - elist (pp_hpara_env pe envo) hpara - | LATEX -> - F.fprintf f "\\textsf{lseg}_{%a}(%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) e1 - (pp_exp_printenv pe) e2 - (Pp.comma_seq (pp_exp_printenv pe)) - elist (pp_hpara_env pe envo) hpara ) + F.fprintf f "%a|->%a:%a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se + (pp_texp_simple pe') te + | Hlseg (k, hpara, e1, e2, elist) -> + F.fprintf f "lseg%a(%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) e1 + (pp_exp_printenv pe) e2 + (Pp.comma_seq (pp_exp_printenv pe)) + elist (pp_hpara_env pe envo) hpara | Hdllseg (k, hpara_dll, iF, oB, oF, iB, elist) -> - match pe.Pp.kind with - | TEXT | HTML -> - F.fprintf f "dllseg%a(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) iF - (pp_exp_printenv pe) oB (pp_exp_printenv pe) oF (pp_exp_printenv pe) iB - (Pp.comma_seq (pp_exp_printenv pe)) - elist (pp_hpara_dll_env pe envo) hpara_dll - | LATEX -> - F.fprintf f "\\textsf{dllseg}_{%a}(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k - (pp_exp_printenv pe) iF (pp_exp_printenv pe) oB (pp_exp_printenv pe) oF - (pp_exp_printenv pe) iB - (Pp.comma_seq (pp_exp_printenv pe)) - elist (pp_hpara_dll_env pe envo) hpara_dll ) ; - color_post_wrapper changed pe0 f + F.fprintf f "dllseg%a(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) iF + (pp_exp_printenv pe) oB (pp_exp_printenv pe) oF (pp_exp_printenv pe) iB + (Pp.comma_seq (pp_exp_printenv pe)) + elist (pp_hpara_dll_env pe envo) hpara_dll ) ; + color_post_wrapper changed f and pp_hpara_env pe envo f hpara = match envo with | None -> let r, n, svars, evars, b = (hpara.root, hpara.next, hpara.svars, hpara.evars, hpara.body) in - F.fprintf f "lam [%a,%a,%a]. exists [%a]. %a" (Ident.pp pe) r (Ident.pp pe) n - (Pp.seq (Ident.pp pe)) - svars - (Pp.seq (Ident.pp pe)) - evars + F.fprintf f "lam [%a,%a,%a]. exists [%a]. %a" Ident.pp r Ident.pp n (Pp.seq Ident.pp) svars + (Pp.seq Ident.pp) evars (pp_star_seq (pp_hpred_env pe envo)) b | Some env -> @@ -954,12 +905,8 @@ and pp_hpara_dll_env pe envo f hpara_dll = , hpara_dll.evars_dll , hpara_dll.body_dll ) in - F.fprintf f "lam [%a,%a,%a,%a]. exists [%a]. %a" (Ident.pp pe) iF (Ident.pp pe) oB - (Ident.pp pe) oF - (Pp.seq (Ident.pp pe)) - svars - (Pp.seq (Ident.pp pe)) - evars + F.fprintf f "lam [%a,%a,%a,%a]. exists [%a]. %a" Ident.pp iF Ident.pp oB Ident.pp oF + (Pp.seq Ident.pp) svars (Pp.seq Ident.pp) evars (pp_star_seq (pp_hpred_env pe envo)) b | Some env -> @@ -1242,7 +1189,7 @@ let fav_from_list l = let fav_to_list fav = List.rev !fav (** Pretty print a fav. *) -let pp_fav pe f fav = Pp.seq (Ident.pp pe) f (fav_to_list fav) +let pp_fav f fav = Pp.seq Ident.pp f (fav_to_list fav) (** Copy a [fav]. *) let fav_copy fav = ref (List.map ~f:(fun x -> x) !fav) diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index fae0cc903..668a0ec87 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -289,7 +289,7 @@ val hpred_get_lhs : hpred -> Exp.t val color_pre_wrapper : Pp.env -> F.formatter -> 'a -> Pp.env * bool (** Begin change color if using diff printing, return updated printenv and change status *) -val color_post_wrapper : bool -> Pp.env -> F.formatter -> unit +val color_post_wrapper : bool -> F.formatter -> unit (** Close color annotation if changed *) val pp_exp_printenv : Pp.env -> F.formatter -> Exp.t -> unit @@ -476,7 +476,7 @@ val fav_duplicates : bool ref (** flag to indicate whether fav's are stored in duplicate form. Only to be used with fav_to_list *) -val pp_fav : Pp.env -> F.formatter -> fav -> unit +val pp_fav : F.formatter -> fav -> unit (** Pretty print a fav. *) val fav_new : unit -> fav diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 196864ba7..9862fb8ac 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -1279,8 +1279,6 @@ module Fieldname = struct Format.fprintf f "%s" field_name - let pp_latex style f fn = Latex.pp_string style f (to_string fn) - let class_name_replace fname ~f = match fname with | Clang {class_name; field_name} -> diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index d8b6e659a..5910e643c 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -589,9 +589,6 @@ module Fieldname : sig val pp : Format.formatter -> t -> unit (** Pretty print a field name. *) - val pp_latex : Latex.style -> Format.formatter -> t -> unit - (** Pretty print a field name in latex. *) - val java_get_class : t -> string (** The class part of the fieldname *) diff --git a/infer/src/absint/Var.ml b/infer/src/absint/Var.ml index 59bc41d66..7d393507b 100644 --- a/infer/src/absint/Var.ml +++ b/infer/src/absint/Var.ml @@ -29,12 +29,7 @@ let is_return = function ProgramVar pvar -> Pvar.is_return pvar | LogicalVar _ - let is_footprint = function ProgramVar _ -> false | LogicalVar id -> Ident.is_footprint id -let pp fmt = function - | ProgramVar pv -> - Pvar.pp Pp.text fmt pv - | LogicalVar id -> - Ident.pp Pp.text fmt id - +let pp fmt = function ProgramVar pv -> Pvar.pp Pp.text fmt pv | LogicalVar id -> Ident.pp fmt id module Map = PrettyPrintable.MakePPMap (struct type nonrec t = t diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index 85f17b507..85436c1d5 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -32,14 +32,6 @@ let load_specfiles () = specs_files_in_dir result_specs_dir -(** Create and initialize latex file *) -let begin_latex_file fmt = - let author = "Infer " ^ Version.versionString in - let title = "Report on Analysis Results" in - let table_of_contents = true in - Latex.pp_begin fmt (author, title, table_of_contents) - - let error_desc_to_csv_string error_desc = let pp fmt = F.fprintf fmt "%a" Localise.pp_error_desc error_desc in Escape.escape_csv (F.asprintf "%t" pp) @@ -684,55 +676,6 @@ module Report = struct let pp_stats fmt stats = Stats.pp fmt stats end -module Summary = struct - let pp_summary_out summary = - let proc_name = Specs.get_proc_name summary in - if CLOpt.equal_command Config.command CLOpt.Report && not Config.quiet then - L.result "Procedure: %a@\n%a@." Typ.Procname.pp proc_name Specs.pp_summary_text summary - - - (** Write proc summary to latex file *) - let write_summary_latex fmt summary = - let proc_name = Specs.get_proc_name summary in - Latex.pp_section fmt - ("Analysis of function " ^ Latex.convert_string (Typ.Procname.to_string proc_name)) ; - F.fprintf fmt "@[%a@]" (Specs.pp_summary_latex Black) summary - - - let pp_summary_xml summary fname = - if Config.xml_specs then - let base = DB.chop_extension (DB.filename_from_string fname) in - let xml_file = DB.filename_add_suffix base ".xml" in - let specs = Specs.get_specs_from_payload summary in - if not (DB.file_exists xml_file) - || DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time xml_file - then - let xml_out = Utils.create_outfile (DB.filename_to_string xml_file) in - Utils.do_outf xml_out (fun outf -> - Dotty.print_specs_xml (Specs.get_signature summary) specs (Specs.get_loc summary) - outf.fmt ; - Utils.close_outf outf ) - - - let print_summary_dot_svg summary fname = - if Config.svg then - let base = DB.chop_extension (DB.filename_from_string fname) in - let specs = Specs.get_specs_from_payload summary in - let dot_file = DB.filename_add_suffix base ".dot" in - let svg_file = DB.filename_add_suffix base ".svg" in - if not (DB.file_exists dot_file) - || DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time dot_file - then Dotty.pp_speclist_dotty_file base specs ; - if not (DB.file_exists svg_file) - || DB.file_modified_time dot_file > DB.file_modified_time svg_file - then - ignore - (Sys.command - ( "dot -Tsvg \"" ^ DB.filename_to_string dot_file ^ "\" >\"" - ^ DB.filename_to_string svg_file ^ "\"" )) - -end - (** Categorize the preconditions of specs and print stats *) module PreconditionStats = struct let nr_nopres = ref 0 @@ -811,9 +754,9 @@ let error_filter filters proc_name file error_desc error_name = && filters.Inferconfig.error_filter error_name && filters.Inferconfig.proc_filter proc_name -type report_kind = Issues | Procs | Stats | Calls | Summary [@@deriving compare] +type report_kind = Issues | Procs | Stats | Calls [@@deriving compare] -type bug_format_kind = Json | Csv | Tests | Text | Latex [@@deriving compare] +type bug_format_kind = Json | Csv | Tests | Text [@@deriving compare] let pp_issue_in_format (format_kind, (outf: Utils.outfile)) error_filter {Issue.proc_name; proc_location; err_key; err_data} = @@ -822,8 +765,6 @@ let pp_issue_in_format (format_kind, (outf: Utils.outfile)) error_filter IssuesCsv.pp_issue outf.fmt error_filter proc_name (Some proc_location) err_key err_data | Json -> IssuesJson.pp_issue outf.fmt error_filter proc_name (Some proc_location) err_key err_data - | Latex -> - L.(die InternalError) "Printing issues in latex is not implemented" | Tests -> L.(die InternalError) "Print issues as tests is not implemented" | Text -> @@ -840,40 +781,30 @@ let pp_issues_in_format (format_kind, (outf: Utils.outfile)) = L.(die InternalError) "Print issues as tests is not implemented" | Text -> IssuesTxt.pp_issues_of_error_log outf.fmt - | Latex -> - L.(die InternalError) "Printing issues in latex is not implemented" let pp_procs_in_format (format_kind, (outf: Utils.outfile)) = match format_kind with | Csv -> ProcsCsv.pp_summary outf.fmt - | Json | Latex | Tests | Text -> - L.(die InternalError) "Printing procs in json/latex/tests/text is not implemented" + | Json | Tests | Text -> + L.(die InternalError) "Printing procs in json/tests/text is not implemented" let pp_calls_in_format (format_kind, (outf: Utils.outfile)) = match format_kind with | Csv -> CallsCsv.pp_calls outf.fmt - | Json | Tests | Text | Latex -> - L.(die InternalError) "Printing calls in json/tests/text/latex is not implemented" + | Json | Tests | Text -> + L.(die InternalError) "Printing calls in json/tests/text is not implemented" let pp_stats_in_format (format_kind, _) = match format_kind with | Csv -> Stats.process_summary - | Json | Tests | Text | Latex -> - L.(die InternalError) "Printing stats in json/tests/text/latex is not implemented" - - -let pp_summary_in_format (format_kind, (outf: Utils.outfile)) = - match format_kind with - | Latex -> - Summary.write_summary_latex outf.fmt - | Json | Csv | Tests | Text -> - L.(die InternalError) "Printing summary in json/csv/tests/text is not implemented" + | Json | Tests | Text -> + L.(die InternalError) "Printing stats in json/tests/text is not implemented" let pp_issues_of_error_log error_filter linereader proc_loc_opt procname err_log bug_format_list = @@ -916,19 +847,8 @@ let pp_stats error_filter linereader summary stats stats_format_list = List.iter ~f:pp_stats_in_format stats_format_list -let pp_summary summary fname summary_format_list = - let pp_summary_in_format format = - let pp_summary = pp_summary_in_format format in - pp_summary summary - in - List.iter ~f:pp_summary_in_format summary_format_list ; - Summary.pp_summary_out summary ; - Summary.pp_summary_xml summary fname ; - Summary.print_summary_dot_svg summary fname - - -let pp_summary_by_report_kind formats_by_report_kind summary fname error_filter linereader stats - file issues_acc = +let pp_summary_by_report_kind formats_by_report_kind summary error_filter linereader stats file + issues_acc = let pp_summary_by_report_kind (report_kind, format_list) = match (report_kind, format_list) with | Procs, _ :: _ -> @@ -937,8 +857,6 @@ let pp_summary_by_report_kind formats_by_report_kind summary fname error_filter pp_stats (error_filter file) linereader summary stats format_list | Calls, _ :: _ -> pp_calls summary format_list - | Summary, _ -> - pp_summary summary fname format_list | _ -> () in @@ -960,8 +878,6 @@ let pp_json_report_by_report_kind formats_by_report_kind fname = L.(die InternalError) "Printing issues from json does not support json output" | Csv -> L.(die InternalError) "Printing issues from json does not support csv output" - | Latex -> - L.(die InternalError) "Printing issues from json does not support latex output" in List.iter ~f:pp_json_issue format_list in @@ -999,15 +915,15 @@ let pp_lint_issues filters formats_by_report_kind linereader procname error_log (** Process a summary *) -let process_summary filters formats_by_report_kind linereader stats fname summary issues_acc = +let process_summary filters formats_by_report_kind linereader stats summary issues_acc = let file = (Specs.get_loc summary).Location.file in let proc_name = Specs.get_proc_name summary in let error_filter = error_filter filters proc_name in let pp_simple_saved = !Config.pp_simple in Config.pp_simple := true ; let issues_acc' = - pp_summary_by_report_kind formats_by_report_kind summary fname error_filter linereader stats - file issues_acc + pp_summary_by_report_kind formats_by_report_kind summary error_filter linereader stats file + issues_acc in if Config.precondition_stats then PreconditionStats.do_summary proc_name summary ; Config.pp_simple := pp_simple_saved ; @@ -1135,11 +1051,6 @@ let init_stats_format_list () = csv_format -let init_summary_format_list () = - let latex_format = Option.value_map ~f:(mk_format Latex) ~default:[] Config.latex in - latex_format - - let init_files format_list_by_kind = let init_files_of_report_kind (report_kind, format_list) = let init_files_of_format (format_kind, (outfile: Utils.outfile)) = @@ -1152,9 +1063,7 @@ let init_files format_list_by_kind = Report.pp_header outfile.fmt () | Json, Issues -> IssuesJson.pp_json_open outfile.fmt () - | Latex, Summary -> - begin_latex_file outfile.fmt - | (Csv | Json | Latex | Tests | Text), _ -> + | (Csv | Json | Tests | Text), _ -> () in List.iter ~f:init_files_of_format format_list @@ -1162,7 +1071,7 @@ let init_files format_list_by_kind = List.iter ~f:init_files_of_report_kind format_list_by_kind -let finalize_and_close_files format_list_by_kind stats pdflatex = +let finalize_and_close_files format_list_by_kind stats = let close_files_of_report_kind (report_kind, format_list) = let close_files_of_format (format_kind, (outfile: Utils.outfile)) = ( match (format_kind, report_kind) with @@ -1170,18 +1079,9 @@ let finalize_and_close_files format_list_by_kind stats pdflatex = F.fprintf outfile.fmt "%a@?" Report.pp_stats stats | Json, Issues -> IssuesJson.pp_json_close outfile.fmt () - | Latex, Summary -> - Latex.pp_end outfile.fmt () - | (Csv | Latex | Tests | Text | Json), _ -> + | (Csv | Tests | Text | Json), _ -> () ) ; - Utils.close_outf outfile ; - (* bug_format_kind report_kind *) - if [%compare.equal : bug_format_kind * report_kind] - (format_kind, report_kind) (Latex, Summary) - then ( - pdflatex outfile.fname ; - let pdf_name = Filename.chop_extension outfile.fname ^ ".pdf" in - ignore (Sys.command ("open " ^ pdf_name)) ) + Utils.close_outf outfile in List.iter ~f:close_files_of_format format_list ; () @@ -1190,16 +1090,14 @@ let finalize_and_close_files format_list_by_kind stats pdflatex = let pp_summary_and_issues formats_by_report_kind issue_formats = - let pdflatex fname = ignore (Sys.command ("pdflatex " ^ fname)) in let stats = Stats.create () in let linereader = Printer.LineReader.create () in let filters = Inferconfig.create_filters Config.analyzer in let iterate_summaries = AnalysisResults.get_summary_iterator () in let all_issues = ref [] in - iterate_summaries (fun (filename, summary) -> + iterate_summaries (fun (_, summary) -> all_issues - := process_summary filters formats_by_report_kind linereader stats filename summary - !all_issues ) ; + := process_summary filters formats_by_report_kind linereader stats summary !all_issues ) ; List.iter ~f:(fun ({Issue.proc_name} as issue) -> let error_filter = error_filter filters proc_name in @@ -1212,7 +1110,7 @@ let pp_summary_and_issues formats_by_report_kind issue_formats = Typ.Procname.Map.iter (pp_lint_issues filters formats_by_report_kind linereader) !LintIssues.errLogMap ; - finalize_and_close_files formats_by_report_kind stats pdflatex + finalize_and_close_files formats_by_report_kind stats let main ~report_csv ~report_json = @@ -1221,8 +1119,7 @@ let main ~report_csv ~report_json = [ (Issues, issue_formats) ; (Procs, init_procs_format_list ()) ; (Calls, init_calls_format_list ()) - ; (Stats, init_stats_format_list ()) - ; (Summary, init_summary_format_list ()) ] + ; (Stats, init_stats_format_list ()) ] in if Config.developer_mode then register_perf_stats_report () ; init_files formats_by_report_kind ; diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index a5413f4e4..ce018aad8 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -135,7 +135,7 @@ let rec strexp_to_string pe coo f se = | Sil.Eexp (Exp.Lvar pvar, _) -> F.fprintf f "%a" (Pvar.pp pe) pvar | Sil.Eexp (Exp.Var id, _) -> - if !print_full_prop then F.fprintf f "%a" (Ident.pp pe) id else () + if !print_full_prop then F.fprintf f "%a" Ident.pp id else () | Sil.Eexp (e, _) -> if !print_full_prop then F.fprintf f "%a" (Sil.pp_exp_printenv pe) e else F.fprintf f "_" | Sil.Estruct (ls, _) -> @@ -1715,4 +1715,3 @@ let print_specs_xml signature specs loc fmt = [xml_signature; xml_specifications] in Io_infer.Xml.pp_document true fmt proc_summary - diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 2d41cff1e..52caae24c 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -571,7 +571,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = let hpred_typ_opt = find_hpred_typ hpred in let value_str_from_pvars_vpath pvars vpath = if pvars <> [] then - let pp = Pp.seq (Pvar.pp_value Pp.text) in + let pp = Pp.seq Pvar.pp_value in let desc_string = F.asprintf "%a" pp pvars in Some desc_string else @@ -1331,4 +1331,3 @@ let explain_null_test_after_dereference tenv exp node line loc = let warning_err loc fmt_string = L.(debug Analysis Medium) ("%a: Warning: " ^^ fmt_string) Location.pp loc - diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 398e2f7e7..1f32d6be6 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -123,8 +123,7 @@ let pp_texp_simple pe = let pp_hpred_stackvar pe0 f (hpred: Sil.hpred) = let pe, changed = Sil.color_pre_wrapper pe0 f hpred in ( match hpred with - | Hpointsto (Exp.Lvar pvar, se, te) - -> ( + | Hpointsto (Exp.Lvar pvar, se, te) -> let pe' = match se with | Eexp (Exp.Var _, _) when not (Pvar.is_global pvar) -> @@ -132,15 +131,10 @@ let pp_hpred_stackvar pe0 f (hpred: Sil.hpred) = | _ -> pe in - match pe'.kind with - | TEXT | HTML -> - F.fprintf f "%a = %a:%a" (Pvar.pp_value pe') pvar (Sil.pp_sexp pe') se - (pp_texp_simple pe') te - | LATEX -> - F.fprintf f "%a{=}%a" (Pvar.pp_value pe') pvar (Sil.pp_sexp pe') se ) + F.fprintf f "%a = %a:%a" Pvar.pp_value pvar (Sil.pp_sexp pe') se (pp_texp_simple pe') te | Hpointsto _ | Hlseg _ | Hdllseg _ -> assert false (* should not happen *) ) ; - Sil.color_post_wrapper changed pe0 f + Sil.color_post_wrapper changed f (** Pretty print a substitution. *) @@ -158,12 +152,8 @@ let d_sub (sub: Sil.subst) = L.add_print_action (PTsub, Obj.repr sub) let pp_sub_entry pe0 f entry = let pe, changed = Sil.color_pre_wrapper pe0 f entry in let x, e = entry in - ( match pe.kind with - | TEXT | HTML -> - F.fprintf f "%a = %a" (Ident.pp pe) x (Sil.pp_exp_printenv pe) e - | LATEX -> - F.fprintf f "%a{=}%a" (Ident.pp pe) x (Sil.pp_exp_printenv pe) e ) ; - Sil.color_post_wrapper changed pe0 f + F.fprintf f "%a = %a" Ident.pp x (Sil.pp_exp_printenv pe) e ; + Sil.color_post_wrapper changed f (** Pretty print a substitution as a list of (ident,exp) pairs *) @@ -204,14 +194,7 @@ let pp_sigma_simple pe env fmt sigma = if sg <> [] then Format.fprintf fmt "%a" (Pp.semicolon_seq ~print_env:pe (pp_hpred_stackvar pe)) sg in - let pp_nl fmt doit = - if doit then - match pe.Pp.kind with - | TEXT | HTML -> - Format.fprintf fmt " ;@\n" - | LATEX -> - Format.fprintf fmt " ; \\\\@\n" - in + let pp_nl fmt doit = if doit then Format.fprintf fmt " ;@\n" in let pp_nonstack fmt = Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)) fmt in if sigma_stack <> [] || sigma_nonstack <> [] then Format.fprintf fmt "%a%a%a" pp_stack sigma_stack pp_nl @@ -260,43 +243,26 @@ let get_pure_extended p = (** Print existential quantification *) -let pp_evars pe f evars = - if evars <> [] then - match pe.Pp.kind with - | TEXT | HTML -> - F.fprintf f "exists [%a]. " (Pp.comma_seq (Ident.pp pe)) evars - | LATEX -> - F.fprintf f "\\exists %a. " (Pp.comma_seq (Ident.pp pe)) evars +let pp_evars f evars = + if evars <> [] then F.fprintf f "exists [%a]. " (Pp.comma_seq Ident.pp) evars (** Print an hpara in simple mode *) let pp_hpara_simple pe_ env n f pred = let pe = Pp.reset_obj_sub pe_ in (* no free vars: disable object substitution *) - match pe.kind with - | TEXT | HTML -> - F.fprintf f "P%d = %a%a" n (pp_evars pe) pred.Sil.evars - (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env))) - pred.Sil.body - | LATEX -> - F.fprintf f "P_{%d} = %a%a\\\\" n (pp_evars pe) pred.Sil.evars - (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env))) - pred.Sil.body + F.fprintf f "P%d = %a%a" n pp_evars pred.Sil.evars + (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env))) + pred.Sil.body (** Print an hpara_dll in simple mode *) let pp_hpara_dll_simple pe_ env n f pred = let pe = Pp.reset_obj_sub pe_ in (* no free vars: disable object substitution *) - match pe.kind with - | TEXT | HTML -> - F.fprintf f "P%d = %a%a" n (pp_evars pe) pred.Sil.evars_dll - (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env))) - pred.Sil.body_dll - | LATEX -> - F.fprintf f "P_{%d} = %a%a" n (pp_evars pe) pred.Sil.evars_dll - (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env))) - pred.Sil.body_dll + F.fprintf f "P%d = %a%a" n pp_evars pred.Sil.evars_dll + (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env))) + pred.Sil.body_dll (** Create an environment mapping (ident) expressions to the program variables containing them *) @@ -341,7 +307,6 @@ let prop_pred_env prop = (** Pretty print a proposition. *) let pp_prop pe0 f prop = let pe = prop_update_obj_sub pe0 prop in - let latex = Pp.equal_print_kind pe.Pp.kind Pp.LATEX in let do_print f () = let subl = Sil.sub_to_list prop.sub in (* since prop diff is based on physical equality, we need to extract the sub verbatim *) @@ -350,7 +315,7 @@ let pp_prop pe0 f prop = if subl <> [] then F.fprintf f "%a ;@\n" (pp_subl pe) subl ; if pi <> [] then F.fprintf f "%a ;@\n" (pp_pi pe) pi in - if !Config.pp_simple || latex then + if !Config.pp_simple then let env = prop_pred_env prop in let iter_f n hpara = F.fprintf f "@,@[%a@]" (pp_hpara_simple pe env n) hpara in let iter_f_dll n hpara_dll = @@ -358,9 +323,6 @@ let pp_prop pe0 f prop = in let pp_predicates _ () = if Sil.Predicates.is_empty env then () - else if latex then ( - F.fprintf f "@\n\\\\\\textsf{where }" ; - Sil.Predicates.iter env iter_f iter_f_dll ) else ( F.fprintf f "@,where" ; Sil.Predicates.iter env iter_f iter_f_dll ) @@ -2517,7 +2479,7 @@ let prop_iter_make_id_primed tenv id iter = | Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 -> L.internal_error "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n" ; L.internal_error "Broken Assumption: id notin e for all (id,e) in sub@\n" ; - L.internal_error "(id,e) : (%a,%a)@\n" (Ident.pp Pp.text) id1 Exp.pp e1 ; + L.internal_error "(id,e) : (%a,%a)@\n" Ident.pp id1 Exp.pp e1 ; L.internal_error "PROP : %a@\n@." (pp_prop Pp.text) (prop_iter_to_prop tenv iter) ; assert false | Aeq (Var id1, e1) when Ident.equal pid id1 -> diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index 1d8c71ab2..6bc37e923 100644 --- a/infer/src/backend/propgraph.ml +++ b/infer/src/backend/propgraph.ml @@ -287,12 +287,10 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist = | TEXT -> F.fprintf f "%s %d of %d:@\n%a" s n num (Prop.pp_prop pe) x | HTML -> - F.fprintf f "%s %d of %d:@\n%a@\n" s n num (Prop.pp_prop pe) x - | LATEX -> - F.fprintf f "@[%a@]@\n" (Prop.pp_prop pe) x ) - | x_ :: l -> - let pe = update_pe_diff x_ in - let x = add_base_stack x_ in + F.fprintf f "%s %d of %d:@\n%a@\n" s n num (Prop.pp_prop pe) x ) + | _x :: l -> + let pe = update_pe_diff _x in + let x = add_base_stack _x in match pe.kind with | TEXT -> F.fprintf f "%s %d of %d:@\n%a@\n%a" s n num (Prop.pp_prop pe) x @@ -302,10 +300,6 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist = F.fprintf f "%s %d of %d:@\n%a@\n%a" s n num (Prop.pp_prop pe) x (pp_seq_newline (n + 1)) l - | LATEX -> - F.fprintf f "@[%a@]\\\\@\n\\bigvee\\\\@\n%a" (Prop.pp_prop pe) x - (pp_seq_newline (n + 1)) - l in pp_seq_newline 1 f plist @@ -313,4 +307,3 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist = (** dump a propset *) let d_proplist (p: 'a Prop.t) (pl: 'b Prop.t list) = L.add_print_action (L.PTproplist, Obj.repr (p, pl)) - diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index a23f6b2b5..e5e58be29 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -430,13 +430,6 @@ let pp_spec pe num_opt fmt spec = pre Io_infer.Html.pp_end_color () ; F.fprintf fmt "%a" (Propgraph.pp_proplist pe_post "POST" (pre, true)) post_list ; F.fprintf fmt "----------------------------------------------------------------" - | LATEX -> - F.fprintf fmt "\\textbf{\\large Requires}\\\\@\n@[%a%a%a@]\\\\@\n" Latex.pp_color Pp.Blue - (Prop.pp_prop (Pp.latex Blue)) - pre Latex.pp_color pe.Pp.color ; - F.fprintf fmt "\\textbf{\\large Ensures}\\\\@\n@[%a@]" - (Propgraph.pp_proplist pe_post "POST" (pre, true)) - post_list (** Dump a spec *) @@ -458,13 +451,6 @@ let pp_specs pe fmt specs = incr cnt ; F.fprintf fmt "%a
@\n" (pp_spec pe (Some (!cnt, total))) spec) specs - | LATEX -> - List.iter - ~f:(fun spec -> - incr cnt ; - F.fprintf fmt "\\subsection*{Spec %d of %d}@\n\\(%a\\)@\n" !cnt total (pp_spec pe None) - spec) - specs let describe_phase summary = @@ -541,16 +527,6 @@ let pp_summary_text fmt summary = summary.payload -let pp_summary_latex color fmt summary = - let pe = Pp.latex color in - F.fprintf fmt "\\begin{verbatim}@\n" ; - pp_summary_no_stats_specs fmt summary ; - F.fprintf fmt "%a@\n" pp_errlog (get_err_log summary) ; - F.fprintf fmt "%a@\n" pp_stats summary.stats ; - F.fprintf fmt "\\end{verbatim}@\n" ; - F.fprintf fmt "%a@\n" (pp_specs pe) (get_specs_from_payload summary) - - let pp_summary_html source color fmt summary = let pe = Pp.html color in Io_infer.Html.pp_start_color fmt Black ; diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 37ab91f19..b065315a0 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -221,9 +221,6 @@ val pp_specs : Pp.env -> Format.formatter -> Prop.normal spec list -> unit val pp_summary_html : SourceFile.t -> Pp.color -> Format.formatter -> summary -> unit (** Print the summary in html format *) -val pp_summary_latex : Pp.color -> Format.formatter -> summary -> unit -(** Print the summary in latext format *) - val pp_summary_text : Format.formatter -> summary -> unit (** Print the summary in text format *) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 10139608f..80956537a 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1425,11 +1425,6 @@ and join_cond = |} -and latex = - CLOpt.mk_path_opt ~deprecated:["latex"] ~long:"latex" ~meta:"file" - "Write a latex report of the analysis results to a file" - - and log_file = CLOpt.mk_string ~deprecated:["out_file"; "-out-file"] ~long:"log-file" ~meta:"file" ~default:"logs" "Specify the file to use for logging" @@ -2472,8 +2467,6 @@ and jobs = !jobs and join_cond = !join_cond -and latex = !latex - and linter = !linter and linters = diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 0deb06714..388cc905c 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -497,8 +497,6 @@ val join_cond : int val keep_going : bool -val latex : string option - val linter : string option val linters : bool diff --git a/infer/src/base/Latex.ml b/infer/src/base/Latex.ml deleted file mode 100644 index ce0885448..000000000 --- a/infer/src/base/Latex.ml +++ /dev/null @@ -1,72 +0,0 @@ -(* - * Copyright (c) 2009 - 2013 Monoidics ltd. - * Copyright (c) 2013 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd -module F = Format - -(** Produce output in latex *) - -type style = Boldface | Roman | Italics - -(** Convert a string to a latex-friendly format *) -let convert_string s = - if String.contains s '_' then - let cnt = ref 0 in - let s' = ref "" in - let f c = - if Char.equal c '_' then s' := !s' ^ "\\_" else s' := !s' ^ Char.escaped s.[!cnt] ; - incr cnt - in - String.iter ~f s ; !s' - else s - - -(** Print a string in the given style, after converting it into latex-friendly format *) -let pp_string style f s = - let converted = convert_string s in - match style with - | Boldface -> - F.fprintf f "\\textbf{%s}" converted - | Roman -> - F.fprintf f "\\textrm{%s}" converted - | Italics -> - F.fprintf f "\\textit{%s}" converted - - -let color_to_string (c: Pp.color) = - match c with - | Black -> - "black" - | Blue -> - "blue" - | Green -> - "green" - | Orange -> - "orange" - | Red -> - "red" - - -(** Print color command *) -let pp_color f color = F.fprintf f "\\color{%s}" (color_to_string color) - -(** Prelude for a latex file with the given author and title *) -let pp_begin f (author, title, table_of_contents) = - let pp_toc f () = if table_of_contents then F.fprintf f "\\tableofcontents@\n" else () in - F.fprintf f - "\\documentclass{article}@\n\\usepackage{hyperref}@\n\\usepackage{color}@\n\\author{%s}@\n\\title{%s}@\n\\begin{document}@\n\\maketitle@\n%a" - author title pp_toc () - - -(** Epilogue for a latex file *) -let pp_end f () = F.fprintf f "\\end{document}@\n" - -(** Section with the given title *) -let pp_section f title = F.fprintf f "\\section{%s}@\n" title diff --git a/infer/src/base/Latex.mli b/infer/src/base/Latex.mli deleted file mode 100644 index f262c255c..000000000 --- a/infer/src/base/Latex.mli +++ /dev/null @@ -1,31 +0,0 @@ -(* - * Copyright (c) 2009 - 2013 Monoidics ltd. - * Copyright (c) 2013 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd - -type style = Boldface | Roman | Italics - -val convert_string : string -> string -(** Convert a string to a latex-friendly format *) - -val pp_string : style -> Format.formatter -> string -> unit -(** Print a string in the given style, after converting it into latex-friendly format *) - -val pp_color : Format.formatter -> Pp.color -> unit -(** Print color command *) - -val pp_begin : Format.formatter -> string * string * bool -> unit -(** Prelude for a latex file with the given author and title and table of contents flag *) - -val pp_end : Format.formatter -> unit -> unit -(** Epilogue for a latex file *) - -val pp_section : Format.formatter -> string -> unit -(** Section with the given title *) diff --git a/infer/src/base/Pp.ml b/infer/src/base/Pp.ml index a9ad6a812..c0f91127d 100644 --- a/infer/src/base/Pp.ml +++ b/infer/src/base/Pp.ml @@ -18,7 +18,7 @@ module CLOpt = CommandLineOption type simple_kind = SIM_DEFAULT | SIM_WITH_TYP (** Kind of printing *) -type print_kind = TEXT | LATEX | HTML [@@deriving compare] +type print_kind = TEXT | HTML [@@deriving compare] let equal_print_kind = [%compare.equal : print_kind] @@ -66,17 +66,6 @@ let html color = kind= HTML; cmap_norm= colormap_from_color color; cmap_foot= colormap_from_color color; color } -(** Default latex print environment *) -let latex color = - { opt= SIM_DEFAULT - ; kind= LATEX - ; break_lines= false - ; cmap_norm= colormap_from_color color - ; cmap_foot= colormap_from_color color - ; color - ; obj_sub= None } - - (** Extend the normal colormap for the given object with the given color *) let extend_colormap pe (x: Obj.t) (c: color) = let colormap (y: Obj.t) = if phys_equal x y then c else pe.cmap_norm y in @@ -110,16 +99,14 @@ let color_string = function "color_red" -let seq ?(print_env= text) ?sep:(sep_text = " ") ?(sep_html= sep_text) ?(sep_latex= sep_text) pp = +let seq ?(print_env= text) ?sep:(sep_text = " ") ?(sep_html= sep_text) pp = let rec aux f = function | [] -> () | [x] -> F.fprintf f "%a" pp x | x :: l -> - let sep = - match print_env.kind with TEXT -> sep_text | HTML -> sep_html | LATEX -> sep_latex - in + let sep = match print_env.kind with TEXT -> sep_text | HTML -> sep_html in if print_env.break_lines then F.fprintf f "%a%s@ %a" pp x sep aux l else F.fprintf f "%a%s%a" pp x sep aux l in @@ -130,7 +117,7 @@ let comma_seq ?print_env pp f l = seq ?print_env ~sep:"," pp f l let semicolon_seq ?print_env pp f l = seq ?print_env ~sep:";" pp f l -let or_seq ?print_env pp f = seq ?print_env ~sep:" ||" ~sep_html:" ∨" ~sep_latex:" \\vee" pp f +let or_seq ?print_env pp f = seq ?print_env ~sep:" ||" ~sep_html:" ∨" pp f (** Print the current time and date in a format similar to the "date" command *) let current_time f () = diff --git a/infer/src/base/Pp.mli b/infer/src/base/Pp.mli index ea3c94e0d..439b2ae80 100644 --- a/infer/src/base/Pp.mli +++ b/infer/src/base/Pp.mli @@ -25,7 +25,7 @@ type colormap = Obj.t -> color type simple_kind = SIM_DEFAULT | SIM_WITH_TYP (** Kind of printing *) -type print_kind = TEXT | LATEX | HTML [@@deriving compare] +type print_kind = TEXT | HTML [@@deriving compare] val equal_print_kind : print_kind -> print_kind -> bool @@ -62,9 +62,6 @@ val text : env val html : color -> env (** Default html print environment *) -val latex : color -> env -(** Default latex print environment *) - val color_string : color -> string (** string representation of colors *) @@ -76,10 +73,10 @@ val cli_args : F.formatter -> string list -> unit (** pretty print command line arguments, expanding argument files to print their contents *) val seq : - ?print_env:env -> ?sep:string -> ?sep_html:string -> ?sep_latex:string - -> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit + ?print_env:env -> ?sep:string -> ?sep_html:string -> (F.formatter -> 'a -> unit) -> F.formatter + -> 'a list -> unit (** Pretty print a sequence with [sep] followed by a space between each element. By default, - [print_env] is [text], [sep] is "", and [sep_html] and [sep_latex] set to [sep]. *) + [print_env] is [text], [sep] is "", and [sep_html] set to [sep]. *) val comma_seq : ?print_env:env -> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit (** Pretty print a comma-separated sequence. *) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 81dacf2f9..b43bcd103 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -424,7 +424,7 @@ module AliasMap = struct let pp : F.formatter -> t -> unit = fun fmt x -> let pp_sep fmt () = F.fprintf fmt ", @," in - let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k AliasTarget.pp v in + let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Ident.pp k AliasTarget.pp v in (* F.fprintf fmt "@[Logical Variables :@,"; *) F.fprintf fmt "@[{ @," ; F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ;