Reimplement command line options

Summary:
Reimplement command line options in preparation for uniformly passing
options from the top-level infer driver that invokes a build command
through the build system to the descendant infer processes.

All command line options of all executables are collected into Config,
and declared using a new CommandLineOption module that supports
maintining backward compatibility with the current command line
interface.  Very few values representing command line options are
mutable now, as they are set once during parsing but are constant
thereafter.  All ordering dependencies are contained within the
implementation of Config, and the implementation of Config is careful to
avoid unintended interactions and ordering dependencies between options.

Reviewed By: jvillard

Differential Revision: D3273345

fbshipit-source-id: 8e8c6fa
master
Josh Berdine 9 years ago committed by Facebook Github Bot 4
parent d73d4ea177
commit 3e2fa59262

@ -136,7 +136,7 @@ module Node = struct
let old_pdesc = Procname.Hash.find old_procs pname in
let changed =
(* in continue_capture mode keep the old changed bit *)
(!Config.continue_capture && old_pdesc.pd_attributes.ProcAttributes.changed) ||
(Config.continue_capture && old_pdesc.pd_attributes.ProcAttributes.changed) ||
not (pdescs_eq old_pdesc new_pdesc) in
new_pdesc.pd_attributes.changed <- changed
with Not_found -> () in
@ -937,13 +937,13 @@ let remove_abducted_retvars p =
let remove_locals (curr_f : Procdesc.t) p =
let names_of_locals = IList.map (get_name_of_local curr_f) (Procdesc.get_locals curr_f) in
let names_of_locals' = match !Config.curr_language with
| Config.C_CPP -> (* in ObjC to deal with block we need to remove static locals *)
| Config.Clang -> (* in ObjC to deal with block we need to remove static locals *)
let names_of_static_locals = get_name_of_objc_static_locals curr_f p in
let names_of_block_locals = get_name_of_objc_block_locals p in
names_of_block_locals @ names_of_locals @ names_of_static_locals
| _ -> names_of_locals in
let removed, p' = Prop.deallocate_stack_vars p names_of_locals' in
(removed, if !Config.angelic_execution then remove_abducted_retvars p' else p')
(removed, if Config.angelic_execution then remove_abducted_retvars p' else p')
let remove_formals (curr_f : Procdesc.t) p =
let pname = Procdesc.get_proc_name curr_f in
@ -1158,7 +1158,7 @@ let inline_java_synthetic_methods cfg =
let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg : cfg) =
inline_java_synthetic_methods cfg;
if save_sources then save_source_files cfg;
if !Config.incremental_procs then
if Config.incremental_procs then
begin
match load_cfg_from_file filename with
| Some old_cfg -> Node.mark_unchanged_pdescs cfg old_cfg

@ -255,11 +255,11 @@ let get_method = function
(** Return the language of the procedure. *)
let get_language = function
| ObjC_Cpp _ ->
Config.C_CPP
Config.Clang
| C _ ->
Config.C_CPP
Config.Clang
| Block _ ->
Config.C_CPP
Config.Clang
| Java _ ->
Config.Java

@ -238,7 +238,7 @@ module Subtype = struct
| NORMAL -> ""
let pp f (t, flag) =
if !Config.print_types then
if Config.print_types then
match t with
| Exact ->
F.fprintf f "%s" (flag_to_string flag)
@ -428,7 +428,7 @@ module Subtype = struct
and in case return the updated subtype [st1] *)
let case_analysis (c1, st1) (c2, st2) f is_interface =
let f = check_subtype f in
if (!Config.subtype_multirange) then
if Config.subtype_multirange then
get_subtypes (c1, st1) (c2, st2) f is_interface
else case_analysis_basic (c1, st1) (c2, st2) f
@ -1662,7 +1662,7 @@ module HpredSet = Set.Make
(** Begin change color if using diff printing, return updated printenv and change status *)
let color_pre_wrapper pe f x =
if !Config.print_using_diff && pe.pe_kind != PP_TEXT then begin
if Config.print_using_diff && pe.pe_kind != PP_TEXT then begin
let color = pe.pe_cmap_norm (Obj.repr x) in
if color != pe.pe_color then begin
(if pe.pe_kind == PP_HTML then Io_infer.Html.pp_start_color else Latex.pp_color) f color;
@ -1681,7 +1681,7 @@ let color_post_wrapper changed pe f =
(** Print a sequence with difference mode if enabled. *)
let pp_seq_diff pp pe0 f =
if not !Config.print_using_diff
if not Config.print_using_diff
then pp_comma_seq pp f
else
let rec doit = function
@ -1780,7 +1780,7 @@ let ptr_kind_string = function
| Pk_objc_autoreleasing -> "__autoreleasing *"
let java () = !Config.curr_language = Config.Java
let eradicate_java () = !Config.eradicate && java ()
let eradicate_java () = Config.eradicate && java ()
(** convert a dexp to a string *)
let rec dexp_to_string = function
@ -1878,7 +1878,7 @@ and attribute_to_string pe = function
| Racquire, Rlock -> "LOCKED"
| Rrelease, Rlock -> "UNLOCKED" in
let str_vpath =
if !Config.trace_error
if Config.trace_error
then pp_to_string (pp_vpath pe) ra.ra_vpath
else "" in
name ^ (str_binop pe Lt) ^ Procname.to_string ra.ra_pname ^ ":" ^
@ -1927,7 +1927,7 @@ and pp_const pe f = function
(** Pretty print a type. Do nothing by default. *)
and pp_typ pe f te =
if !Config.print_types then pp_typ_full pe f te else ()
if Config.print_types then pp_typ_full pe f te else ()
and pp_struct_typ pe pp_base f struct_typ = match struct_typ.struct_name with
| Some name when false ->
@ -2004,7 +2004,7 @@ and _pp_exp pe0 pp_t f e0 =
| Const c -> F.fprintf f "%a" (pp_const pe) c
| Cast (typ, e) -> F.fprintf f "(%a)%a" pp_t typ pp_exp e
| UnOp (op, e, _) -> F.fprintf f "%s%a" (str_unop op) pp_exp e
| BinOp (op, Const c, e2) when !Config.smt_output -> print_binop_stm_output (Const c) op e2
| BinOp (op, Const c, e2) when Config.smt_output -> print_binop_stm_output (Const c) op e2
| BinOp (op, e1, e2) -> F.fprintf f "(%a %s %a)" pp_exp e1 (str_binop pe op) pp_exp e2
| Lvar pv -> Pvar.pp pe f pv
| Lfield (e, fld, _) -> F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld
@ -2569,7 +2569,7 @@ let pp_inst pe f inst =
F.fprintf f "%s%s%s" (str_binop pe Lt) str (str_binop pe Gt)
let pp_inst_if_trace pe f inst =
if !Config.trace_error then pp_inst pe f inst
if Config.trace_error then pp_inst pe f inst
(** pretty print a strexp with an optional predicate env *)
let rec pp_sexp_env pe0 envo f se =
@ -3779,7 +3779,7 @@ let exp_add_offsets exp offsets =
(** Convert all the lseg's in sigma to nonempty lsegs. *)
let sigma_to_sigma_ne sigma : (atom list * hpred list) list =
if !Config.nelseg then
if Config.nelseg then
let f eqs_sigma_list hpred = match hpred with
| Hpointsto _ | Hlseg(Lseg_NE, _, _, _, _) | Hdllseg(Lseg_NE, _, _, _, _, _, _) ->
let g (eqs, sigma) = (eqs, hpred:: sigma) in

@ -0,0 +1,378 @@
(*
* Copyright (c) 2016 - 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.
*)
(** Definition and parsing of command line arguments *)
open! Utils
module F = Format
(* Each command line option may appear in the --help list of any executable, these tags are used to
specify which executables for which an option will be documented. *)
type exe = A | C | J | L | P | T
let current_exe =
match Filename.basename Sys.executable_name with
| "InferAnalyze" -> A
| "InferClang" -> C
| "InferJava" -> J
| "InferLLVM" -> L
| "InferPrint" -> P
| _ -> T
type desc = { long: string; short: string; meta: string; doc: string; spec: Arg.spec }
let dashdash long =
match long with
| "" | "--" -> long
| _ -> "--" ^ long
let short_meta {short; meta; spec} =
String.concat " "
((if short = "" then [] else ["| -" ^ short]) @
(match spec with
| Arg.Symbol (symbols, _) ->
["{ " ^ (String.concat " | " symbols) ^ " }" ^ meta]
| _ ->
if meta = "" then [] else ["<" ^ meta ^ ">"]))
let left_length long short_meta =
(String.length (dashdash long)) + (String.length short_meta)
let max_left_length limit current ({long; spec} as desc) =
let short_meta =
match spec with
| Arg.Symbol _ -> short_meta {desc with spec = Arg.Unit (fun () -> ())}
| _ -> short_meta desc in
let length = left_length long short_meta in
if length > limit then current else max current length
let xdesc {long; short; spec; doc} =
let key long short =
match long, short with
| "", "" -> ""
| "--", _ -> "--"
| "", _ -> "-" ^ short
| _ -> "--" ^ long
in
let xspec long spec =
match spec with
(* translate Symbol to String for better formatting of --help messages *)
| Arg.Symbol (symbols, action) ->
Arg.String (fun arg ->
if IList.mem ( = ) arg symbols then
action arg
else
raise (Arg.Bad (F.sprintf "wrong argument '%s'; option '%s' expects one of: %s"
arg (dashdash long) (String.concat " | " symbols)))
)
| _ ->
spec
in
(key long short, xspec long spec, doc)
let pad_and_xform left_width desc =
match desc with
| {doc = ""} ->
xdesc desc
| {long; doc} ->
let short_meta = short_meta desc in
let gap = left_width - (left_length long short_meta) in
if gap < 0 then
xdesc {desc with doc = short_meta ^ "\n" ^ (String.make (4 + left_width) ' ') ^ doc}
else
xdesc {desc with doc = short_meta ^ (String.make (gap + 1) ' ') ^ doc}
let align ?(limit=max_int) desc_list =
let left_width = IList.fold_left (max_left_length limit) 0 desc_list in
(IList.map (pad_and_xform left_width) desc_list)
let check_no_duplicates desc_list =
let rec check_for_duplicates_ = function
| [] | [_] ->
true
| (x, _, _) :: (y, _, _) :: _ when x <> "" && x = y ->
failwith ("Multiple definitions of command line option: " ^ x)
| _ :: tl ->
check_for_duplicates_ tl
in
check_for_duplicates_ (IList.sort (fun (x, _, _) (y, _, _) -> String.compare x y) desc_list)
let full_desc_list = ref []
let exe_desc_lists = [(A, ref []); (C, ref []); (J, ref []); (L, ref []); (P, ref []); (T, ref [])]
(* add desc to all desc_lists for the purposes of parsing, include desc in --help only for exes *)
let add exes desc =
full_desc_list := desc :: !full_desc_list ;
IList.iter (fun (exe, desc_list) ->
let desc =
if IList.mem ( = ) exe exes then
desc
else
{desc with meta = ""; doc = ""} in
desc_list := desc :: !desc_list
) exe_desc_lists
let mk ?(deprecated=[]) ?(exes=[])
~long ?(short="") ~default ~meta doc ~default_to_string ~mk_setter ~mk_spec =
let variable = ref default in
let closure = mk_setter variable in
let setter str =
try closure str
with _ -> raise (Arg.Bad ("bad value " ^ str ^ " for flag " ^ long)) in
let spec = mk_spec setter in
let doc =
let default_string = default_to_string default in
if default_string = "" then doc
else doc ^ " (default: " ^ default_string ^ ")" in
let desc = {long; short; meta; doc; spec} in
(* add desc for long option, with documentation (which includes any short option) for exes *)
add exes desc ;
(* add desc for short option only for parsing, without documentation *)
if short <> "" then
add [] {desc with long = ""; meta = ""; doc = ""} ;
(* add desc for deprecated options only for parsing, without documentation *)
IList.iter (fun deprecated ->
add [] {desc with long = ""; short = deprecated; meta = ""; doc = ""}
) deprecated ;
variable
type 'a t =
?deprecated:string list -> long:Arg.key -> ?short:Arg.key ->
?exes:exe list -> ?meta:string -> Arg.doc ->
'a
let mk_set var value ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
let setter () = var := value in
ignore(
mk ~deprecated ~long ?short ~default:() ?exes ~meta doc
~default_to_string:(fun () -> "")
~mk_setter:(fun _ _ -> setter ())
~mk_spec:(fun _ -> Arg.Unit setter) )
let mk_option ?(default=None) ?(default_to_string=fun _ -> "") ~f
?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
mk ~deprecated ~long ?short ~default ?exes ~meta doc
~default_to_string
~mk_setter:(fun var str -> var := f str)
~mk_spec:(fun set -> Arg.String set)
let mk_bool ?(deprecated_no=[]) ?(default=false) ?(f=fun b -> b)
?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
let nolong =
let len = String.length long in
if len > 3 && String.sub long 0 3 = "no-" then
String.sub long 3 (len - 3)
else
"no-" ^ long
and noshort =
Option.map (fun short ->
let len = String.length short in
if len > 1 && String.sub short 0 1 = "n" then
String.sub short 1 (len - 1)
else
"n" ^ short
) short
in
let doc nolong =
match noshort with
| Some noshort -> doc ^ " (Conversely: --" ^ nolong ^ " | -" ^ noshort ^ ")"
| None -> doc ^ " (Conversely: --" ^ nolong ^ ")"
in
let doc, nodoc =
if not default then
("Activates: " ^ doc nolong, "")
else
("", "Deactivates: " ^ doc long) in
let default_to_string _ = "" in
let mk_spec set = Arg.Unit (fun () -> set "") in
let var =
mk ~long ?short ~deprecated ~default ?exes
~meta doc ~default_to_string ~mk_setter:(fun var _ -> var := f true) ~mk_spec in
ignore(
mk ~long:nolong ?short:noshort ~deprecated:deprecated_no ~default:(not default) ?exes
~meta nodoc ~default_to_string ~mk_setter:(fun _ _ -> var := f false) ~mk_spec );
var
let mk_bool_group ?(deprecated_no=[]) ?(default=false)
?(deprecated=[]) ~long ?short ?exes ?(meta="") doc children =
let f b =
IList.iter (fun child -> child := b) children ;
b
in
mk_bool ~deprecated ~deprecated_no ~default ~long ?short ~f ?exes ~meta doc
let mk_int ~default ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
mk ~deprecated ~long ?short ~default ?exes ~meta doc
~default_to_string:string_of_int
~mk_setter:(fun var str -> var := (int_of_string str))
~mk_spec:(fun set -> Arg.String set)
let mk_float ~default ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
mk ~deprecated ~long ?short ~default ?exes ~meta doc
~default_to_string:string_of_float
~mk_setter:(fun var str -> var := (float_of_string str))
~mk_spec:(fun set -> Arg.String set)
let mk_string ~default ?(f=fun s -> s) ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
mk ~deprecated ~long ?short ~default ?exes ~meta doc
~default_to_string:(fun s -> s)
~mk_setter:(fun var str -> var := f str)
~mk_spec:(fun set -> Arg.String set)
let mk_string_opt ?default ?(f=fun s -> s) ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
let default_to_string = function Some s -> s | None -> "" in
let f s = Some (f s) in
mk_option ~deprecated ~long ?short ~default ~default_to_string ~f ?exes ~meta doc
let mk_string_list ?(default=[]) ?(f=fun s -> s)
?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
mk ~deprecated ~long ?short ~default ?exes ~meta doc
~default_to_string:(String.concat ", ")
~mk_setter:(fun var str -> var := (f str) :: !var)
~mk_spec:(fun set -> Arg.String set)
let mk_symbol ~default ~symbols ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
let strings = IList.map fst symbols in
let sym_to_str = IList.map (fun (x,y) -> (y,x)) symbols in
let of_string str = IList.assoc string_equal str symbols in
let to_string sym = IList.assoc ( = ) sym sym_to_str in
mk ~deprecated ~long ?short ~default ?exes ~meta doc
~default_to_string:(fun s -> to_string s)
~mk_setter:(fun var str -> var := of_string str)
~mk_spec:(fun set -> Arg.Symbol (strings, set))
let mk_symbol_opt ~symbols ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
let strings = IList.map fst symbols in
let of_string str = IList.assoc string_equal str symbols in
mk ~deprecated ~long ?short ~default:None ?exes ~meta doc
~default_to_string:(fun _ -> "")
~mk_setter:(fun var str -> var := Some (of_string str))
~mk_spec:(fun set -> Arg.Symbol (strings, set))
let mk_symbol_seq ?(default=[]) ~symbols ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc =
let strings = IList.map fst symbols in
let sym_to_str = IList.map (fun (x,y) -> (y,x)) symbols in
let of_string str = IList.assoc string_equal str symbols in
let to_string sym = IList.assoc ( = ) sym sym_to_str in
mk ~deprecated ~long ?short ~default ?exes ~meta:(" ,-separated sequence" ^ meta) doc
~default_to_string:(fun syms -> String.concat " " (IList.map to_string syms))
~mk_setter:(fun var str_seq -> var := IList.map of_string (Str.split (Str.regexp ",") str_seq))
~mk_spec:(fun set -> Arg.Symbol (strings, set))
let anon_fun = ref (fun arg -> raise (Arg.Bad ("unexpected anonymous argument: " ^ arg)))
let mk_anon () =
let anon = ref [] in
anon_fun := (fun arg -> anon := arg :: !anon) ;
anon
(** [sep_char] is used to separate elements of argv when encoded into environment variables *)
let sep_char = '^'
let encode_argv_to_env argv =
String.concat (String.make 1 sep_char)
(IList.filter (fun arg ->
not (String.contains arg sep_char)
|| (
F.eprintf "Ignoring unsupported option containing '%c' character: %s@\n" sep_char arg ;
false
)
) argv)
let decode_env_to_argv env =
Str.split (Str.regexp_string (String.make 1 sep_char)) env
let prepend_to_argv args =
let cl_args = match Array.to_list Sys.argv with _ :: tl -> tl | [] -> [] in
(Sys.executable_name, args @ cl_args)
(** [prefix_before_rest (prefix @ ["--" :: rest])] is [prefix] where "--" is not in [prefix]. *)
let prefix_before_rest args =
let rec prefix_before_rest_ rev_keep = function
| [] | "--" :: _ -> IList.rev rev_keep
| keep :: args -> prefix_before_rest_ (keep :: rev_keep) args in
prefix_before_rest_ [] args
let parse env_var exe_usage =
let curr_speclist = ref []
and full_speclist = ref []
in
let usage_msg = exe_usage current_exe
in
let curr_usage status =
Arg.usage !curr_speclist usage_msg ;
exit status
and full_usage status =
Arg.usage !full_speclist usage_msg ;
exit status
in
let help_desc_list =
[ { long = "help"; short = ""; meta = ""; spec = Arg.Unit (fun () -> curr_usage 0);
doc = "Display this list of options" }
; { long = "help-full"; short = ""; meta = ""; spec = Arg.Unit (fun () -> full_usage 0);
doc = "Display the full list of options, including internal and experimental options" }
] in
let section heading speclist =
let norm k =
let len = String.length k in
if len > 3 && String.sub k 0 3 = "no-" then String.sub k 3 (len - 3) else k in
let compare_specs {long = x} {long = y} =
match x, y with
| "--", "--" -> 0
| "--", _ -> 1
| _, "--" -> -1
| _ -> String.compare (norm x) (norm y) in
let sort speclist = IList.sort compare_specs speclist in
let add_heading speclist =
match heading with
| Some heading ->
let doc = "\n " ^ heading ^ "\n" in
{ doc; long = ""; short = ""; meta = ""; spec = Arg.Unit (fun () -> ()) } :: speclist
| None ->
speclist in
let suppress_help speclist =
("-help", Arg.Unit (fun () -> raise (Arg.Bad "unknown option '-help'")), "") :: speclist in
suppress_help (align ~limit:32 (add_heading (sort speclist)))
in
let curr_desc_list = IList.assoc ( = ) current_exe exe_desc_lists
in
(* curr_speclist includes args for current exe with docs, and all other args without docs, so
that all args can be parsed, but --help and parse failures only show external args for
current exe *)
curr_speclist := (section None (help_desc_list @ !curr_desc_list))
;
assert( check_no_duplicates !curr_speclist )
;
full_speclist := (section None (help_desc_list @ !full_desc_list))
;
let env_args = decode_env_to_argv (try Unix.getenv env_var with Not_found -> "") in
(* begin transitional support for INFERCLANG_ARGS *)
let c_args =
Str.split (Str.regexp_string (String.make 1 ':'))
(try Unix.getenv "INFERCLANG_ARGS" with Not_found -> "") in
let env_args = c_args @ env_args in
(* end transitional support for INFERCLANG_ARGS *)
let exe_name, env_cl_args = prepend_to_argv env_args in
Unix.putenv env_var (encode_argv_to_env (prefix_before_rest env_cl_args)) ;
(try
Arg.parse_argv (Array.of_list (exe_name :: env_cl_args)) !curr_speclist !anon_fun usage_msg
with
| Arg.Bad usage_msg -> Pervasives.prerr_string usage_msg; exit 2
| Arg.Help usage_msg -> Pervasives.print_string usage_msg; exit 0
);
curr_usage

@ -0,0 +1,96 @@
(*
* Copyright (c) 2016 - 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.
*)
(** Definition and parsing of command line arguments *)
open! Utils
type exe = A | C | J | L | P | T
val current_exe : exe
(** The [mk_*] functions declare command line options, while [parse] parses then according to the
declared options.
The arguments of the declaration functions are largely treated uniformly:
- [long] declares the option [--long]
- [short] declares the option [-short] as an alias
- [deprecated] declares the option [-key] as an alias, for each [key] in [deprecated]
- [default] specifies the default value
- [default_to_string] is used to document the default value
- [f] specifies a transformation to be performed on the parsed value before setting the config
variable
- [symbols] is an association list sometimes used in place of [f]
- [exes] declares that the option should be included in the external documentation (--help) for
each [exe] in [exes], otherwise it appears only in --help-full
- [meta] is a meta-variable naming the parsed value for documentation purposes
- a documentation string
*)
type 'a t =
?deprecated:string list -> long:string -> ?short:string ->
?exes:exe list -> ?meta:string -> string ->
'a
(** [mk_set variable value] defines a command line option which sets [variable] to [value]. *)
val mk_set : 'a ref -> 'a -> unit t
val mk_option :
?default:'a option -> ?default_to_string:('a option -> string) -> f:(string -> 'a option) ->
'a option ref t
(** [mk_bool long short doc] defines a [bool ref] set by the command line flag [--long] (and
[-short]), and cleared by the flag [--no-long] (and [-nshort]). If [long] already has a "no-",
or [short] nas an "n", prefix, then the existing prefixes will instead be removed. The default
value is [false] unless overridden by [~default:true]. The [doc] string will be prefixed with
either "Activates:" or "Deactivates:", so should be phrased accordingly. *)
val mk_bool : ?deprecated_no:string list -> ?default:bool -> ?f:(bool -> bool) -> bool ref t
(** [mk_bool_group children] behaves as [mk_bool] with the addition that all the [children] are also
set. A child can be unset by including "--no-child" later in the arguments. *)
val mk_bool_group : ?deprecated_no:string list -> ?default:bool -> (bool ref list -> bool ref) t
val mk_int : default:int -> int ref t
val mk_float : default:float -> float ref t
val mk_string : default:string -> ?f:(string -> string) -> string ref t
val mk_string_opt : ?default:string -> ?f:(string -> string) -> string option ref t
(** [mk_string_list] defines a [string list ref], initialized to [[]] unless overridden by
[~default]. Each argument of an occurrence of the option will be prepended to the list, so the
final value will be in the reverse order they appeared on the command line. *)
val mk_string_list :
?default:string list -> ?f:(string -> string) -> string list ref t
(** [mk_symbol long symbols] defines a command line flag [--long <symbol>] where [(<symbol>,_)] is
an element of [symbols]. *)
val mk_symbol : default:'a -> symbols:(string * 'a) list -> 'a ref t
(** [mk_symbol_opt] is similar to [mk_symbol] but defaults to [None]. *)
val mk_symbol_opt : symbols:(string * 'a) list -> 'a option ref t
(** [mk_symbol_seq long symbols] defines a command line flag [--long <symbol sequence>] where
[<symbol sequence>] is a comma-separated sequence of [<symbol>]s such that [(<symbol>,_)] is an
element of [symbols]. *)
val mk_symbol_seq : ?default:'a list -> symbols:(string * 'a) list -> 'a list ref t
(** [mk_anon ()] defines a [string list ref] of the anonymous command line arguments, in the reverse
order they appeared on the command line. *)
val mk_anon :
unit ->
string list ref
(** [parse env_var exe_usage] parses command line arguments as specified by preceding calls to the
[mk_*] functions, and returns a function that prints the usage message and help text then exits.
The decoded value of environment variable [env_var] is prepended to [Sys.argv] before parsing.
Therefore arguments passed on the command line supercede those specified in the environment
variable. WARNING: If an argument appears both in the environment variable and on the command
line, it will be interpreted twice. *)
val parse : string -> (exe -> Arg.usage_msg) -> (int -> 'a)

@ -71,8 +71,8 @@ let source_file_to_string fname =
exception No_project_root
let project_root () =
match !Config.project_root with
| None -> L.err "No -project_root option passed@."; raise No_project_root
match Config.project_root with
| None -> L.err "No --project-root option passed@."; raise No_project_root
| Some path -> path
(* Checking if the path exists may be needed only in some cases, hence the flag check_exists *)
@ -122,10 +122,10 @@ let source_dir_get_internal_file source_dir extension =
Filename.concat source_dir fname
let captured_dir () =
Filename.concat !Config.results_dir Config.captured_dir_name
Filename.concat Config.results_dir Config.captured_dir_name
let sources_dir () =
Filename.concat !Config.results_dir Config.sources_dir_name
Filename.concat Config.results_dir Config.sources_dir_name
(** get the source directory corresponding to a source file *)
let source_dir_from_source_file source_file =
@ -295,7 +295,7 @@ module Results_dir = struct
(** convert a path to a filename *)
let path_to_filename pk path =
let base = match pk with
| Abs_root -> !Config.results_dir
| Abs_root -> Config.results_dir
| Abs_source_dir ->
let dir = source_dir_from_source_file !current_source in
source_dir_to_string dir
@ -307,7 +307,7 @@ module Results_dir = struct
(** initialize the results directory *)
let init () =
create_dir !Config.results_dir;
create_dir Config.results_dir;
create_dir (specs_dir ());
create_dir (path_to_filename Abs_root [Config.attributes_dir_name]);
create_dir (path_to_filename Abs_root [Config.sources_dir_name]);

@ -38,10 +38,10 @@ let pp_failure_kind fmt = function
(** Count the number of symbolic operations *)
(** Timeout in seconds for each function *)
let timeout_seconds = ref (!Config.seconds_per_iteration *. (float_of_int !Config.iterations))
let timeout_seconds = ref (Config.seconds_per_iteration *. (float_of_int Config.iterations))
(** Timeout in SymOps *)
let timeout_symops = ref (!Config.symops_per_iteration * !Config.iterations)
let timeout_symops = ref (Config.symops_per_iteration * Config.iterations)
let get_timeout_seconds () = !timeout_seconds

@ -211,7 +211,7 @@ let mk_rule_lsls_ls k1 k2 impl_ok1 impl_ok2 para =
r_condition = condition }
let mk_rules_for_sll (para : Sil.hpara) : rule list =
if not !Config.nelseg then
if not Config.nelseg then
begin
let pts_pts = mk_rule_ptspts_ls true true para in
let pts_pels = mk_rule_ptsls_ls Sil.Lseg_PE true false para in
@ -384,7 +384,7 @@ let mk_rule_dlldll_dll k1 k2 impl_ok1 impl_ok2 para =
r_condition = condition }
let mk_rules_for_dll (para : Sil.hpara_dll) : rule list =
if not !Config.nelseg then
if not Config.nelseg then
begin
let pts_pts = mk_rule_ptspts_dll true true para in
let pts_pedll = mk_rule_ptsdll_dll Sil.Lseg_PE true false para in
@ -1026,7 +1026,7 @@ let check_observer_is_unsubscribed_deallocation prop e =
match Prop.get_observer_attribute prop e with
| Some Sil.Aobserver ->
(match pvar_opt with
| Some pvar when !Config.nsnotification_center_checker_backend ->
| Some pvar when Config.nsnotification_center_checker_backend ->
L.d_strln (" ERROR: Object " ^ (Pvar.to_string pvar) ^
" is being deallocated while still registered in a notification center");
let desc = Localise.desc_registered_observer_being_deallocated pvar loc in
@ -1109,8 +1109,8 @@ let check_junk ?original_prop pname tenv prop =
match resource with
| Sil.Rmemory Sil.Mobjc -> should_raise_objc_leak hpred
| Sil.Rmemory Sil.Mnew | Sil.Rmemory Sil.Mnew_array
when !Config.curr_language = Config.C_CPP ->
Mleak_buckets.should_raise_cpp_leak ()
when !Config.curr_language = Config.Clang ->
Mleak_buckets.should_raise_cpp_leak
| _ -> None in
let exn_retain_cycle cycle =
let cycle_dotty = get_retain_cycle_dotty original_prop cycle in
@ -1137,7 +1137,7 @@ let check_junk ?original_prop pname tenv prop =
ignore_cycle, exn_retain_cycle cycle
| Some _, Sil.Rmemory Sil.Mobjc
| Some _, Sil.Rmemory Sil.Mnew
| Some _, Sil.Rmemory Sil.Mnew_array when !Config.curr_language = Config.C_CPP ->
| Some _, Sil.Rmemory Sil.Mnew_array when !Config.curr_language = Config.Clang ->
ml_bucket_opt = None, exn_leak
| Some _, Sil.Rmemory _ -> !Config.curr_language = Config.Java, exn_leak
| Some _, Sil.Rignore -> true, exn_leak
@ -1160,7 +1160,7 @@ let check_junk ?original_prop pname tenv prop =
(* None attribute only reported if it's the first one *)
IList.mem attr_opt_equal alloc_attribute !leaks_reported in
let ignore_leak =
!Config.allowleak || ignore_resource || is_undefined || already_reported () in
!Config.allow_leak || ignore_resource || is_undefined || already_reported () in
let report_and_continue =
!Config.curr_language = Config.Java || !Config.footprint in
let report_leak () =

@ -321,7 +321,7 @@ let generic_strexp_abstract
try
let matched, footprint_part, matchings_cur_fp' = match_select_next matchings_cur_fp in
let n = IList.length (snd matchings_cur_fp') + 1 in
if !Config.trace_absarray then (L.d_strln ("Num of fp candidates " ^ (string_of_int n)));
if Config.trace_absarray then (L.d_strln ("Num of fp candidates " ^ (string_of_int n)));
let strexp_data = StrexpMatch.get_data matched in
let p1, changed = do_abstract footprint_part p0 strexp_data in
if changed then (p1, true)
@ -331,7 +331,8 @@ let generic_strexp_abstract
let rec find_then_abstract bound p0 =
if bound = 0 then p0
else begin
if !Config.trace_absarray then (L.d_strln ("Applying " ^ abstraction_name ^ " to"); Prop.d_prop p0; L.d_ln (); L.d_ln ());
if Config.trace_absarray then
(L.d_strln ("Applying " ^ abstraction_name ^ " to"); Prop.d_prop p0; L.d_ln (); L.d_ln ());
let matchings_cur_fp = find_strexp_to_abstract p0 in
let p1, changed = match_abstract p0 matchings_cur_fp in
if changed then find_then_abstract (bound - 1) p1 else p0
@ -443,19 +444,21 @@ let strexp_can_abstract ((_, se, typ) : StrexpMatch.strexp_data) : bool =
(** This function abstracts a strexp *)
let strexp_do_abstract
footprint_part p ((path, se_in, _) : StrexpMatch.strexp_data) : Prop.normal Prop.t * bool =
if !Config.trace_absarray && footprint_part then (L.d_str "strexp_do_abstract (footprint)"; L.d_ln ());
if !Config.trace_absarray && not footprint_part then (L.d_str "strexp_do_abstract (nonfootprint)"; L.d_ln ());
if Config.trace_absarray && footprint_part then
(L.d_str "strexp_do_abstract (footprint)"; L.d_ln ());
if Config.trace_absarray && not footprint_part then
(L.d_str "strexp_do_abstract (nonfootprint)"; L.d_ln ());
let prune_and_blur d_keys keep blur path keep_keys blur_keys =
let p2, changed2 =
if !Config.trace_absarray then (L.d_str "keep "; d_keys keep_keys; L.d_ln ());
if Config.trace_absarray then (L.d_str "keep "; d_keys keep_keys; L.d_ln ());
keep p path keep_keys in
let p3, changed3 =
if blur_keys == [] then (p2, false)
else begin
if !Config.trace_absarray then (L.d_str "blur "; d_keys blur_keys; L.d_ln ());
if Config.trace_absarray then (L.d_str "blur "; d_keys blur_keys; L.d_ln ());
blur p2 path blur_keys
end in
if !Config.trace_absarray then (L.d_strln "Returns"; Prop.d_prop p3; L.d_ln (); L.d_ln ());
if Config.trace_absarray then (L.d_strln "Returns"; Prop.d_prop p3; L.d_ln (); L.d_ln ());
(p3, changed2 || changed3) in
let prune_and_blur_indices =
prune_and_blur Sil.d_exp_list keep_only_indices blur_array_indices in
@ -484,7 +487,7 @@ let strexp_do_abstract
let keep_ksel = IList.filter should_keep ksel in
let keep_keys = IList.map fst keep_ksel in
let keep_keys' = if keep_keys == [] then default_keys else keep_keys in
if !Config.trace_absarray then (L.d_str "keep "; d_keys keep_keys'; L.d_ln ());
if Config.trace_absarray then (L.d_str "keep "; d_keys keep_keys'; L.d_ln ());
abstract keep_keys' [] in
let do_array_reexecution esel =
(* array case re-execution: remove and blur constant and primed indices *)

@ -24,12 +24,14 @@ let check_nested_loop path pos_opt =
let loop_visits_log = ref [] in
let in_nested_loop () = match !loop_visits_log with
| true :: true :: _ ->
if !verbose then L.d_strln "in nested loop";
if verbose then L.d_strln "in nested loop";
true (* last two loop visits were entering loops *)
| _ -> false in
let do_node_caller node = match Cfg.Node.get_kind node with
| Cfg.Node.Prune_node (b, (Sil.Ik_dowhile | Sil.Ik_for | Sil.Ik_while), _) ->
(* if !verbose then L.d_strln ((if b then "enter" else "exit") ^ " node " ^ (string_of_int (Cfg.Node.get_id node))); *)
(* if verbose then *)
(* L.d_strln ((if b then "enter" else "exit") ^ " node " *)
(* ^ (string_of_int (Cfg.Node.get_id node))); *)
loop_visits_log := b :: !loop_visits_log
| _ -> () in
let do_any_node _level _node =
@ -129,7 +131,7 @@ let check_access access_opt de_opt =
let classify_access desc access_opt de_opt is_nullable =
let default_bucket = if is_nullable then Localise.BucketLevel.b1 else Localise.BucketLevel.b5 in
let show_in_message = !Config.show_buckets in
let show_in_message = Config.show_buckets in
match check_access access_opt de_opt with
| None -> Localise.error_desc_set_bucket desc default_bucket show_in_message
| Some bucket -> Localise.error_desc_set_bucket desc bucket show_in_message

@ -54,7 +54,7 @@ let get_procedure_definition exe_env proc_name =
(idenv, tenv, proc_name, proc_desc, language))
(Exe_env.get_proc_desc exe_env proc_name)
let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.C_CPP
let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.Clang
(** Invoke all registered procedure callbacks on the given procedure. *)
let iterate_procedure_callbacks exe_env caller_pname =

@ -34,14 +34,14 @@ let cluster_should_be_analyzed cluster =
let modified =
DB.file_was_updated_after_start (DB.filename_from_string fname) in
if modified &&
!Config.developer_mode
Config.developer_mode
then L.stdout "Modified: %s@." fname;
modified in
begin
match in_ondemand_config with
| Some b -> (* ondemand config file is specified *)
b
| None when !Config.reactive_mode ->
| None when Config.reactive_mode ->
check_modified ()
| None ->
true
@ -53,7 +53,7 @@ let pp_prolog fmt clusters =
Sys.executable_name
(Escape.escape_map
(fun c -> if c = '#' then Some "\\#" else None)
!Config.results_dir);
Config.results_dir);
F.fprintf fmt "CLUSTERS=";
IList.iteri
@ -64,7 +64,7 @@ let pp_prolog fmt clusters =
F.fprintf fmt "@.@.default: test@.@.all: test@.@.";
F.fprintf fmt "test: $(CLUSTERS)@.";
if !Config.show_progress_bar then F.fprintf fmt "\techo \"\"@."
if Config.show_progress_bar then F.fprintf fmt "\techo \"\"@."
let pp_epilog fmt () =
F.fprintf fmt "@.clean:@.\trm -f $(CLUSTERS)@."

File diff suppressed because it is too large Load Diff

@ -0,0 +1,222 @@
(*
* 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! Utils
(** Configuration values: either constant, determined at compile time, or set at startup
time by system calls, environment variables, or command line options *)
type language = Clang | Java
val string_of_language : language -> string
type clang_lang = C | CPP | OBJC | OBJCPP
type os_type = Unix | Win32 | Cygwin
type zip_library = {
zip_filename : string;
zip_channel : Zip.in_file Lazy.t;
models : bool;
}
(** Configuration values *)
val allow_missing_index_in_proc_call : bool
val anonymous_block_num_sep : string
val anonymous_block_prefix : string
val assign : string
val attributes_dir_name : string
val backend_stats_dir_name : string
val bound_error_allowed_in_procedure_call : bool
val captured_dir_name : string
val default_failure_name : string
val default_in_zip_results_dir : string
val dotty_output : string
val filter_buckets : bool
val frontend_stats_dir_name : string
val global_tenv_filename : string
val idempotent_getters : bool
val incremental_procs : bool
val inferconfig_file : string
val initial_analysis_time : float
val ivar_attributes : string
val max_recursion : int
val meet_level : int
val models_dir : string
val nsnotification_center_checker_backend : bool
val objc_method_call_semantics : bool
val os_type : os_type
val perf_stats_prefix : string
val proc_stats_filename : string
val property_attributes : string
val report_nullable_inconsistency : bool
val reporting_stats_dir_name : string
val save_compact_summaries : bool
val save_time_in_summaries : bool
val smt_output : bool
val source_file_extentions : string list
val sources_dir_name : string
val specs_dir_name : string
val specs_files_suffix : string
val start_filename : string
val taint_analysis : bool
val trace_absarray : bool
val undo_join : bool
val unsafe_unret : string
val weak : string
(** Configuration values specified by environment variables *)
val from_env_variable : string -> bool
val get_env_variable : string -> string option
val analyze_models : bool
val lazy_dynamic_dispatch : bool
val report_custom_error : bool
val sound_dynamic_dispatch : bool
(** Configuration values specified by command-line options *)
val anon_args : string list
val abs_struct : int
val allow_specs_cleanup : bool
val analysis_stops : bool
val analyzer : analyzer option
val angelic_execution : bool
val array_level : int
val ast_file : string option
val bugs_csv : outfile option
val bugs_json : outfile option
val bugs_txt : outfile option
val bugs_xml : outfile option
val calls_csv : outfile option
val checkers : bool
val checkers_enabled : bool
val clang_lang : clang_lang
val cluster_cmdline : string option
val code_query : string option
val continue_capture : bool
val create_harness : bool
val cxx_experimental : bool
val debug_mode : bool
val dependency_mode : bool
val developer_mode : bool
val dotty_cfg_libs : bool
val eradicate : bool
val err_file_cmdline : string
val infer_cache : string option
val inferconfig_home : string option
val iterations : int
val javac_verbose_out : string
val join_cond : int
val latex : outfile option
val load_analysis_results : string option
val makefile_cmdline : string
val merge : bool
val ml_buckets :
[ `MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown ] list
val models_file : string option
val models_mode : bool
val modified_targets : string option
val monitor_prop_size : bool
val nelseg : bool
val no_static_final : bool
val no_translate_libs : bool
val nonstop : bool
val objc_memory_model_on : bool
val only_footprint : bool
val optimistic_cast : bool
val out_file_cmdline : string
val precondition_stats : bool
val print_builtins : bool
val print_types : bool
val print_using_diff : bool
val procs_csv : outfile option
val procs_xml : outfile option
val project_root : string option
val quiet : bool
val reactive_mode : bool
val report : outfile option
val report_runtime_exceptions : bool
val reports_include_ml_loc : bool
val results_dir : string
val save_analysis_results : string option
val seconds_per_iteration : float
val show_buckets : bool
val show_progress_bar : bool
val source_file : string option
val source_file_copy : string option
val spec_abs_level : int
val specs_library : string list
val stats_mode : bool
val subtype_multirange : bool
val suppress_warnings_annotations : string option
val svg : bool
val symops_per_iteration : int
val test : bool
val test_filtering : bool
val testing_mode : bool
val trace_error : bool
val trace_join : bool
val trace_rearrange : bool
val type_size : bool
val unit_test : bool
val whole_seconds : bool
val worklist_mode : int
val write_dotty : bool
val write_html : bool
val xml_specs : bool
val zip_libraries : zip_library list
(** Global variables *)
(** [set_reference_and_call_function ref val f x] calls f x with ref set to val.
Restore the initial value also in case of exception. *)
val set_reference_and_call_function : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
val footprint : bool ref
(** Call f x with footprint set to true.
Restore the initial value of footprint also in case of exception. *)
val run_in_footprint_mode : ('a -> 'b) -> 'a -> 'b
(** Call f x with footprint set to false.
Restore the initial value of footprint also in case of exception. *)
val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b
val forcing_delayed_prints : bool ref
val nLOC : int ref
val pp_simple : bool ref
(** Global variables with initial values specified by command-line options *)
val abs_val : int ref
val reset_abs_val : unit -> unit
(** Call f x with abs_val set to zero.
Restore the initial value also in case of exception. *)
val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b
val allow_leak : bool ref
val arc_mode : bool ref
val curr_language : language ref
(** Command Line Interface Documentation *)
val print_usage_exit : unit -> 'a

@ -254,7 +254,7 @@ module CheckJoinPre : InfoLossCheckerSig = struct
| Sil.Lvar _ -> false
| Sil.Var id when Ident.is_normal id -> IList.length es >= 1
| Sil.Var _ ->
if !Config.join_cond = 0 then
if Config.join_cond = 0 then
IList.exists (Sil.exp_equal Sil.exp_zero) es
else if Dangling.check side e then
begin
@ -689,7 +689,7 @@ end = struct
let get_other_atoms side atom_in =
let build_other_atoms construct side e =
if !Config.trace_join then (L.d_str "build_other_atoms: "; Sil.d_exp e; L.d_ln ());
if Config.trace_join then (L.d_str "build_other_atoms: "; Sil.d_exp e; L.d_ln ());
let others1 = get_others_direct_or_induced side e in
let others2 = match others1 with None -> get_others_deep side e | Some _ -> others1 in
match others2 with
@ -697,7 +697,7 @@ end = struct
| Some (e_res, e_op) ->
let a_res = construct e_res in
let a_op = construct e_op in
if !Config.trace_join then begin
if Config.trace_join then begin
L.d_str "build_other_atoms (successful) ";
Sil.d_atom a_res; L.d_str ", "; Sil.d_atom a_op; L.d_ln ()
end;
@ -1392,7 +1392,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
try
let todo_curr = Todo.pop () in
let e1, e2, e = todo_curr in
if !Config.trace_join then begin
if Config.trace_join then begin
L.d_strln ".... sigma_partial_join' ....";
L.d_str "TODO: "; Sil.d_exp e1; L.d_str ","; Sil.d_exp e2; L.d_str ","; Sil.d_exp e; L.d_ln ();
L.d_strln "SIGMA1 ="; Prop.d_sigma sigma1_in; L.d_ln ();
@ -1407,7 +1407,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
| Some (Sil.Hlseg (k, _, _, _, _) as lseg), None
| Some (Sil.Hdllseg (k, _, _, _, _, _, _) as lseg), None ->
if (not !Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then
if (not Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then
let sigma_acc' = join_list_and_non Lhs e lseg e1 e2 :: sigma_acc in
sigma_partial_join' mode sigma_acc' sigma1 sigma2
else
@ -1415,7 +1415,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
| None, Some (Sil.Hlseg (k, _, _, _, _) as lseg)
| None, Some (Sil.Hdllseg (k, _, _, _, _, _, _) as lseg) ->
if (not !Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then
if (not Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then
let sigma_acc' = join_list_and_non Rhs e lseg e2 e1 :: sigma_acc in
sigma_partial_join' mode sigma_acc' sigma1 sigma2
else
@ -1643,21 +1643,23 @@ let pi_partial_join mode
| Sil.Aneq _ -> false
| e -> Prop.atom_is_inequality e in
begin
if !Config.trace_join then begin
if Config.trace_join then begin
L.d_str "pi1: "; Prop.d_pi pi1; L.d_ln ();
L.d_str "pi2: "; Prop.d_pi pi2; L.d_ln ()
end;
let atom_list1 =
let p2 = Prop.normalize ep2 in
IList.fold_left (handle_atom_with_widening Lhs p2 pi2) [] pi1 in
if !Config.trace_join then (L.d_str "atom_list1: "; Prop.d_pi atom_list1; L.d_ln ());
if Config.trace_join then (L.d_str "atom_list1: "; Prop.d_pi atom_list1; L.d_ln ());
let atom_list_combined =
let p1 = Prop.normalize ep1 in
IList.fold_left (handle_atom_with_widening Rhs p1 pi1) atom_list1 pi2 in
if !Config.trace_join then (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ());
if Config.trace_join then
(L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ());
let atom_list_filtered =
IList.filter filter_atom atom_list_combined in
if !Config.trace_join then (L.d_str "atom_list_filtered: "; Prop.d_pi atom_list_filtered; L.d_ln ());
if Config.trace_join then
(L.d_str "atom_list_filtered: "; Prop.d_pi atom_list_filtered; L.d_ln ());
let atom_list_res =
IList.rev atom_list_filtered in
atom_list_res
@ -2001,7 +2003,7 @@ let proplist_meet_generate plist =
let propset_meet_generate_pre pset =
let plist = Propset.to_proplist pset in
if !Config.meet_level = 0 then plist
if Config.meet_level = 0 then plist
else
let pset1 = proplist_meet_generate plist in
let pset_new = Propset.diff pset1 pset in

@ -1007,7 +1007,7 @@ let pp_cfgnode fmt (n: Cfg.Node.t) =
let print_icfg fmt cfg =
let print_node node =
let loc = Cfg.Node.get_loc node in
if (!Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file !DB.current_source) then
if (Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file !DB.current_source) then
F.fprintf fmt "%a\n" pp_cfgnode node in
IList.iter print_node (Cfg.Node.get_all_nodes cfg)
@ -1019,7 +1019,10 @@ let print_edges fmt edges =
IList.iter print_edge edges
let print_icfg_dotty cfg (extra_edges : (Cfg.Node.t * Cfg.Node.t) list) =
let chan = open_out (DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [!Config.dotty_output])) in
let chan =
open_out
(DB.filename_to_string
(DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [Config.dotty_output])) in
let fmt = Format.formatter_of_out_channel chan in
F.fprintf fmt "digraph iCFG {\n";
print_icfg fmt cfg;

@ -127,7 +127,7 @@ let find_normal_variable_funcall
true
| _ -> false in
ignore (IList.exists find_declaration node_instrs);
if !verbose && !res == None
if verbose && !res == None
then
(L.d_str
("find_normal_variable_funcall could not find " ^
@ -235,7 +235,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
let node_instrs = Cfg.Node.get_instrs node in
let find_declaration = function
| Sil.Letderef (id0, e, _, _) when Ident.equal id id0 ->
if !verbose
if verbose
then
(L.d_str "find_normal_variable_letderef defining ";
Sil.d_exp e; L.d_ln ());
@ -243,7 +243,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
true
| Sil.Call ([id0], Sil.Const (Sil.Cfun pn), (e, _):: _, _, _)
when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") ->
if !verbose
if verbose
then
(L.d_str "find_normal_variable_letderef cast on ";
Sil.d_exp e; L.d_ln ());
@ -251,7 +251,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
true
| Sil.Call ([id0], (Sil.Const (Sil.Cfun pname) as fun_exp), args, loc, call_flags)
when Ident.equal id id0 ->
if !verbose
if verbose
then
(L.d_str "find_normal_variable_letderef function call ";
Sil.d_exp fun_exp; L.d_ln ());
@ -269,7 +269,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
true
| _ -> false in
ignore (IList.exists find_declaration node_instrs);
if !verbose && !res == None
if verbose && !res == None
then
(L.d_str
("find_normal_variable_letderef could not find " ^
@ -287,20 +287,20 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
let seen = Sil.ExpSet.add e _seen in
match Prop.exp_normalize_noabs Sil.sub_empty e with
| Sil.Const c ->
if !verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ());
Some (Sil.Dderef (Sil.Dconst c))
| Sil.BinOp(Sil.PlusPI, e1, e2) ->
if !verbose then (L.d_str "exp_lv_dexp: (e1 +PI e2) "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_lv_dexp: (e1 +PI e2) "; Sil.d_exp e; L.d_ln ());
(match _exp_lv_dexp seen node e1, _exp_rv_dexp seen node e2 with
| Some de1, Some de2 -> Some (Sil.Dbinop(Sil.PlusPI, de1, de2))
| _ -> None)
| Sil.Var id when Ident.is_normal id ->
if !verbose then (L.d_str "exp_lv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_lv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
(match _find_normal_variable_letderef seen node id with
| None -> None
| Some de -> Some (Sil.Dderef de))
| Sil.Lvar pvar ->
if !verbose then (L.d_str "exp_lv_dexp: program var "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_lv_dexp: program var "; Sil.d_exp e; L.d_ln ());
if pvar_is_frontend_tmp pvar then
begin
match find_program_variable_assignment node pvar with
@ -322,7 +322,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
end
else Some (Sil.Dpvar pvar)
| Sil.Lfield (Sil.Var id, f, _) when Ident.is_normal id ->
if !verbose then
if verbose then
begin
L.d_str "exp_lv_dexp: Lfield with var ";
Sil.d_exp (Sil.Var id);
@ -333,7 +333,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
| None -> None
| Some de -> Some (Sil.Darrow (de, f)))
| Sil.Lfield (e1, f, _) ->
if !verbose then
if verbose then
begin
L.d_str "exp_lv_dexp: Lfield ";
Sil.d_exp e1;
@ -344,7 +344,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
| None -> None
| Some de -> Some (Sil.Ddot (de, f)))
| Sil.Lindex (e1, e2) ->
if !verbose then
if verbose then
begin
L.d_str "exp_lv_dexp: Lindex ";
Sil.d_exp e1;
@ -359,7 +359,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
Some (Sil.Darray (de1, Sil.Dunknown))
| Some de1, Some de2 -> Some (Sil.Darray (de1, de2)))
| _ ->
if !verbose then (L.d_str "exp_lv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_lv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
None
(** describe rvalue [e] as a dexp *)
@ -370,18 +370,18 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
let seen = Sil.ExpSet.add e _seen in
match e with
| Sil.Const c ->
if !verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ());
Some (Sil.Dconst c)
| Sil.Lvar pv ->
if !verbose then (L.d_str "exp_rv_dexp: program var "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_rv_dexp: program var "; Sil.d_exp e; L.d_ln ());
if pvar_is_frontend_tmp pv
then _exp_lv_dexp _seen (* avoid spurious cycle detection *) node e
else Some (Sil.Dpvaraddr pv)
| Sil.Var id when Ident.is_normal id ->
if !verbose then (L.d_str "exp_rv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_rv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
_find_normal_variable_letderef seen node id
| Sil.Lfield (e1, f, _) ->
if !verbose then
if verbose then
begin
L.d_str "exp_rv_dexp: Lfield ";
Sil.d_exp e1;
@ -392,7 +392,7 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
| None -> None
| Some de -> Some (Sil.Ddot(de, f)))
| Sil.Lindex (e1, e2) ->
if !verbose then
if verbose then
begin
L.d_str "exp_rv_dexp: Lindex ";
Sil.d_exp e1;
@ -404,23 +404,23 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
| None, _ | _, None -> None
| Some de1, Some de2 -> Some (Sil.Darray(de1, de2)))
| Sil.BinOp (op, e1, e2) ->
if !verbose then (L.d_str "exp_rv_dexp: BinOp "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_rv_dexp: BinOp "; Sil.d_exp e; L.d_ln ());
(match _exp_rv_dexp seen node e1, _exp_rv_dexp seen node e2 with
| None, _ | _, None -> None
| Some de1, Some de2 -> Some (Sil.Dbinop (op, de1, de2)))
| Sil.UnOp (op, e1, _) ->
if !verbose then (L.d_str "exp_rv_dexp: UnOp "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_rv_dexp: UnOp "; Sil.d_exp e; L.d_ln ());
(match _exp_rv_dexp seen node e1 with
| None -> None
| Some de1 -> Some (Sil.Dunop (op, de1)))
| Sil.Cast (_, e1) ->
if !verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ());
_exp_rv_dexp seen node e1
| Sil.Sizeof (typ, sub) ->
if !verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ());
Some (Sil.Dsizeof (typ, sub))
| _ ->
if !verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
None
let find_normal_variable_letderef = _find_normal_variable_letderef Sil.ExpSet.empty
@ -536,10 +536,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
| _ -> false in
let value_str = match instro with
| None ->
if !verbose then (L.d_str "explain_leak: no current instruction"; L.d_ln ());
if verbose then (L.d_str "explain_leak: no current instruction"; L.d_ln ());
value_str_from_pvars_vpath [] vpath
| Some (Sil.Nullify (pvar, _)) when check_pvar pvar ->
if !verbose
if verbose
then
(L.d_str "explain_leak: current instruction is Nullify for pvar ";
Pvar.d pvar; L.d_ln ());
@ -547,10 +547,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
| None -> None
| Some de -> Some (Sil.dexp_to_string de))
| Some (Sil.Abstract _) ->
if !verbose then (L.d_str "explain_leak: current instruction is Abstract"; L.d_ln ());
if verbose then (L.d_str "explain_leak: current instruction is Abstract"; L.d_ln ());
let get_nullify = function
| Sil.Nullify (pvar, _) when check_pvar pvar ->
if !verbose
if verbose
then
(L.d_str "explain_leak: found nullify before Abstract for pvar ";
Pvar.d pvar; L.d_ln ());
@ -561,7 +561,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
IList.filter (fun pvar -> not (pvar_is_frontend_tmp pvar)) nullify_pvars in
value_str_from_pvars_vpath nullify_pvars_notmp vpath
| Some (Sil.Set (lexp, _, _, _)) when vpath = None ->
if !verbose
if verbose
then
(L.d_str "explain_leak: current instruction Set for ";
Sil.d_exp lexp; L.d_ln ());
@ -569,7 +569,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
| Some dexp -> Some (Sil.dexp_to_string dexp)
| None -> None)
| Some instr ->
if !verbose
if verbose
then
(L.d_str "explain_leak: case not matched in instr ";
Sil.d_instr instr; L.d_ln());
@ -584,13 +584,13 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(* we don't know it's been allocated,
but it's coming from list abstraction and we have a name *)
Exceptions.Exn_user, bucket
else Exceptions.Exn_developer, Some (Mleak_buckets.ml_bucket_unknown_origin ()) in
else Exceptions.Exn_developer, Some Mleak_buckets.ml_bucket_unknown_origin in
exn_cat, Localise.desc_leak hpred_typ_opt value_str resource_opt res_action_opt loc bucket
(** find the dexp, if any, where the given value is stored
also return the type of the value if found *)
let vpath_find prop _exp : Sil.dexp option * Sil.typ option =
if !verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ());
if verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ());
let rec find sigma_acc sigma_todo exp =
let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with
| Sil.Eexp (e, _) when Sil.exp_equal exp e ->
@ -613,7 +613,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option =
| None, _ -> ()
| Some de, typo -> res := Some (Sil.Darrow (de, f)), typo)
| lexp ->
if !verbose
if verbose
then
(L.d_str "vpath_find do_fse: no match on Eexp ";
Sil.d_exp lexp; L.d_ln ()))
@ -632,7 +632,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option =
| None, typo -> None, typo
| Some de, typo -> Some (Sil.Dderef de), typo)
| lexp ->
if !verbose
if verbose
then
(L.d_str "vpath_find do_sexp: no match on Eexp ";
Sil.d_exp lexp; L.d_ln ());
@ -665,7 +665,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option =
| Some de, typo -> Some de, typo
| None, _ -> find (hpred:: sigma_acc) sigma_todo' exp) in
let res = find [] (Prop.get_sigma prop) _exp in
if !verbose then begin
if verbose then begin
match res with
| None, _ -> L.d_str "vpath_find: cannot find "; Sil.d_exp _exp; L.d_ln ()
| Some de, typo -> L.d_str "vpath_find: found "; L.d_str (Sil.dexp_to_string de); L.d_str " : ";
@ -683,7 +683,7 @@ let explain_dexp_access prop dexp is_nullable =
| None -> None
| Some (Sil.Eexp (_, inst)) -> Some inst
| Some se ->
if !verbose then (L.d_str "sexpo_to_inst: can't find inst "; Sil.d_sexp se; L.d_ln());
if verbose then (L.d_str "sexpo_to_inst: can't find inst "; Sil.d_sexp se; L.d_ln());
None in
let find_ptsto (e : Sil.exp) : Sil.strexp option =
let res = ref None in
@ -695,7 +695,7 @@ let explain_dexp_access prop dexp is_nullable =
!res in
let rec lookup_fld fsel f = match fsel with
| [] ->
if !verbose
if verbose
then
(L.d_strln ("lookup_fld: can't find field " ^ Ident.fieldname_to_string f));
None
@ -704,7 +704,7 @@ let explain_dexp_access prop dexp is_nullable =
else lookup_fld fsel' f in
let rec lookup_esel esel e = match esel with
| [] ->
if !verbose then (L.d_str "lookup_esel: can't find index "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "lookup_esel: can't find index "; Sil.d_exp e; L.d_ln ());
None
| (e1, se):: esel' ->
if Sil.exp_equal e1 e then Some se
@ -718,7 +718,7 @@ let explain_dexp_access prop dexp is_nullable =
| Some Sil.Earray (_, esel, _), Some Sil.Eexp (e, _) ->
lookup_esel esel e
| Some se1, Some se2 ->
if !verbose
if verbose
then
(L.d_str "lookup: case not matched on Darray ";
Sil.d_sexp se1; L.d_str " "; Sil.d_sexp se2; L.d_ln());
@ -729,7 +729,7 @@ let explain_dexp_access prop dexp is_nullable =
| Some Sil.Estruct (fsel, _) ->
lookup_fld fsel f
| Some _ ->
if !verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ());
if verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ());
None)
| Sil.Ddot (de1, f) ->
(match lookup de1 with
@ -737,10 +737,10 @@ let explain_dexp_access prop dexp is_nullable =
| Some Sil.Estruct (fsel, _) ->
lookup_fld fsel f
| Some _ ->
if !verbose then (L.d_str "lookup: case not matched on Ddot "; L.d_ln ());
if verbose then (L.d_str "lookup: case not matched on Ddot "; L.d_ln ());
None)
| Sil.Dpvar pvar ->
if !verbose then (L.d_str "lookup: found Dpvar "; L.d_ln ());
if verbose then (L.d_str "lookup: found Dpvar "; L.d_ln ());
(find_ptsto (Sil.Lvar pvar))
| Sil.Dderef de ->
(match lookup de with
@ -748,24 +748,24 @@ let explain_dexp_access prop dexp is_nullable =
| Some (Sil.Eexp (e, _)) -> find_ptsto e
| Some _ -> None)
| (Sil.Dbinop(Sil.PlusPI, Sil.Dpvar _, Sil.Dconst _) as de) ->
if !verbose then (L.d_strln ("lookup: case )pvar + constant) " ^ Sil.dexp_to_string de));
if verbose then (L.d_strln ("lookup: case )pvar + constant) " ^ Sil.dexp_to_string de));
None
| Sil.Dfcall (Sil.Dconst c, _, loc, _) ->
if !verbose then (L.d_strln "lookup: found Dfcall ");
if verbose then (L.d_strln "lookup: found Dfcall ");
(match c with
| Sil.Cfun _ -> (* Treat function as an update *)
Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Location.line))
| _ -> None)
| Sil.Dretcall (Sil.Dconst (Sil.Cfun pname as c ) , _, loc, _ )
when method_of_pointer_wrapper pname ->
if !verbose then (L.d_strln "lookup: found Dretcall ");
if verbose then (L.d_strln "lookup: found Dretcall ");
Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_pointer_wrapper_call loc.Location.line))
| de ->
if !verbose then (L.d_strln ("lookup: unknown case not matched " ^ Sil.dexp_to_string de));
if verbose then (L.d_strln ("lookup: unknown case not matched " ^ Sil.dexp_to_string de));
None in
let access_opt = match sexpo_to_inst (lookup dexp) with
| None ->
if !verbose
if verbose
then
(L.d_strln ("explain_dexp_access: cannot find inst of " ^ Sil.dexp_to_string dexp));
None
@ -780,7 +780,7 @@ let explain_dexp_access prop dexp is_nullable =
| Some Sil.Ialloc when !Config.curr_language = Config.Java ->
Some Localise.Initialized_automatically
| Some inst ->
if !verbose
if verbose
then
(L.d_strln
("explain_dexp_access: inst is not an update " ^
@ -830,7 +830,7 @@ let create_dereference_desc
| _ -> access_opt in
let desc = Localise.dereference_string deref_str value_str access_opt' loc in
let desc =
if !Config.curr_language = Config.C_CPP && not is_premature_nil then
if !Config.curr_language = Config.Clang && not is_premature_nil then
match de_opt with
| Some (Sil.Dpvar pvar)
| Some (Sil.Dpvaraddr pvar) ->
@ -855,60 +855,60 @@ let _explain_access
deref_str prop loc =
let rec find_outermost_dereference node e = match e with
| Sil.Const _ ->
if !verbose then (L.d_str "find_outermost_dereference: constant "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "find_outermost_dereference: constant "; Sil.d_exp e; L.d_ln ());
exp_lv_dexp node e
| Sil.Var id when Ident.is_normal id -> (* look up the normal variable declaration *)
if !verbose
if verbose
then
(L.d_str "find_outermost_dereference: normal var ";
Sil.d_exp e; L.d_ln ());
find_normal_variable_letderef node id
| Sil.Lfield (e', _, _) ->
if !verbose then (L.d_str "find_outermost_dereference: Lfield "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "find_outermost_dereference: Lfield "; Sil.d_exp e; L.d_ln ());
find_outermost_dereference node e'
| Sil.Lindex(e', _) ->
if !verbose then (L.d_str "find_outermost_dereference: Lindex "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "find_outermost_dereference: Lindex "; Sil.d_exp e; L.d_ln ());
find_outermost_dereference node e'
| Sil.Lvar _ ->
if !verbose then (L.d_str "find_outermost_dereference: Lvar "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "find_outermost_dereference: Lvar "; Sil.d_exp e; L.d_ln ());
exp_lv_dexp node e
| Sil.BinOp(Sil.PlusPI, Sil.Lvar _, _) ->
if !verbose
if verbose
then
(L.d_str "find_outermost_dereference: Lvar+index ";
Sil.d_exp e; L.d_ln ());
exp_lv_dexp node e
| Sil.Cast (_, e') ->
if !verbose then (L.d_str "find_outermost_dereference: cast "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "find_outermost_dereference: cast "; Sil.d_exp e; L.d_ln ());
find_outermost_dereference node e'
| Sil.BinOp(Sil.PtrFld, _, e') ->
if !verbose then (L.d_str "find_outermost_dereference: PtrFld "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "find_outermost_dereference: PtrFld "; Sil.d_exp e; L.d_ln ());
find_outermost_dereference node e'
| _ ->
if !verbose
if verbose
then
(L.d_str "find_outermost_dereference: no match for ";
Sil.d_exp e; L.d_ln ());
None in
let find_exp_dereferenced () = match State.get_instr () with
| Some Sil.Set (e, _, _, _) ->
if !verbose then (L.d_str "explain_dereference Sil.Set "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "explain_dereference Sil.Set "; Sil.d_exp e; L.d_ln ());
Some e
| Some Sil.Letderef (_, e, _, _) ->
if !verbose then (L.d_str "explain_dereference Sil.Leteref "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "explain_dereference Sil.Leteref "; Sil.d_exp e; L.d_ln ());
Some e
| Some Sil.Call (_, Sil.Const (Sil.Cfun fn), [(e, _)], _, _)
when Procname.to_string fn = "free" ->
if !verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ());
Some e
| Some Sil.Call (_, (Sil.Var _ as e), _, _, _) ->
if !verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ());
if verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ());
Some e
| _ -> None in
let node = State.get_node () in
match find_exp_dereferenced () with
| None ->
if !verbose then L.d_strln "_explain_access: find_exp_dereferenced returned None";
if verbose then L.d_strln "_explain_access: find_exp_dereferenced returned None";
Localise.no_desc
| Some e ->
L.d_strln "Finding deref'd exp";
@ -1015,7 +1015,7 @@ let explain_dereference_as_caller_expression
find 1 formal_params in
match find_with_exp spec_pre exp with
| Some (pv, pvar_off) ->
if !verbose then L.d_strln ("pvar: " ^ (Pvar.to_string pv));
if verbose then L.d_strln ("pvar: " ^ (Pvar.to_string pv));
let pv_name = Pvar.get_name pv in
if Pvar.is_global pv
then
@ -1023,14 +1023,14 @@ let explain_dereference_as_caller_expression
create_dereference_desc ~use_buckets dexp deref_str actual_pre loc
else if Pvar.is_callee pv then
let position = find_formal_param_number pv_name in
if !verbose then L.d_strln ("parameter number: " ^ string_of_int position);
if verbose then L.d_strln ("parameter number: " ^ string_of_int position);
explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off
else
if Prop.has_dangling_uninit_attribute spec_pre exp then
Localise.desc_uninitialized_dangling_pointer_deref deref_str (Pvar.to_string pv) loc
else Localise.no_desc
| None ->
if !verbose
if verbose
then (L.d_str "explain_dereference_as_caller_expression ";
Sil.d_exp exp; L.d_str ": cannot explain None "; L.d_ln ());
Localise.no_desc
@ -1141,7 +1141,7 @@ let explain_null_test_after_dereference exp node line loc =
| None -> Localise.no_desc
let _warning loc fmt fmt_string =
if !Config.developer_mode then
if Config.developer_mode then
begin
F.fprintf
fmt "%s:%d: Warning: " (DB.source_file_to_string !DB.current_source) loc.Location.line;

@ -175,17 +175,17 @@ let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn =
| Some ekind -> ekind
| _ -> _ekind in
let hide_java_loc_zero = (* hide java errors at location zero unless in -developer_mode *)
!Config.developer_mode = false &&
Config.developer_mode = false &&
!Config.curr_language = Config.Java &&
loc.Location.line = 0 in
let hide_memory_error =
match Localise.error_desc_get_bucket desc with
| Some bucket when bucket = (Mleak_buckets.ml_bucket_unknown_origin ()) ->
not (Mleak_buckets.should_raise_leak_unknown_origin ())
| Some bucket when bucket = Mleak_buckets.ml_bucket_unknown_origin ->
not Mleak_buckets.should_raise_leak_unknown_origin
| _ -> false in
let log_it =
visibility == Exceptions.Exn_user ||
(!Config.developer_mode && visibility == Exceptions.Exn_developer) in
(Config.developer_mode && visibility == Exceptions.Exn_developer) in
if log_it && not hide_java_loc_zero && not hide_memory_error then begin
let added =
add_issue err_log

@ -88,7 +88,7 @@ exception Wrong_argument_number of L.ml_loc
(** Turn an exception into a descriptive string, error description, location in ml source, and category *)
let recognize_exception exn =
let filter_out_bucket desc =
!Config.filter_buckets &&
Config.filter_buckets &&
match Localise.error_desc_get_bucket desc with
| None -> false
| Some bucket -> bucket <> Localise.BucketLevel.b1 in
@ -101,7 +101,7 @@ let recognize_exception exn =
(Localise.context_leak,
desc, None, Exn_user, High, None, Nocat)
| Analysis_stops (desc, ml_loc_opt) ->
let visibility = if !Config.analysis_stops then Exn_user else Exn_developer in
let visibility = if Config.analysis_stops then Exn_user else Exn_developer in
(Localise.analysis_stops, desc, ml_loc_opt, visibility, Medium, None, Nocat)
| Array_of_pointsto ml_loc ->
(Localise.from_string "Array_of_pointsto",

@ -15,233 +15,13 @@ open! Utils
module L = Logging
module F = Format
(** command line option: if true, run the analysis in checker mode *)
let checkers = ref false
(** command line option: name of the makefile to create with clusters and dependencies *)
let makefile_cmdline = ref ""
(** optional command-line name of the .cluster file *)
let cluster_cmdline = ref None
(** value of -out_file command-line *)
let out_file_cmdline = ref ""
(** value of -err_file command-line *)
let err_file_cmdline = ref ""
(** List of obj memory leak buckets to be checked in Objective-C/C++ *)
let ml_buckets_arg = ref "cf"
(** Whether specs can be cleaned up before starting analysis *)
let allow_specs_cleanup = ref false
let version_string () =
"Infer version "
^ Version.versionString
^ "\nCopyright 2009 - present Facebook. All Rights Reserved.\n"
let print_version () =
F.fprintf F.std_formatter "%s@." (version_string ());
exit 0
let print_version_json () =
F.fprintf F.std_formatter "%s@." Version.versionJson;
exit 0
let arg_desc =
let base_arg =
let desc =
base_arg_desc @
[
"-err_file",
Arg.Set_string err_file_cmdline,
Some "file",
"use file for the err channel"
;
"-iterations",
Arg.Set_int Config.iterations,
Some "n",
"set the max number of operations for each function, \
expressed as a multiple of symbolic operations (default n=1)"
;
"-nonstop",
Arg.Set Config.nonstop,
None,
"activate the nonstop mode: the analysis continues after finding errors. \
With this option the analysis can become less precise."
;
"-out_file",
Arg.Set_string out_file_cmdline,
Some "file",
"use file for the out channel"
;
"-print_builtins",
Arg.Unit Builtin.print_and_exit,
None,
"print the builtin functions and exit"
;
"-reactive",
Arg.Unit (fun () -> Config.reactive_mode := true),
None,
"analyze in reactive propagation mode starting from changed files"
;
"-continue",
Arg.Set Config.continue_capture,
None,
"continue the capture for the reactive analysis,\
increasing the changed files/procedures."
;
(* TODO: merge with the -project_root option *)
"-java",
Arg.Unit (fun () -> Config.curr_language := Config.Java),
None,
"Set language to Java"
;
"-version",
Arg.Unit print_version,
None,
"print version information and exit"
;
"-version_json",
Arg.Unit print_version_json,
None,
"print version json formatted"
;
"-objcm",
Arg.Set Config.objc_memory_model_on,
None,
"Use ObjC memory model"
;
"-no_progress_bar",
Arg.Unit (fun () -> Config.show_progress_bar := false),
None,
"Do not show a progress bar"
;
"-ml_buckets",
Arg.Set_string ml_buckets_arg,
Some "ml_buckets",
"memory leak buckets to be checked, separated by commas. \
The possible buckets are cf (Core Foundation), arc, narc (No arc), cpp, unknown_origin"
;
] in
Arg.create_options_desc false "Analysis Options" desc in
let reserved_arg =
let desc =
reserved_arg_desc @
[
"-allow_specs_cleanup",
Arg.Unit (fun () -> allow_specs_cleanup := true),
None,
"Allow to remove existing specs before running analysis when it's not incremental"
;
"-analysis_stops",
Arg.Set Config.analysis_stops,
None,
"issue a warning when the analysis stops"
;
"-angelic_execution",
Arg.Set Config.angelic_execution,
None,
"activate angelic execution: \
The analysis ignores errors caused by unknown procedure calls."
;
"-checkers",
Arg.Unit (fun () -> checkers := true),
None,
" run only the checkers instead of the full analysis"
;
"-cluster",
Arg.String (fun s -> cluster_cmdline := Some s),
Some "fname",
"specify a .cluster file to be analyzed"
;
"-codequery",
Arg.String (fun s -> CodeQuery.query := Some s),
Some "query",
" execute the code query"
;
"-eradicate",
Arg.Unit (fun () ->
Config.eradicate := true;
checkers := true),
None,
" activate the eradicate checker for java annotations"
;
"-merge",
Arg.Set Config.merge,
None,
"merge the captured results directories specified in the dependency file"
;
"-makefile",
Arg.Set_string makefile_cmdline,
Some "file",
"create a makefile to perform the analysis"
;
"-modified_targets",
Arg.String (fun file -> MergeCapture.modified_file file),
Some "file",
"read the file of buck targets modified since the last analysis"
;
"-optimistic_cast",
Arg.Set Config.optimistic_cast,
None,
"allow cast of undefined values"
;
"-print_buckets",
Arg.Unit (fun() -> Config.show_buckets := true; Config.show_ml_buckets := true),
None,
"Add buckets to issue descriptions, useful when developing infer"
;
"-seconds_per_iteration",
Arg.Set_float Config.seconds_per_iteration,
Some "n",
"set the number of seconds per iteration (default n=30)"
;
"-subtype_multirange",
Arg.Set Config.subtype_multirange,
None,
"use the multirange subtyping domain"
;
"-symops_per_iteration",
Arg.Set_int Config.symops_per_iteration,
Some "n",
"set the number of symbolic operations per iteration (default n="
^ (string_of_int !Config.symops_per_iteration) ^ ")"
;
"-tracing",
Arg.Unit (fun () -> Config.report_runtime_exceptions := true),
None,
"Report error traces for runtime exceptions (Only for Java)"
;
"-type_size",
Arg.Set Config.type_size,
None,
"consider the size of types during analysis"
;
] in
Arg.create_options_desc false
"Reserved Options: Experimental features, use with caution!" desc in
base_arg @ reserved_arg
let usage =
(version_string ()) ^ "\
Usage: InferAnalyze [options]\n\
Analyze the files captured in the project results directory, \
which can be specified with the -results_dir option."
let print_usage_exit () =
Arg.usage arg_desc usage;
exit(1)
let () = (* parse command-line arguments *)
let f _ =
() (* ignore anonymous arguments *) in
Arg.parse "INFER_ARGS" arg_desc f usage;
if not (Sys.file_exists !Config.results_dir) then
let () =
if Config.print_builtins then Builtin.print_and_exit () ;
(match Config.modified_targets with Some file -> MergeCapture.modified_file file | None -> ()) ;
if not (Sys.file_exists Config.results_dir) then
begin
L.err "ERROR: results directory %s does not exist@.@." !Config.results_dir;
print_usage_exit ()
L.err "ERROR: results directory %s does not exist@.@." Config.results_dir;
Config.print_usage_exit ()
end
let analyze_exe_env exe_env =
@ -250,7 +30,7 @@ let analyze_exe_env exe_env =
Specs.clear_spec_tbl ();
Random.self_init ();
let line_reader = Printer.LineReader.create () in
if !checkers then
if Config.checkers then
begin
(** run the checkers only *)
let call_graph = Exe_env.get_cg exe_env in
@ -299,7 +79,7 @@ let close_output_file = function
| Some (_, cout) -> close_out cout
let setup_logging () =
if !Config.developer_mode then
if Config.developer_mode then
let log_dir_name = "log" in
let analyzer_out_name = "analyzer_out" in
let analyzer_err_name = "analyzer_err" in
@ -308,18 +88,18 @@ let setup_logging () =
(DB.Results_dir.path_to_filename DB.Results_dir.Abs_root [log_dir_name]) in
DB.create_dir log_dir;
let analyzer_out_file =
if !out_file_cmdline = "" then Filename.concat log_dir analyzer_out_name
else !out_file_cmdline in
if Config.out_file_cmdline = "" then Filename.concat log_dir analyzer_out_name
else Config.out_file_cmdline in
let analyzer_err_file =
if !err_file_cmdline = "" then Filename.concat log_dir analyzer_err_name
else !err_file_cmdline in
if Config.err_file_cmdline = "" then Filename.concat log_dir analyzer_err_name
else Config.err_file_cmdline in
let analyzer_out_of = open_output_file Logging.set_out_formatter analyzer_out_file in
let analyzer_err_of = open_output_file Logging.set_err_formatter analyzer_err_file in
analyzer_out_of, analyzer_err_of
else None, None
let teardown_logging analyzer_out_of analyzer_err_of =
if !Config.developer_mode then
if Config.developer_mode then
begin
L.flush_streams ();
close_output_file analyzer_out_of;
@ -337,11 +117,11 @@ let output_json_makefile_stats clusters =
("procedures", `Int num_procs);
("lines", `Int num_lines) ] in
(* write stats file to disk, intentionally overwriting old file if it already exists *)
let f = open_out (Filename.concat !Config.results_dir Config.proc_stats_filename) in
let f = open_out (Filename.concat Config.results_dir Config.proc_stats_filename) in
Yojson.Basic.pretty_to_channel f file_stats
let print_prolog () =
match !cluster_cmdline with
match Config.cluster_cmdline with
| None ->
L.stdout "Starting analysis (Infer version %s)@." Version.versionString;
| Some clname -> L.stdout "Cluster %s@." clname
@ -354,45 +134,43 @@ let process_cluster_cmdline fname =
analyze_cluster (nr - 1) cluster
let register_perf_stats_report () =
let stats_dir = Filename.concat !Config.results_dir Config.backend_stats_dir_name in
let cluster = match !cluster_cmdline with Some cl -> "_" ^ (Filename.basename cl) | None -> "" in
let stats_file = Filename.concat stats_dir (Config.perf_stats_prefix ^ cluster ^ ".json") in
DB.create_dir !Config.results_dir ;
let stats_dir = Filename.concat Config.results_dir Config.backend_stats_dir_name in
let cluster = match Config.cluster_cmdline with Some cl -> "_" ^ cl | None -> "" in
let stats_base = Config.perf_stats_prefix ^ "_" ^ (Filename.basename cluster) ^ ".json" in
let stats_file = Filename.concat stats_dir stats_base in
DB.create_dir Config.results_dir ;
DB.create_dir stats_dir ;
PerfStats.register_report_at_exit stats_file
let () =
register_perf_stats_report () ;
if !Config.developer_mode then
if Config.developer_mode then
Printexc.record_backtrace true;
print_prolog ();
RegisterCheckers.register ();
if !allow_specs_cleanup = true && !cluster_cmdline = None then
if Config.allow_specs_cleanup = true && Config.cluster_cmdline = None then
DB.Results_dir.clean_specs_dir ();
let analyzer_out_of, analyzer_err_of = setup_logging () in
if !Config.curr_language = Config.C_CPP
then Mleak_buckets.init_buckets !ml_buckets_arg;
let finish_logging () =
teardown_logging analyzer_out_of analyzer_err_of in
match !cluster_cmdline with
match Config.cluster_cmdline with
| Some fname ->
process_cluster_cmdline fname;
finish_logging ()
| None ->
if !Config.merge then MergeCapture.merge_captured_targets ();
if Config.merge then MergeCapture.merge_captured_targets ();
let clusters = DB.find_source_dirs () in
L.err "Found %d source files in %s@."
(IList.length clusters) !Config.results_dir;
(IList.length clusters) Config.results_dir;
if !makefile_cmdline <> ""
if Config.makefile_cmdline <> ""
then
ClusterMakefile.create_cluster_makefile clusters !makefile_cmdline
ClusterMakefile.create_cluster_makefile clusters Config.makefile_cmdline
else
begin
IList.iteri

@ -338,9 +338,9 @@ let disabled_checks_by_default = [
]
let inferconfig () =
match !Config.inferconfig_home with
| Some dir -> Filename.concat dir Config.inferconfig_file
| None -> Config.inferconfig_file
match Config.inferconfig_home, Config.project_root with
| Some dir, _ | _, Some dir -> Filename.concat dir Config.inferconfig_file
| None, None -> Config.inferconfig_file
let load_filters analyzer =
let inferconfig_file = inferconfig () in
@ -386,7 +386,6 @@ let filters_from_inferconfig inferconfig : filters =
(* Create filters based on .inferconfig *)
(* The environment varialble NO_PATH_FILTERING disables path filtering. *)
let create_filters analyzer =
Config.project_root := Some (Sys.getcwd ());
if Config.from_env_variable "NO_PATH_FILTERING" then do_not_filter
else
match load_filters (Utils.string_of_analyzer analyzer) with
@ -420,7 +419,6 @@ let is_checker_enabled checker_name =
(* are of the form: path/to/file.java -> {infer, eradicate} meaning that analysis results will *)
(* be reported on path/to/file.java both for infer and for eradicate *)
let test () =
Config.project_root := Some (Sys.getcwd ());
let filters =
IList.map (fun analyzer -> (analyzer, create_filters analyzer)) analyzers in
let matching_analyzers path =

@ -14,69 +14,8 @@ module L = Logging
module F = Format
open Jsonbug_j
(** Outfile to save the latex report *)
let latex = ref None
(** command line flag: if true, print whole seconds only *)
let whole_seconds = ref false
(** Outfile to save bugs stats in csv format *)
let bugs_csv = ref None
(** Outfile to save bugs stats in JSON format *)
let bugs_json = ref None
(** Outfile to save bugs stats in txt format *)
let bugs_txt = ref None
(** Outfile to save bugs stats in xml format *)
let bugs_xml = ref None
(** Outfile to save procedures stats in csv format *)
let procs_csv = ref None
(** Outfile to save procedures stats in xml format *)
let procs_xml = ref None
(** Outfile to save call stats in csv format *)
let calls_csv = ref None
(** Outfile to save the analysis report *)
let report = ref None
(** command line flag: if true, produce a svg file *)
let svg = ref false
(** command line flag: if true, export specs to xml files *)
let xml_specs = ref false
(** command line flag: if true, produce unit test for each spec *)
let unit_test = ref false
(** command line flag: if true, do not print the spec to standard output *)
let quiet = ref false
(** command line flag: if true, print stats about preconditions to standard output *)
let precondition_stats = ref false
(** name of the file to load analysis results from *)
let load_analysis_results = ref None
(** If true then include Infer source code locations in json reports *)
let reports_include_ml_loc = ref false
(** name of the file to load save results to *)
let save_analysis_results = ref None
(** command-line option to print the location of the copy of a source file *)
let source_file_copy = ref None
(** command line option to test the filtering based on .inferconfig *)
let test_filtering = ref false
(** Setup the analyzer in order to filter out errors for this analyzer only *)
let analyzer = ref None
let handle_source_file_copy_option () = match !source_file_copy with
| None -> ()
| Some source_file ->
@ -88,157 +27,9 @@ let canonic_path_from_string s =
if s = Filename.dir_sep then s
else Filename.concat (Filename.dirname s) (Filename.basename s) ^ Filename.dir_sep
let arg_desc =
let base_arg =
let desc =
[
"-bugs",
Arg.String (fun s -> bugs_csv := create_outfile s),
Some "bugs.csv",
"create file bugs.csv containing a list of bugs in CSV format"
;
"-bugs_json",
Arg.String (fun s -> bugs_json := create_outfile s),
Some "bugs.json",
"create file bugs.json containing a list of bugs in JSON format"
;
"-bugs_txt",
Arg.String (fun s -> bugs_txt := create_outfile s),
Some "bugs.txt",
"create file bugs.txt containing a list of bugs in text format"
;
"-bugs_xml",
Arg.String (fun s -> bugs_xml := create_outfile s),
Some "bugs.xml",
"create file bugs.xml containing a list of bugs in XML format"
;
"-calls",
Arg.String (fun s -> calls_csv := create_outfile s),
Some "calls.csv",
"write individual calls in csv format to file.csv"
;
"-load_results",
Arg.String (fun s -> load_analysis_results := Some s),
Some "file.iar",
"load analysis results from Infer Analysis Results file file.iar"
;
"-procs",
Arg.String (fun s -> procs_csv := create_outfile s),
Some "procs.csv",
"create file procs.csv containing statistics for each procedure in CSV format"
;
"-procs_xml",
Arg.String (fun s -> procs_xml := create_outfile s),
Some "procs.xml",
"create file procs.xml containing statistics for each procedure in XML format"
;
"-results_dir",
Arg.String (fun s -> Config.results_dir := s),
Some "dir",
"read all the .specs files in the results dir"
;
"-lib",
Arg.String (fun s ->
Config.specs_library := filename_to_absolute s :: !Config.specs_library),
Some "dir",
"add dir to the list of directories to be searched for spec files"
;
"-q",
Arg.Set quiet,
None,
"quiet: do not print specs on standard output"
;
"-save_results",
Arg.String (fun s -> save_analysis_results := Some s),
Some "file.iar",
"save analysis results to Infer Analysis Results file file.iar"
;
"-unit_test",
Arg.Set unit_test,
None,
"print unit test code"
;
"-xml",
Arg.Set xml_specs,
None,
"export specs into XML files file1.xml ... filen.xml"
;
"-test_filtering",
Arg.Set test_filtering,
None,
"list all the files Infer can report on (should be call at the root of the procject, \
where .inferconfig lives)."
;
"-analyzer",
Arg.String (fun s -> analyzer := Some (Utils.analyzer_of_string s)),
Some "analyzer",
"setup the analyzer for the path filtering"
;
"-inferconfig_home",
Arg.String (fun s -> Config.inferconfig_home := Some s),
Some "dir",
"Path to the .inferconfig file"
;
"-with_infer_src_loc",
Arg.Set reports_include_ml_loc,
None,
"include the location (in the Infer source code) from where reports are generated"
;
] in
Arg.create_options_desc false "Options" desc in
let reserved_arg =
let desc =
[
"-latex",
Arg.String (fun s -> latex := create_outfile s),
Some "file.tex",
"print latex report to file.tex"
;
"-print_types",
Arg.Set Config.print_types,
None,
"print types in symbolic heaps"
;
"-precondition_stats",
Arg.Set precondition_stats,
None,
"print stats about preconditions to standard output"
;
"-report",
Arg.String (fun s -> report := create_outfile s),
Some "report_file",
"create file report_file containing a report of the analysis results"
;
"-source_file_copy",
Arg.String (fun s -> source_file_copy := Some (DB.abs_source_file_from_path s)),
Some "source_file",
"print the path of the copy of source_file in the results directory"
;
"-svg",
Arg.Set svg,
None,
"generate .dot and .svg"
;
"-whole_seconds",
Arg.Set whole_seconds,
None,
"print whole seconds only"
;
] in
Arg.create_options_desc false "Reserved Options" desc in
base_arg @ reserved_arg
let usage =
"Usage: InferPrint [options] name1.specs ... namen.specs\n\
Read, convert, and print .specs files. \
To process all the .specs in the current directory, pass . as only parameter \
To process all the .specs in the results directory, use option -results_dir \
Each spec is printed to standard output unless option -q is used."
let print_usage_exit err_s =
L.err "Load Error: %s@.@." err_s;
Arg.usage arg_desc usage;
exit(1)
Config.print_usage_exit ()
(** return the list of the .specs files in the results dir and libs, if they're defined *)
let load_specfiles () =
@ -250,7 +41,7 @@ let load_specfiles () =
IList.filter is_specs_file all_filepaths in
let specs_dirs =
let result_specs_dir = DB.filename_to_string (DB.Results_dir.specs_dir ()) in
result_specs_dir :: !Config.specs_library in
result_specs_dir :: Config.specs_library in
IList.flatten (IList.map specs_files_in_dir specs_dirs)
(** Create and initialize latex file *)
@ -265,7 +56,7 @@ 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 (Procname.to_string proc_name)));
F.fprintf fmt "@[<v>%a@]" (Specs.pp_summary (pe_latex Black) !whole_seconds) summary
F.fprintf fmt "@[<v>%a@]" (Specs.pp_summary (pe_latex Black) Config.whole_seconds) summary
let error_desc_to_csv_string error_desc =
let pp fmt () = F.fprintf fmt "%a" Localise.pp_error_desc error_desc in
@ -591,7 +382,7 @@ module BugsJson = struct
let file =
DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in
let json_ml_loc = match ml_loc_opt with
| Some (file, lnum, cnum, enum) when !reports_include_ml_loc ->
| Some (file, lnum, cnum, enum) when Config.reports_include_ml_loc ->
Some Jsonbug_j.{ file; lnum; cnum; enum; }
| _ -> None in
let bug = {
@ -969,30 +760,30 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna
let base = DB.chop_extension (DB.filename_from_string fname) in
let pp_simple_saved = !Config.pp_simple in
Config.pp_simple := true;
if !quiet then ()
if Config.quiet then ()
else L.out "Procedure: %a@\n%a@."
Procname.pp proc_name (Specs.pp_summary pe_text !whole_seconds) summary;
Procname.pp proc_name (Specs.pp_summary pe_text Config.whole_seconds) summary;
let error_filter error_desc error_name =
let always_report () =
Localise.error_desc_extract_tag_value error_desc "always_report" = "true" in
(!Config.write_html || not (Localise.equal error_name Localise.skip_function)) &&
(Config.write_html || not (Localise.equal error_name Localise.skip_function)) &&
(filters.Inferconfig.path_filter summary.Specs.attributes.ProcAttributes.loc.Location.file
|| always_report ()) &&
filters.Inferconfig.error_filter error_name &&
filters.Inferconfig.proc_filter proc_name in
do_outf procs_csv (fun outf -> ProcsCsv.pp_summary top_proc_set outf.fmt summary);
do_outf calls_csv (fun outf -> CallsCsv.pp_calls outf.fmt summary);
do_outf procs_xml (fun outf -> ProcsXml.pp_proc top_proc_set outf.fmt summary);
do_outf bugs_csv (fun outf -> BugsCsv.pp_bugs error_filter outf.fmt summary);
do_outf bugs_json (fun outf -> BugsJson.pp_bugs error_filter outf.fmt summary);
do_outf bugs_txt (fun outf -> BugsTxt.pp_bugs error_filter outf.fmt summary);
do_outf bugs_xml (fun outf -> BugsXml.pp_bugs error_filter linereader outf.fmt summary);
do_outf report (fun _ -> Stats.process_summary error_filter summary linereader stats);
if !precondition_stats then PreconditionStats.do_summary proc_name summary;
if !unit_test then UnitTest.print_unit_test proc_name summary;
do_outf Config.procs_csv (fun outf -> ProcsCsv.pp_summary top_proc_set outf.fmt summary);
do_outf Config.calls_csv (fun outf -> CallsCsv.pp_calls outf.fmt summary);
do_outf Config.procs_xml (fun outf -> ProcsXml.pp_proc top_proc_set outf.fmt summary);
do_outf Config.bugs_csv (fun outf -> BugsCsv.pp_bugs error_filter outf.fmt summary);
do_outf Config.bugs_json (fun outf -> BugsJson.pp_bugs error_filter outf.fmt summary);
do_outf Config.bugs_txt (fun outf -> BugsTxt.pp_bugs error_filter outf.fmt summary);
do_outf Config.bugs_xml (fun outf -> BugsXml.pp_bugs error_filter linereader outf.fmt summary);
do_outf Config.report (fun _ -> Stats.process_summary error_filter summary linereader stats);
if Config.precondition_stats then PreconditionStats.do_summary proc_name summary;
if Config.unit_test then UnitTest.print_unit_test proc_name summary;
Config.pp_simple := pp_simple_saved;
do_outf latex (fun outf -> write_summary_latex outf.fmt summary);
if !svg then begin
do_outf Config.latex (fun outf -> write_summary_latex outf.fmt summary);
if Config.svg then begin
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
@ -1008,14 +799,14 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna
"\" >\"" ^
(DB.filename_to_string svg_file) ^"\""))
end;
if !xml_specs then begin
if Config.xml_specs then begin
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
begin
let xml_out = ref (create_outfile (DB.filename_to_string xml_file)) in
let xml_out = create_outfile (DB.filename_to_string xml_file) in
do_outf xml_out (fun outf ->
Dotty.print_specs_xml
(Specs.get_signature summary)
@ -1029,26 +820,28 @@ module AnalysisResults = struct
type t = (string * Specs.summary) list
let spec_files_from_cmdline =
(* parse command-line arguments, and find spec files specified there *)
let args = ref [] in
let f arg =
if not (Filename.check_suffix arg Config.specs_files_suffix) && arg <> "."
then print_usage_exit "arguments must be .specs files"
else args := arg::!args in
Arg.parse "INFERPRINT_ARGS" arg_desc f usage;
if !test_filtering then
(* find spec files specified by command-line arguments *)
IList.iter (fun arg ->
if not (Filename.check_suffix arg Config.specs_files_suffix) && arg <> "."
then print_usage_exit "arguments must be .specs files"
) Config.anon_args ;
(match Config.source_file_copy with
| Some s -> source_file_copy := Some (DB.abs_source_file_from_path s)
| None -> ()
);
if Config.test_filtering then
begin
Inferconfig.test ();
exit(0)
end;
IList.append (if !args = ["."] then begin
IList.append (if Config.anon_args = ["."] then begin
let arr = Sys.readdir "." in
let all_files = Array.to_list arr in
IList.filter
(fun fname -> (Filename.check_suffix fname Config.specs_files_suffix))
all_files
end
else !args) (load_specfiles ())
else Config.anon_args) (load_specfiles ())
(** apply [f] to [arg] with the gc compaction disabled during the execution *)
let apply_without_gc f arg =
@ -1113,10 +906,10 @@ module AnalysisResults = struct
let get_summary_iterator () =
let iterator_of_summary_list r =
fun f -> IList.iter f r in
match !load_analysis_results with
match Config.load_analysis_results with
| None ->
begin
match !save_analysis_results with
match Config.save_analysis_results with
| None ->
iterator_of_spec_files ()
| Some s ->
@ -1139,54 +932,53 @@ end
let compute_top_procedures = ref false
let register_perf_stats_report () =
let stats_dir = Filename.concat !Config.results_dir Config.reporting_stats_dir_name in
let stats_dir = Filename.concat Config.results_dir Config.reporting_stats_dir_name in
let stats_file = Filename.concat stats_dir (Config.perf_stats_prefix ^ ".json") in
DB.create_dir !Config.results_dir ;
DB.create_dir Config.results_dir ;
DB.create_dir stats_dir ;
PerfStats.register_report_at_exit stats_file
let () =
register_perf_stats_report () ;
Config.developer_mode := true;
Config.print_using_diff := true;
handle_source_file_copy_option ();
let iterate_summaries = AnalysisResults.get_summary_iterator () in
let filters =
match !analyzer with
match Config.analyzer with
| None -> Inferconfig.do_not_filter
| Some analyzer -> Inferconfig.create_filters analyzer in
let pdflatex fname = ignore (Sys.command ("pdflatex " ^ fname)) in
do_outf latex (fun outf -> begin_latex_file outf.fmt);
do_outf procs_csv (fun outf -> ProcsCsv.pp_header outf.fmt ());
do_outf procs_xml (fun outf -> ProcsXml.pp_procs_open outf.fmt ());
do_outf calls_csv (fun outf -> CallsCsv.pp_header outf.fmt ());
do_outf bugs_csv (fun outf -> BugsCsv.pp_header outf.fmt ());
do_outf bugs_json (fun outf -> BugsJson.pp_json_open outf.fmt ());
do_outf bugs_xml (fun outf -> BugsXml.pp_bugs_open outf.fmt ());
do_outf report (fun outf -> Report.pp_header outf.fmt ());
do_outf Config.latex (fun outf -> begin_latex_file outf.fmt);
do_outf Config.procs_csv (fun outf -> ProcsCsv.pp_header outf.fmt ());
do_outf Config.procs_xml (fun outf -> ProcsXml.pp_procs_open outf.fmt ());
do_outf Config.calls_csv (fun outf -> CallsCsv.pp_header outf.fmt ());
do_outf Config.bugs_csv (fun outf -> BugsCsv.pp_header outf.fmt ());
do_outf Config.bugs_json (fun outf -> BugsJson.pp_json_open outf.fmt ());
do_outf Config.bugs_xml (fun outf -> BugsXml.pp_bugs_open outf.fmt ());
do_outf Config.report (fun outf -> Report.pp_header outf.fmt ());
let top_proc = TopProcedures.create () in
if !compute_top_procedures && (!procs_csv != None || !procs_xml != None)
if !compute_top_procedures && (Config.procs_csv != None || Config.procs_xml != None)
then iterate_summaries (TopProcedures.process_summary top_proc);
let top_proc_set = TopProcedures.top_set top_proc in
let linereader = Printer.LineReader.create () in
let stats = Stats.create () in
iterate_summaries (process_summary filters linereader stats top_proc_set);
if !unit_test then UnitTest.print_unit_test_main ();
do_outf procs_csv close_outf;
do_outf procs_xml (fun outf -> ProcsXml.pp_procs_close outf.fmt (); close_outf outf);
do_outf bugs_csv close_outf;
do_outf bugs_json (fun outf -> BugsJson.pp_json_close outf.fmt (); close_outf outf);
do_outf bugs_json close_outf;
do_outf calls_csv close_outf;
do_outf bugs_txt close_outf;
do_outf bugs_xml (fun outf -> BugsXml.pp_bugs_close outf.fmt (); close_outf outf);
do_outf latex (fun outf ->
if Config.unit_test then UnitTest.print_unit_test_main ();
do_outf Config.procs_csv close_outf;
do_outf Config.procs_xml (fun outf -> ProcsXml.pp_procs_close outf.fmt (); close_outf outf);
do_outf Config.bugs_csv close_outf;
do_outf Config.bugs_json (fun outf -> BugsJson.pp_json_close outf.fmt (); close_outf outf);
do_outf Config.bugs_json close_outf;
do_outf Config.calls_csv close_outf;
do_outf Config.bugs_txt close_outf;
do_outf Config.bugs_xml (fun outf -> BugsXml.pp_bugs_close outf.fmt (); close_outf outf);
do_outf Config.latex (fun outf ->
Latex.pp_end outf.fmt ();
close_outf outf;
pdflatex outf.fname;
let pdf_name = (Filename.chop_extension outf.fname) ^ ".pdf" in
ignore (Sys.command ("open " ^ pdf_name)));
do_outf report (fun outf -> F.fprintf outf.fmt "%a@?" Report.pp_stats stats; close_outf outf);
if !precondition_stats then PreconditionStats.pp_stats ()
do_outf Config.report
(fun outf -> F.fprintf outf.fmt "%a@?" Report.pp_stats stats; close_outf outf);
if Config.precondition_stats then PreconditionStats.pp_stats ()

@ -48,7 +48,7 @@ module NodeVisitSet =
if n <> 0 then n else compare_distance_to_exit x1 x2
let compare x1 x2 =
if !Config.footprint then
match !Config.worklist_mode with
match Config.worklist_mode with
| 0 -> compare_ids x1.node x2.node
| 1 -> compare_distance_to_exit x1 x2
| _ -> compare_number_of_visits x1 x2
@ -167,7 +167,7 @@ let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.node) : Paths.PathSet.t
let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t =
if !Config.footprint
then
run_in_re_execution_mode
Config.run_in_re_execution_mode
(Abs.lifted_abstract pname tenv)
pset
else
@ -179,7 +179,7 @@ let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.Path
else Some (Abs.abstract pname tenv p) in
if !Config.footprint
then
run_in_re_execution_mode
Config.run_in_re_execution_mode
(Paths.PathSet.map_option abs_option)
pathset
else
@ -189,13 +189,13 @@ let do_join_pre plist =
Dom.proplist_collapse_pre plist
let do_join_post pname tenv (pset: Paths.PathSet.t) =
if !Config.spec_abs_level <= 0 then
if Config.spec_abs_level <= 0 then
Dom.pathset_collapse pset
else
Dom.pathset_collapse (Dom.pathset_collapse_impl pname tenv pset)
let do_meet_pre pset =
if !Config.meet_level > 0 then
if Config.meet_level > 0 then
Dom.propset_meet_generate_pre pset
else
Propset.to_proplist pset
@ -206,7 +206,7 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list =
let collect_do_abstract_one tenv prop =
if !Config.footprint
then
run_in_re_execution_mode
Config.run_in_re_execution_mode
(Abs.abstract_no_symop tenv)
prop
else
@ -325,7 +325,7 @@ let check_prop_size p _ =
(* Check prop size and filter out possible unabstracted lists *)
let check_prop_size edgeset_todo =
if !Config.monitor_prop_size then Paths.PathSet.iter check_prop_size edgeset_todo
if Config.monitor_prop_size then Paths.PathSet.iter check_prop_size edgeset_todo
let reset_prop_metrics () =
prop_max_size := (0, Prop.prop_emp);
@ -436,7 +436,7 @@ let check_assignement_guard node =
let check_guard n =
IList.for_all check_instr (Cfg.Node.get_instrs n) in
IList.for_all check_guard succs in
if !Config.curr_language = Config.C_CPP &&
if !Config.curr_language = Config.Clang &&
succs_are_all_prune_nodes () &&
succs_same_loc_as_node () &&
succs_have_simple_guards () then
@ -566,7 +566,7 @@ let forward_tabulate tenv wl =
exe_iter
(fun prop path cnt num_paths ->
try
let prop = if !Config.taint_analysis then
let prop = if Config.taint_analysis then
let tainted_params = Taint.tainted_params proc_name in
Tabulation.add_param_taint proc_name formal_params prop tainted_params
else prop in
@ -581,7 +581,7 @@ let forward_tabulate tenv wl =
with
| exn when Exceptions.handle_exception exn && !Config.footprint ->
handle_exn curr_node exn;
if !Config.nonstop then
if Config.nonstop then
propagate_nodes_divergence
tenv proc_desc (Paths.PathSet.from_renamed_list [(prop, path)])
succ_nodes exn_nodes wl;
@ -794,7 +794,7 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr
let sigma_new_formals =
let do_formal (pv, typ) =
let texp = match !Config.curr_language with
| Config.C_CPP -> Sil.Sizeof (typ, Sil.Subtype.exact)
| Config.Clang -> Sil.Sizeof (typ, Sil.Subtype.exact)
| Config.Java -> Sil.Sizeof (typ, Sil.Subtype.subtypes) in
Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in
IList.map do_formal new_formals in
@ -937,7 +937,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
let check_recursion_level () =
let summary = Specs.get_summary_unsafe "check_recursion_level" pname in
let recursion_level = Specs.get_timestamp summary in
if recursion_level > !Config.max_recursion then
if recursion_level > Config.max_recursion then
begin
L.err "Reached maximum level of recursion, raising a Timeout@.";
raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level))
@ -1017,7 +1017,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
(pp_intra_stats wl pdesc) proc_name
outcome;
speco in
if !Config.undo_join then
if Config.undo_join then
ignore (Specs.Jprop.filter filter candidate_preconditions)
else
ignore (IList.map filter candidate_preconditions) in
@ -1031,7 +1031,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
DB.Results_dir.path_to_filename
DB.Results_dir.Abs_source_dir
[(Procname.to_filename proc_name)] in
if !Config.write_dotty then
if Config.write_dotty then
Dotty.pp_speclist_dotty_file filename specs;
L.out "@.@.================================================";
L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Procname.pp proc_name;
@ -1273,9 +1273,9 @@ let analyze_proc exe_env proc_desc : Specs.summary =
let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in
let updated_summary =
update_summary prev_summary specs phase proc_name elapsed res in
if !Config.curr_language == Config.C_CPP && Config.report_custom_error then
if !Config.curr_language == Config.Clang && Config.report_custom_error then
report_custom_errors updated_summary;
if !Config.curr_language == Config.Java && !Config.report_runtime_exceptions then
if !Config.curr_language == Config.Java && Config.report_runtime_exceptions then
report_runtime_exceptions tenv proc_desc updated_summary;
updated_summary
@ -1284,7 +1284,7 @@ let transition_footprint_re_exe proc_name joined_pres =
L.out "Transition %a from footprint to re-exe@." Procname.pp proc_name;
let summary = Specs.get_summary_unsafe "transition_footprint_re_exe" proc_name in
let summary' =
if !Config.only_footprint then
if Config.only_footprint then
{ summary with
Specs.phase = Specs.RE_EXECUTION;
}
@ -1316,7 +1316,7 @@ let perform_transition exe_env tenv proc_name =
let transition () =
(* disable exceptions for leaks and protect against any other errors *)
let joined_pres =
let allowleak = !Config.allowleak in
let allow_leak = !Config.allow_leak in
(* apply the start node to f, and do nothing in case of exception *)
let apply_start_node f =
try
@ -1328,14 +1328,14 @@ let perform_transition exe_env tenv proc_name =
with exn when SymOp.exn_not_failure exn -> () in
apply_start_node (do_before_node 0);
try
Config.allowleak := true;
Config.allow_leak := true;
let res = collect_preconditions tenv proc_name in
Config.allowleak := allowleak;
Config.allow_leak := allow_leak;
apply_start_node do_after_node;
res
with exn when SymOp.exn_not_failure exn ->
apply_start_node do_after_node;
Config.allowleak := allowleak;
Config.allow_leak := allow_leak;
L.err "Error in collect_preconditions for %a@." Procname.pp proc_name;
let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
let err_str = "exception raised " ^ (Localise.to_string err_name) in
@ -1357,7 +1357,7 @@ let interprocedural_algorithm exe_env : unit =
match Exe_env.get_proc_desc exe_env proc_name with
| Some proc_desc ->
let reactive_changed =
if !Config.reactive_mode
if Config.reactive_mode
then (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.changed
else true in
if
@ -1417,13 +1417,13 @@ let do_analysis exe_env =
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
let tenv = Exe_env.get_tenv exe_env proc_name in
let summaryfp =
run_in_footprint_mode (analyze_proc exe_env) proc_desc in
Config.run_in_footprint_mode (analyze_proc exe_env) proc_desc in
Specs.add_summary proc_name summaryfp;
perform_transition exe_env tenv proc_name;
let summaryre =
run_in_re_execution_mode (analyze_proc exe_env) proc_desc in
Config.run_in_re_execution_mode (analyze_proc exe_env) proc_desc in
Specs.add_summary proc_name summaryre in
{
Ondemand.analyze_ondemand;
@ -1538,7 +1538,7 @@ let print_stats_cfg proc_shadowed cfg =
(** Print the stats for all the files in the exe_env *)
let print_stats exe_env =
if !Config.developer_mode then
if Config.developer_mode then
Exe_env.iter_files
(fun fname cfg ->
let proc_shadowed proc_desc =

@ -680,7 +680,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
[("is not " ^ rxxx ^ " after " ^ _line tags loc)] in
let bucket_str =
match bucket_opt with
| Some bucket when !Config.show_ml_buckets -> bucket
| Some bucket when Config.show_buckets -> bucket
| _ -> "" in
{ no_desc with descriptions = bucket_str :: xxx_allocated_to @ by_call_to @ is_not_rxxx_after;
tags = !tags }

@ -83,7 +83,7 @@ let set_err_formatter fmt =
(** Flush the current streams *)
let flush_streams () =
if !Config.developer_mode then
if Config.developer_mode then
begin
F.fprintf !current_out_formatter "@?";
F.fprintf !current_err_formatter "@?"
@ -91,8 +91,8 @@ let flush_streams () =
(** extend the current print log *)
let add_print_action pact =
if !Config.write_html then delayed_actions := pact :: !delayed_actions
else if not !Config.test then !printer_hook !current_out_formatter pact
if Config.write_html then delayed_actions := pact :: !delayed_actions
else if not Config.test then !printer_hook !current_out_formatter pact
(** reset the delayed print actions *)
let reset_delayed_prints () =
@ -110,7 +110,7 @@ let do_print fmt fmt_string =
F.fprintf fmt fmt_string
let do_print_in_developer_mode fmt fmt_string =
if !Config.developer_mode then
if Config.developer_mode then
F.fprintf fmt fmt_string
else
F.ifprintf fmt fmt_string
@ -143,7 +143,7 @@ let pp_ml_loc fmt ml_loc =
F.fprintf fmt "%s" (ml_loc_to_string ml_loc)
let pp_ml_loc_opt fmt ml_loc_opt =
if !Config.developer_mode then match ml_loc_opt with
if Config.developer_mode then match ml_loc_opt with
| None -> ()
| Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc
@ -197,7 +197,7 @@ let d_decrease_indent (indent: int) =
add_print_action (PTdecrease_indent, Obj.repr indent)
let log_progress_simple text =
if !Config.show_progress_bar then
if Config.show_progress_bar then
F.fprintf Format.err_formatter "%s@?" text
let log_progress_file () =
@ -207,7 +207,7 @@ let log_progress_procedure () =
log_progress_simple "."
let log_progress_timeout_event failure_kind =
if !Config.developer_mode then
if Config.developer_mode then
begin
match failure_kind with
| SymOp.FKtimeout ->

@ -114,7 +114,7 @@ and fsel_match fsel1 sub vars fsel2 =
| [], [] -> Some (sub, vars)
| [], _ -> None
| _, [] ->
if (!Config.abs_struct <= 0) then None
if (Config.abs_struct <= 0) then None
else Some (sub, vars) (* This can lead to great information loss *)
| (fld1, se1') :: fsel1', (fld2, se2') :: fsel2' ->
let n = Sil.fld_compare fld1 fld2 in
@ -123,7 +123,7 @@ and fsel_match fsel1 sub vars fsel2 =
| None -> None
| Some (sub', vars') -> fsel_match fsel1' sub' vars' fsel2'
end
else if (n < 0 && !Config.abs_struct > 0) then
else if (n < 0 && Config.abs_struct > 0) then
fsel_match fsel1' sub vars fsel2
(* This can lead to great information loss *)
else None

@ -19,13 +19,13 @@ module F = Format
let check_timestamp_of_symlinks = true
let buck_out () =
match !Config.project_root with
match Config.project_root with
| Some root ->
Filename.concat root "buck-out"
| None ->
Filename.concat (Filename.dirname !Config.results_dir) "buck-out"
Filename.concat (Filename.dirname Config.results_dir) "buck-out"
let infer_deps () = Filename.concat !Config.results_dir "infer-deps.txt"
let infer_deps () = Filename.concat Config.results_dir "infer-deps.txt"
let modified_targets = ref StringSet.empty
@ -147,7 +147,7 @@ let should_link ~target ~target_results_dir ~stats infer_out_src infer_out_dst =
and to determine whether the destination has never been copied.
In both cases, perform the link. *)
let process_merge_file deps_file =
let infer_out_dst = !Config.results_dir in
let infer_out_dst = Config.results_dir in
let stats = empty_stats () in
let process_line line =
match Str.split_delim (Str.regexp (Str.quote "\t")) line with

@ -14,103 +14,80 @@ open! Utils
let objc_arc_flag = "objc_arc"
let bucket_delimiter = ","
type mleak_bucket =
| MLeak_cf
| MLeak_arc
| MLeak_no_arc
| MLeak_cpp
| MLeak_unknown
let ml_buckets = ref []
let bucket_from_string bucket_s =
match bucket_s with
| "cf" -> MLeak_cf
| "arc" -> MLeak_arc
| "narc" -> MLeak_no_arc
| "cpp" -> MLeak_cpp
| "unknown_origin" -> MLeak_unknown
| _ -> assert false
let bucket_to_message bucket =
match bucket with
| MLeak_cf -> "[CF]"
| MLeak_arc -> "[ARC]"
| MLeak_no_arc -> "[NO ARC]"
| MLeak_cpp -> "[CPP]"
| MLeak_unknown -> "[UNKNOWN ORIGIN]"
| `MLeak_cf -> "[CF]"
| `MLeak_arc -> "[ARC]"
| `MLeak_no_arc -> "[NO ARC]"
| `MLeak_cpp -> "[CPP]"
| `MLeak_unknown -> "[UNKNOWN ORIGIN]"
let mleak_bucket_compare b1 b2 =
match b1, b2 with
| MLeak_cf, MLeak_cf -> 0
| MLeak_cf, _ -> -1
| _, MLeak_cf -> 1
| MLeak_arc, MLeak_arc -> 0
| MLeak_arc, _ -> -1
| _, MLeak_arc -> 1
| MLeak_no_arc, MLeak_no_arc -> 0
| MLeak_no_arc, _ -> -1
| _, MLeak_no_arc -> 1
| MLeak_unknown, MLeak_unknown -> 0
| MLeak_unknown, _ -> -1
| _, MLeak_unknown -> 1
| MLeak_cpp, MLeak_cpp -> 0
| `MLeak_all, `MLeak_all -> 0
| `MLeak_all, _ -> -1
| _, `MLeak_all -> 1
| `MLeak_cf, `MLeak_cf -> 0
| `MLeak_cf, _ -> -1
| _, `MLeak_cf -> 1
| `MLeak_arc, `MLeak_arc -> 0
| `MLeak_arc, _ -> -1
| _, `MLeak_arc -> 1
| `MLeak_no_arc, `MLeak_no_arc -> 0
| `MLeak_no_arc, _ -> -1
| _, `MLeak_no_arc -> 1
| `MLeak_unknown, `MLeak_unknown -> 0
| `MLeak_unknown, _ -> -1
| _, `MLeak_unknown -> 1
| `MLeak_cpp, `MLeak_cpp -> 0
let mleak_bucket_eq b1 b2 =
mleak_bucket_compare b1 b2 = 0
let init_buckets ml_buckets_arg =
let buckets =
Str.split (Str.regexp bucket_delimiter) ml_buckets_arg in
let buckets =
match buckets with
| ["all"] -> []
| _ -> IList.map bucket_from_string buckets in
ml_buckets := buckets
let contains_all =
IList.mem mleak_bucket_eq `MLeak_all Config.ml_buckets
let contains_cf ml_buckets =
IList.mem mleak_bucket_eq MLeak_cf ml_buckets
let contains_cf =
IList.mem mleak_bucket_eq `MLeak_cf Config.ml_buckets
let contains_arc ml_buckets =
IList.mem mleak_bucket_eq MLeak_arc ml_buckets
let contains_arc =
IList.mem mleak_bucket_eq `MLeak_arc Config.ml_buckets
let contains_narc ml_buckets =
IList.mem mleak_bucket_eq MLeak_no_arc ml_buckets
let contains_narc =
IList.mem mleak_bucket_eq `MLeak_no_arc Config.ml_buckets
let contains_cpp ml_buckets =
IList.mem mleak_bucket_eq MLeak_cpp ml_buckets
let contains_cpp =
IList.mem mleak_bucket_eq `MLeak_cpp Config.ml_buckets
let contains_unknown_origin ml_buckets =
IList.mem mleak_bucket_eq MLeak_unknown ml_buckets
let contains_unknown_origin =
IList.mem mleak_bucket_eq `MLeak_unknown Config.ml_buckets
let should_raise_leak_cf typ =
if contains_cf !ml_buckets then
if contains_cf then
Objc_models.is_core_lib_type typ
else false
let should_raise_leak_arc () =
if contains_arc !ml_buckets then
if contains_arc then
!Config.arc_mode
else false
let should_raise_leak_no_arc () =
if contains_narc !ml_buckets then
if contains_narc then
not (!Config.arc_mode)
else false
let should_raise_leak_unknown_origin () =
contains_unknown_origin !ml_buckets
let should_raise_leak_unknown_origin =
contains_unknown_origin
let ml_bucket_unknown_origin () =
bucket_to_message MLeak_unknown
let ml_bucket_unknown_origin =
bucket_to_message `MLeak_unknown
(* Returns whether a memory leak should be raised for a C++ object.*)
(* If ml_buckets contains cpp, then check leaks from C++ objects. *)
let should_raise_cpp_leak () =
if contains_cpp !ml_buckets then
Some (bucket_to_message MLeak_cpp)
let should_raise_cpp_leak =
if contains_cpp then
Some (bucket_to_message `MLeak_cpp)
else None
(* Returns whether a memory leak should be raised. *)
@ -118,11 +95,10 @@ let should_raise_cpp_leak () =
(* If arc is passed, check leaks from code that compiles with arc*)
(* If no arc is passed check the leaks from code that compiles without arc *)
let should_raise_objc_leak typ =
if IList.length !ml_buckets = 0 then Some ""
else
if should_raise_leak_cf typ then Some (bucket_to_message MLeak_cf)
else if should_raise_leak_arc () then Some (bucket_to_message MLeak_arc)
else if should_raise_leak_no_arc () then Some (bucket_to_message MLeak_no_arc)
if Config.ml_buckets = [] || contains_all then Some ""
else if should_raise_leak_cf typ then Some (bucket_to_message `MLeak_cf)
else if should_raise_leak_arc () then Some (bucket_to_message `MLeak_arc)
else if should_raise_leak_no_arc () then Some (bucket_to_message `MLeak_no_arc)
else None
(*

@ -13,8 +13,6 @@ open! Utils
val objc_arc_flag : string
val init_buckets : string -> unit
(* Returns whether a memory leak should be raised. *)
(* If cf is passed, then check leaks from Core Foundation. *)
(* If arc is passed, check leaks from code that compiles with arc*)
@ -23,8 +21,8 @@ val should_raise_objc_leak : Sil.typ -> string option
(* Returns whether a memory leak should be raised for a C++ object.*)
(* If ml_buckets contains cpp, then check leaks from C++ objects. *)
val should_raise_cpp_leak : unit -> string option
val should_raise_cpp_leak : string option
val should_raise_leak_unknown_origin : unit -> bool
val should_raise_leak_unknown_origin : bool
val ml_bucket_unknown_origin : unit -> string
val ml_bucket_unknown_origin : string

@ -140,7 +140,7 @@ let execute___print_value { Builtin.pdesc; prop_; path; args; }
let is_undefined_opt prop n_lexp =
let is_undef =
Option.is_some (Prop.get_undef_attribute prop n_lexp) in
is_undef && (!Config.angelic_execution || !Config.optimistic_cast)
is_undef && (Config.angelic_execution || Config.optimistic_cast)
(** Creates an object in the heap with a given type, when the object is not known to be null or when
it doesn't appear already in the heap. *)
@ -512,7 +512,7 @@ let execute___objc_retain_impl
let execute___objc_retain builtin_args
: Builtin.ret_typ =
if !Config.objc_memory_model_on then
if Config.objc_memory_model_on then
execute___objc_retain_impl builtin_args
else execute___no_op builtin_args.Builtin.prop_ builtin_args.Builtin.path
@ -531,7 +531,7 @@ let execute___objc_release_impl
let execute___objc_release builtin_args
: Builtin.ret_typ =
if !Config.objc_memory_model_on then
if Config.objc_memory_model_on then
execute___objc_release_impl builtin_args
else execute___no_op builtin_args.Builtin.prop_ builtin_args.Builtin.path
@ -547,7 +547,7 @@ let execute___set_autorelease_attribute
| [(lexp, _)], _ ->
let pname = Cfg.Procdesc.get_proc_name pdesc in
let prop = return_result lexp prop_ ret_ids in
if !Config.objc_memory_model_on then
if Config.objc_memory_model_on then
let n_lexp, prop = check_arith_norm_exp pname lexp prop in
let prop' = Prop.add_or_replace_exp_attribute prop n_lexp Sil.Aautorelease in
[(prop', path)]
@ -558,7 +558,7 @@ let execute___set_autorelease_attribute
let execute___release_autorelease_pool
({ Builtin.prop_; path; } as builtin_args)
: Builtin.ret_typ =
if !Config.objc_memory_model_on then
if Config.objc_memory_model_on then
let autoreleased_objects = Prop.get_atoms_with_attribute Sil.Aautorelease prop_ in
let prop_without_attribute = Prop.remove_attribute Sil.Aautorelease prop_ in
let call_release res exp =
@ -725,7 +725,7 @@ let _execute_free_nonzero mk pdesc tenv instr prop lexp typ loc =
IList.rev prop_list
end
with Rearrange.ARRAY_ACCESS ->
if (!Config.array_level = 0) then assert false
if (Config.array_level = 0) then assert false
else begin
L.d_strln ".... Array containing allocated heap cells ....";
L.d_str " Instr: "; Sil.d_instr instr; L.d_ln ();

@ -167,7 +167,7 @@ end
(** Execute the delayed print actions *)
let force_delayed_print fmt =
let pe_default =
if !Config.write_html then pe_html Black else pe_text in
if Config.write_html then pe_html Black else pe_text in
function
| (L.PTatom, a) ->
let (a: Sil.atom) = Obj.obj a in
@ -191,7 +191,7 @@ let force_delayed_print fmt =
F.fprintf fmt "%s@[" !s
| (L.PTinstr, i) ->
let (i: Sil.instr) = Obj.obj i in
if !Config.write_html
if Config.write_html
then
F.fprintf fmt "%a%a%a"
Io_infer.Html.pp_start_color Green
@ -201,7 +201,7 @@ let force_delayed_print fmt =
Sil.pp_instr pe_text fmt i
| (L.PTinstr_list, il) ->
let (il: Sil.instr list) = Obj.obj il in
if !Config.write_html
if Config.write_html
then
F.fprintf fmt "%a%a%a"
Io_infer.Html.pp_start_color Green
@ -220,7 +220,7 @@ let force_delayed_print fmt =
Location.pp fmt loc
| (L.PTnode_instrs, b_n) ->
let (b: bool), (io: Sil.instr option), (n: Cfg.node) = Obj.obj b_n in
if !Config.write_html
if Config.write_html
then
F.fprintf fmt "%a%a%a"
Io_infer.Html.pp_start_color Green
@ -271,14 +271,14 @@ let force_delayed_print fmt =
| (L.PTspec, spec) ->
let (spec: Prop.normal Specs.spec) = Obj.obj spec in
Specs.pp_spec
(if !Config.write_html then pe_html Blue else pe_text)
(if Config.write_html then pe_html Blue else pe_text)
None fmt spec
| (L.PTstr, s) ->
let (s: string) = Obj.obj s in
F.fprintf fmt "%s" s
| (L.PTstr_color, s) ->
let (s: string), (c: color) = Obj.obj s in
if !Config.write_html
if Config.write_html
then
F.fprintf fmt "%a%s%a"
Io_infer.Html.pp_start_color c
@ -291,7 +291,7 @@ let force_delayed_print fmt =
F.fprintf fmt "%s@\n" s
| (L.PTstrln_color, s) ->
let (s: string), (c: color) = Obj.obj s in
if !Config.write_html
if Config.write_html
then
F.fprintf fmt "%a%s%a@\n"
Io_infer.Html.pp_start_color c
@ -313,7 +313,7 @@ let force_delayed_print fmt =
(pp_seq (Sil.pp_typ pe_default)) fmt tl
| (L.PTerror, s) ->
let (s: string) = Obj.obj s in
if !Config.write_html
if Config.write_html
then
F.fprintf fmt "%aERROR: %s%a"
Io_infer.Html.pp_start_color Red
@ -323,7 +323,7 @@ let force_delayed_print fmt =
F.fprintf fmt "ERROR: %s" s
| (L.PTwarning, s) ->
let (s: string) = Obj.obj s in
if !Config.write_html
if Config.write_html
then
F.fprintf fmt "%aWARNING: %s%a"
Io_infer.Html.pp_start_color Orange
@ -333,7 +333,7 @@ let force_delayed_print fmt =
F.fprintf fmt "WARNING: %s" s
| (L.PTinfo, s) ->
let (s: string) = Obj.obj s in
if !Config.write_html
if Config.write_html
then
F.fprintf fmt "%aINFO: %s%a"
Io_infer.Html.pp_start_color Blue
@ -377,14 +377,14 @@ let start_session node (loc: Location.t) proc_name session =
Io_infer.Html.pp_start_color Black
let node_start_session node loc proc_name session =
if !Config.write_html then
if Config.write_html then
start_session node loc proc_name session
(** Finish a session, and perform delayed print actions if required *)
let node_finish_session node =
if !Config.test == false then force_delayed_prints ()
if Config.test == false then force_delayed_prints ()
else L.reset_delayed_prints ();
if !Config.write_html then begin
if Config.write_html then begin
F.fprintf !curr_html_formatter "</LISTING>%a"
Io_infer.Html.pp_end_color ();
NodesHtml.finish_node (Cfg.Node.get_id node :> int)
@ -393,7 +393,7 @@ let node_finish_session node =
(** Write html file for the procedure.
The boolean indicates whether to print whole seconds only *)
let write_proc_html whole_seconds pdesc =
if !Config.write_html then
if Config.write_html then
begin
let pname = Cfg.Procdesc.get_proc_name pdesc in
let nodes = IList.sort Cfg.Node.compare (Cfg.Procdesc.get_nodes pdesc) in
@ -561,7 +561,7 @@ let write_html_file linereader filename cfg =
(** Create filename.ext.html for each file in the exe_env. *)
let write_all_html_files linereader exe_env =
if !Config.write_html then
if Config.write_html then
Exe_env.iter_files
(fun _ cfg ->
let source_files_in_cfg =

@ -153,12 +153,12 @@ let pp_sub_entry pe0 f entry =
(** Pretty print a substitution as a list of (ident,exp) pairs *)
let pp_subl pe =
if !Config.smt_output then pp_semicolon_seq pe (pp_sub_entry pe)
if Config.smt_output then pp_semicolon_seq pe (pp_sub_entry pe)
else pp_semicolon_seq_oneline pe (pp_sub_entry pe)
(** Pretty print a pi. *)
let pp_pi pe =
if !Config.smt_output then pp_semicolon_seq pe (Sil.pp_atom pe)
if Config.smt_output then pp_semicolon_seq pe (Sil.pp_atom pe)
else pp_semicolon_seq_oneline pe (Sil.pp_atom pe)
(** Dump a pi. *)
@ -1395,7 +1395,7 @@ let footprint_normalize prop =
sigma_fav_add fav nsigma;
fav in
(* TODO (t4893479): make this check less angelic *)
if Sil.fav_exists fp_vars Ident.is_normal && not !Config.angelic_execution then
if Sil.fav_exists fp_vars Ident.is_normal && not Config.angelic_execution then
begin
L.d_strln "footprint part contains normal variables";
d_pi npi; L.d_ln ();

@ -205,7 +205,7 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist =
if extract_stack then Prop.replace_sigma (base_stack @ Prop.get_sigma prop) prop
else Prop.expose prop in
let update_pe_diff (prop: Prop.normal Prop.t) : printenv =
if !Config.print_using_diff then
if Config.print_using_diff then
let diff = compute_diff Blue (from_prop base_prop) (from_prop prop) in
let cmap_norm = diff_get_colormap false diff in
let cmap_foot = diff_get_colormap true diff in

@ -709,7 +709,7 @@ let get_smt_key a p =
let check_atom prop a0 =
let a = Prop.atom_normalize_prop prop a0 in
let prop_no_fp = Prop.replace_sigma_footprint [] (Prop.replace_pi_footprint [] prop) in
if !Config.smt_output then begin
if Config.smt_output then begin
let key = get_smt_key a prop_no_fp in
let key_filename =
DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [(key ^ ".cns")] in
@ -823,11 +823,11 @@ let check_inconsistency_base prop =
let is_java_this pvar =
!Config.curr_language = Config.Java && Pvar.is_this pvar in
let is_objc_instance_self pvar =
!Config.curr_language = Config.C_CPP &&
!Config.curr_language = Config.Clang &&
Pvar.get_name pvar = Mangled.from_string "self" &&
procedure_attr.ProcAttributes.is_objc_instance_method in
let is_cpp_this pvar =
!Config.curr_language = Config.C_CPP && Pvar.is_this pvar &&
!Config.curr_language = Config.Clang && Pvar.is_this pvar &&
procedure_attr.ProcAttributes.is_cpp_instance_method in
let do_hpred = function
| Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) ->
@ -1255,7 +1255,7 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs
else None in
let index_missing_opt =
if index_missing != [] &&
(!Config.Experiment.allow_missing_index_in_proc_call || !Config.footprint)
(Config.allow_missing_index_in_proc_call || !Config.footprint)
then Some (Sil.Earray (size1, index_missing, inst1))
else None in
subs'', index_frame_opt, index_missing_opt
@ -1600,7 +1600,7 @@ end
let cast_exception tenv texp1 texp2 e1 subs =
let _ = match texp1, texp2 with
| Sil.Sizeof (t1, _), Sil.Sizeof (t2, st2) ->
if !Config.developer_mode ||
if Config.developer_mode ||
(Sil.Subtype.is_cast st2 &&
not (Subtyping_check.check_subtype tenv t1 t2)) then
ProverState.checks := Class_cast_check (texp1, texp2, e1) :: !ProverState.checks
@ -1679,7 +1679,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
(** pre-process implication between a non-array and an array: the non-array is turned into an array of size given by its type
only active in type_size mode *)
let sexp_imply_preprocess se1 texp1 se2 = match se1, texp1, se2 with
| Sil.Eexp (_, inst), Sil.Sizeof _, Sil.Earray _ when !Config.type_size ->
| Sil.Eexp (_, inst), Sil.Sizeof _, Sil.Earray _ when Config.type_size ->
let se1' = Sil.Earray (texp1, [(Sil.exp_zero, se1)], inst) in
L.d_strln_color Orange "sexp_imply_preprocess"; L.d_str " se1: "; Sil.d_sexp se1; L.d_ln (); L.d_str " se1': "; Sil.d_sexp se1'; L.d_ln ();
se1'
@ -1934,7 +1934,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
let sexp =
let index = Sil.exp_int (Sil.Int.of_int (String.length s)) in
match !Config.curr_language with
| Config.C_CPP ->
| Config.Clang ->
Sil.Earray (size, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none)
| Config.Java ->
let mk_fld_sexp s =
@ -1945,7 +1945,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
Sil.Estruct (IList.map mk_fld_sexp fields, Sil.inst_none) in
let const_string_texp =
match !Config.curr_language with
| Config.C_CPP -> Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size), Sil.Subtype.exact)
| Config.Clang -> Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size), Sil.Subtype.exact)
| Config.Java ->
let object_type =
Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in
@ -2088,7 +2088,8 @@ let check_array_bounds (sub1, sub2) prop =
let check_failed atom =
ProverState.checks := Bounds_check :: !ProverState.checks;
L.d_str_color Red "bounds_check failed: provable atom: "; Sil.d_atom atom; L.d_ln();
if (not !Config.Experiment.bound_error_allowed_in_procedure_call) then raise (IMPL_EXC ("bounds check", (sub1, sub2), EXC_FALSE)) in
if (not Config.bound_error_allowed_in_procedure_call) then
raise (IMPL_EXC ("bounds check", (sub1, sub2), EXC_FALSE)) in
let fail_if_le e' e'' =
let lt_ineq = Prop.mk_inequality (Sil.BinOp(Sil.Le, e', e'')) in
if check_atom prop lt_ineq then check_failed lt_ineq in

@ -76,7 +76,7 @@ let check_bad_index pname p size index loc =
(** Perform bounds checking *)
let bounds_check pname prop size e =
if !Config.trace_rearrange then
if Config.trace_rearrange then
begin
L.d_str "Bounds check index:"; Sil.d_exp e;
L.d_str " size: "; Sil.d_exp size;
@ -86,7 +86,7 @@ let bounds_check pname prop size e =
let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp t
(off: Sil.offset list) inst : Sil.atom list * Sil.strexp * Sil.typ =
if !Config.trace_rearrange then
if Config.trace_rearrange then
begin
L.d_increase_indent 1;
L.d_strln "entering create_struct_values";
@ -167,7 +167,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
L.d_str "create_struct_values type:"; Sil.d_typ_full t; L.d_str " off: "; Sil.d_offset_list off; L.d_ln();
assert false in
if !Config.trace_rearrange then
if Config.trace_rearrange then
begin
let _, se, _ = res in
L.d_strln "exiting create_struct_values, returning";
@ -246,7 +246,7 @@ let rec _strexp_extend_values
let size = match se with
| Sil.Eexp (_, Sil.Ialloc) -> Sil.exp_one (* if allocated explicitly, we know size is 1 *)
| _ ->
if !Config.type_size then Sil.exp_one (* Sil.Sizeof (typ, Sil.Subtype.exact) *)
if Config.type_size then Sil.exp_one (* Sil.Sizeof (typ, Sil.Subtype.exact) *)
else Sil.exp_get_undefined false in
let se_new = Sil.Earray(size, [(Sil.exp_zero, se)], inst) in
@ -379,8 +379,10 @@ let strexp_extend_values
if footprint_part then
off', IList.map (fun (id, e) -> Prop.mk_eq (Sil.Var id) e) eqs
else off, [] in
if !Config.trace_rearrange then (L.d_str "entering strexp_extend_values se: "; Sil.d_sexp se; L.d_str " typ: ";
Sil.d_typ_full typ; L.d_str " off': "; Sil.d_offset_list off'; L.d_strln (if footprint_part then " FP" else " RE"));
if Config.trace_rearrange then
(L.d_str "entering strexp_extend_values se: "; Sil.d_sexp se; L.d_str " typ: ";
Sil.d_typ_full typ; L.d_str " off': "; Sil.d_offset_list off';
L.d_strln (if footprint_part then " FP" else " RE"));
let atoms_se_typ_list =
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se typ off' inst in
@ -389,7 +391,7 @@ let strexp_extend_values
let check_neg_atom atom = Prover.check_atom Prop.prop_emp (neg_atom atom) in
let check_not_inconsistent (atoms, _, _) = not (IList.exists check_neg_atom atoms) in
IList.filter check_not_inconsistent atoms_se_typ_list in
if !Config.trace_rearrange then L.d_strln "exiting strexp_extend_values";
if Config.trace_rearrange then L.d_strln "exiting strexp_extend_values";
let st = match te with
| Sil.Sizeof(_, st) -> st
| _ -> Sil.Subtype.exact in
@ -408,9 +410,9 @@ let mk_ptsto_exp_footprint
then begin
(* in angelic mode, purposely ignore dangling pointer warnings during the footprint phase -- we
* will fix them during the re - execution phase *)
if not (!Config.angelic_execution && !Config.footprint) then
if not (Config.angelic_execution && !Config.footprint) then
begin
if !Config.developer_mode then
if Config.developer_mode then
L.err "!!!! Footprint Error, Bad Root : %a !!!! @\n" (Sil.pp_exp pe_text) lexp;
let deref_str = Localise.deref_str_dangling None in
let err_desc =
@ -422,7 +424,7 @@ let mk_ptsto_exp_footprint
end;
let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
let st = match !Config.curr_language with
| Config.C_CPP -> Sil.Subtype.exact
| Config.Clang -> Sil.Subtype.exact
| Config.Java -> Sil.Subtype.subtypes in
let create_ptsto footprint_part off0 = match root, off0, typ with
| Sil.Lvar pvar, [], Sil.Tfun _ ->
@ -477,7 +479,8 @@ let fav_max_stamp fav =
[lexp] -- field splitting model. It also materializes all
indices accessed in lexp. *)
let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
if !Config.trace_rearrange then (L.d_str "entering prop_iter_extend_ptsto lexp: "; Sil.d_exp lexp; L.d_ln ());
if Config.trace_rearrange then
(L.d_str "entering prop_iter_extend_ptsto lexp: "; Sil.d_exp lexp; L.d_ln ());
let offset = Sil.exp_get_offsets lexp in
let max_stamp = fav_max_stamp (Prop.prop_iter_fav iter) in
let max_stamp_val = !max_stamp in
@ -507,7 +510,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
let iter' = IList.fold_left (Prop.prop_iter_add_atom !Config.footprint) iter atoms in
Prop.prop_iter_update_current iter' (Sil.Hpointsto (e, se, te)) in
let do_extend e se te =
if !Config.trace_rearrange then begin
if Config.trace_rearrange then begin
L.d_strln "entering do_extend";
L.d_str "e: "; Sil.d_exp e; L.d_str " se : "; Sil.d_sexp se; L.d_str " te: "; Sil.d_texp_full te;
L.d_ln (); L.d_ln ()
@ -618,12 +621,12 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
exception ARRAY_ACCESS
let rearrange_arith lexp prop =
if !Config.trace_rearrange then begin
if Config.trace_rearrange then begin
L.d_strln "entering rearrange_arith";
L.d_str "lexp: "; Sil.d_exp lexp; L.d_ln ();
L.d_str "prop: "; L.d_ln (); Prop.d_prop prop; L.d_ln (); L.d_ln ()
end;
if (!Config.array_level >= 2) then raise ARRAY_ACCESS
if (Config.array_level >= 2) then raise ARRAY_ACCESS
else
let root = Sil.root_of_lexp lexp in
if Prover.check_allocatedness prop root then
@ -638,7 +641,7 @@ let pp_rearrangement_error message prop lexp =
(** do re-arrangment for an iter whose current element is a pointsto *)
let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
if !Config.trace_rearrange then begin
if Config.trace_rearrange then begin
L.d_increase_indent 1;
L.d_strln "entering iter_rearrange_ptsto";
L.d_str "lexp: "; Sil.d_exp lexp; L.d_ln ();
@ -677,7 +680,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
| _ -> [iter]
end in
begin
if !Config.trace_rearrange then begin
if Config.trace_rearrange then begin
L.d_strln "exiting iter_rearrange_ptsto, returning results";
Prop.d_proplist_with_typ (IList.map Prop.prop_iter_to_prop res);
L.d_decrease_indent 1;
@ -688,7 +691,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
(** do re-arrangment for an iter whose current element is a nonempty listseg *)
let iter_rearrange_ne_lseg recurse_on_iters iter para e1 e2 elist =
if (!Config.nelseg) then
if Config.nelseg then
let iter_inductive_case =
let n' = Sil.Var (Ident.create_fresh Ident.kprimed) in
let (_, para_inst1) = Sil.hpara_instantiate para e1 n' elist in
@ -848,7 +851,7 @@ let rec iter_rearrange
inst: (Sil.offset list) Prop.prop_iter list =
let typ = match Sil.exp_get_offsets lexp with
| Sil.Off_fld (f, ((Sil.Tstruct _) as struct_typ)) :: _ -> (* access through field: get the struct type from the field *)
if !Config.trace_rearrange then begin
if Config.trace_rearrange then begin
L.d_increase_indent 1;
L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Ident.fieldname_to_string f);
L.d_str " type from instruction: "; Sil.d_typ_full typ_from_instr; L.d_ln();
@ -859,7 +862,7 @@ let rec iter_rearrange
struct_typ
| _ ->
typ_from_instr in
if !Config.trace_rearrange then begin
if Config.trace_rearrange then begin
L.d_increase_indent 1;
L.d_strln "entering iter_rearrange";
L.d_str "lexp: "; Sil.d_exp lexp; L.d_ln ();
@ -869,11 +872,11 @@ let rec iter_rearrange
L.d_ln (); L.d_ln ()
end;
let default_case_iter (iter': unit Prop.prop_iter) =
if !Config.trace_rearrange then L.d_strln "entering default_case_iter";
if Config.trace_rearrange then L.d_strln "entering default_case_iter";
if !Config.footprint then
prop_iter_add_hpred_footprint pname tenv prop iter' (lexp, typ) inst
else
if (!Config.array_level >= 1 && not !Config.footprint && Sil.exp_pointer_arith lexp)
if (Config.array_level >= 1 && not !Config.footprint && Sil.exp_pointer_arith lexp)
then rearrange_arith lexp prop
else begin
pp_rearrangement_error "cannot find predicate with root" prop lexp;
@ -906,7 +909,7 @@ let rec iter_rearrange
| Some iter ->
match Prop.prop_iter_current iter with
| (Sil.Hpointsto (_, _, texp), off) ->
if !Config.type_size then check_type_size pname prop texp off typ_from_instr;
if Config.type_size then check_type_size pname prop texp off typ_from_instr;
iter_rearrange_ptsto pname tenv prop iter lexp inst
| (Sil.Hlseg (Sil.Lseg_NE, para, e1, e2, elist), _) ->
iter_rearrange_ne_lseg recurse_on_iters iter para e1 e2 elist
@ -926,7 +929,7 @@ let rec iter_rearrange
| Some _, _ -> iter_rearrange_pe_dllseg_first recurse_on_iters default_case_iter iter para_dll e1 e2 e3 e4 elist
| _, Some _ -> iter_rearrange_pe_dllseg_last recurse_on_iters default_case_iter iter para_dll e1 e2 e3 e4 elist
end in
if !Config.trace_rearrange then begin
if Config.trace_rearrange then begin
L.d_strln "exiting iter_rearrange, returning results";
Prop.d_proplist_with_typ (IList.map Prop.prop_iter_to_prop res);
L.d_decrease_indent 1;
@ -983,7 +986,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
let is_deref_of_nullable =
let is_definitely_non_null exp prop =
Prover.check_disequal prop exp Sil.exp_zero in
!Config.report_nullable_inconsistency && not (is_definitely_non_null root prop)
Config.report_nullable_inconsistency && not (is_definitely_non_null root prop)
&& is_only_pt_by_nullable_fld_or_param root in
let relevant_attributes_getters = [
Prop.get_resource_attribute;
@ -1026,7 +1029,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
let err_desc = Errdesc.explain_dereference deref_str prop (State.get_loc ()) in
raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__))
| Some (Sil.Aundef (s, _, undef_loc, _)) ->
if !Config.angelic_execution then ()
if Config.angelic_execution then ()
else
let deref_str = Localise.deref_str_undef (s, undef_loc) in
let err_desc = Errdesc.explain_dereference deref_str prop loc in
@ -1071,7 +1074,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc =
Some (Sil.Lfield(e'', fn, t)), true (* the block dereferences is a field of an object*)
| Some (_, e) -> Some e, false
| _ -> None, false in
if (!Config.curr_language = Config.C_CPP) &&
if (!Config.curr_language = Config.Clang) &&
fun_exp_may_be_null () &&
not (is_fun_exp_captured_var ()) then
begin
@ -1085,7 +1088,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc =
| _ -> err_desc_nobuckets) in
let err_desc =
Localise.error_desc_set_bucket
err_desc_nobuckets' Localise.BucketLevel.b1 !Config.show_buckets in
err_desc_nobuckets' Localise.BucketLevel.b1 Config.show_buckets in
if is_field_deref then
raise
(Exceptions.Field_not_null_checked
@ -1099,7 +1102,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc =
either is a local or it's a modified param *)
let err_desc =
Localise.error_desc_set_bucket
err_desc_nobuckets Localise.BucketLevel.b1 !Config.show_buckets in
err_desc_nobuckets Localise.BucketLevel.b1 Config.show_buckets in
raise (Exceptions.Null_dereference
(err_desc, __POS__))
end

@ -519,7 +519,7 @@ let res_dir_specs_filename pname =
let specs_library_filenames pname =
IList.map
(fun specs_dir -> DB.filename_from_string (Filename.concat specs_dir (specs_filename pname)))
!Config.specs_library
Config.specs_library
(** paths to the .specs file for the given procedure in the models folder *)
let specs_models_filename pname =
@ -540,10 +540,10 @@ let store_summary pname (summ: summary) =
}
| None -> payload in
let summ1 = { summ with payload = process_payload summ.payload } in
let summ2 = if !Config.save_compact_summaries
let summ2 = if Config.save_compact_summaries
then summary_compact (Sil.create_sharing_env ()) summ1
else summ1 in
let summ3 = if !Config.save_time_in_summaries
let summ3 = if Config.save_time_in_summaries
then summ2
else
{ summ2 with

@ -387,7 +387,7 @@ let call_should_be_skipped callee_pname summary =
(* skip abstract methods *)
|| summary.Specs.attributes.ProcAttributes.is_abstract
(* treat calls with no specs as skip functions in angelic mode *)
|| (!Config.angelic_execution && Specs.get_specs_from_payload summary == [])
|| (Config.angelic_execution && Specs.get_specs_from_payload summary == [])
(** In case of constant string dereference, return the result immediately *)
let check_constant_string_dereference lexp =
@ -828,7 +828,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
let add_tainted_post ret_exp callee_pname prop =
Prop.add_or_replace_exp_attribute prop ret_exp (Sil.Ataint callee_pname) in
if !Config.angelic_execution && not (is_rec_call callee_pname) then
if Config.angelic_execution && not (is_rec_call callee_pname) then
(* introduce a fresh program variable to allow abduction on the return value *)
let abducted_ret_pv = Pvar.mk_abducted_ret callee_pname callee_loc in
(* prevent introducing multiple abducted retvals for a single call site in a loop *)
@ -842,7 +842,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
(* bind return id to the abducted value pointed to by the pvar we introduced *)
bind_exp_to_abducted_val ret_exp abducted_ret_pv prop in
let prop'' = add_ret_non_null ret_exp typ prop' in
if !Config.taint_analysis && Taint.returns_tainted callee_pname None then
if Config.taint_analysis && Taint.returns_tainted callee_pname None then
add_tainted_post ret_exp { Sil.taint_source = callee_pname; taint_kind = Unknown } prop''
else prop''
else add_ret_non_null ret_exp typ prop
@ -886,7 +886,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
Prop.add_or_replace_exp_attribute prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit)
else prop' in
let prop''' =
if !Config.taint_analysis
if Config.taint_analysis
then add_taint prop'' id rhs_exp pname tenv
else prop'' in
prop''' :: acc in
@ -917,7 +917,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
else callee_opt in
IList.fold_left fold_undef_pname None (Prop.get_exp_attributes prop exp) in
let prop' =
if !Config.angelic_execution then
if Config.angelic_execution then
(* when we try to deref an undefined value, add it to the footprint *)
match exp_get_undef_attr n_rhs_exp' with
| Some (Sil.Aundef (callee_pname, ret_annots, callee_loc, _)) ->
@ -930,7 +930,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
Rearrange.rearrange ~report_deref_errors pdesc tenv n_rhs_exp' typ prop' loc in
IList.rev (IList.fold_left (execute_letderef_ pdesc tenv id loc) [] iter_list)
with Rearrange.ARRAY_ACCESS ->
if (!Config.array_level = 0) then assert false
if (Config.array_level = 0) then assert false
else
let undef = Sil.exp_get_undefined false in
[Prop.conjoin_eq (Sil.Var id) undef prop_]
@ -969,7 +969,7 @@ let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp
let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in
IList.rev (IList.fold_left (execute_set_ pdesc tenv n_rhs_exp) [] iter_list)
with Rearrange.ARRAY_ACCESS ->
if (!Config.array_level = 0) then assert false
if (Config.array_level = 0) then assert false
else [prop_]
(** Execute [instr] with a symbolic heap [prop].*)
@ -1034,7 +1034,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
(* in comparisons, nil is translated as (void * ) 0 rather than 0 *)
let is_comparison_to_nil = function
| Sil.Cast ((Sil.Tptr (Sil.Tvoid, _)), exp) ->
!Config.curr_language = Config.C_CPP && Sil.exp_is_zero exp
!Config.curr_language = Config.Clang && Sil.exp_is_zero exp
| _ -> false in
match Prop.exp_normalize_prop Prop.prop_emp cond with
| Sil.Const (Sil.Cint i) when report_condition_always_true_false i ->
@ -1065,7 +1065,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let exn = Exceptions.Bad_pointer_comparison (desc, __POS__) in
Reporting.log_warning current_pname exn
| _ -> () in
if not !Config.report_runtime_exceptions then
if not Config.report_runtime_exceptions then
check_already_dereferenced current_pname cond prop__;
check_condition_always_true_false ();
let n_cond, prop = check_arith_norm_exp current_pname cond prop__ in
@ -1145,7 +1145,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let ret_typ_opt = Option.map Cfg.Procdesc.get_ret_type callee_pdesc_opt in
let sentinel_result =
if !Config.curr_language = Config.C_CPP then
if !Config.curr_language = Config.Clang then
check_variadic_sentinel_if_present
(call_args prop_r callee_pname actual_params ret_ids loc)
else [(prop_r, path)] in
@ -1244,7 +1244,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
IList.map
(Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_initial)
(IList.map add_None ptl) in
run_in_re_execution_mode (* no footprint vars for locals *)
Config.run_in_re_execution_mode (* no footprint vars for locals *)
sigma_locals () in
let sigma' = Prop.get_sigma prop_ @ sigma_locals in
let prop' = Prop.normalize (Prop.replace_sigma sigma' prop_) in
@ -1283,7 +1283,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
| hpred -> hpred)
(Prop.get_sigma prop) in
Prop.normalize (Prop.replace_sigma sigma' prop) in
if !Config.angelic_execution then
if Config.angelic_execution then
let add_actual_by_ref_to_footprint prop (actual, actual_typ) =
match actual with
| Sil.Lvar actual_pv ->
@ -1391,7 +1391,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
IList.fold_left do_attribute p (Prop.get_exp_attributes p e) in
IList.fold_left do_exp prop actual_pars in
let add_tainted_pre prop actuals caller_pname callee_pname =
if !Config.taint_analysis then
if Config.taint_analysis then
match Taint.accepts_sensitive_params callee_pname None with
| [] -> prop
| param_nums ->
@ -1587,7 +1587,7 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= act
(* In case we call an objc instance method we add and extra spec *)
(* were the receiver is null and the semantics of the call is nop*)
let callee_attrs = Specs.get_attributes summary in
if (!Config.curr_language <> Config.Java) && !Config.objc_method_call_semantics &&
if (!Config.curr_language <> Config.Java) && Config.objc_method_call_semantics &&
(Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then
handle_objc_method_call actual_pars actual_params pre tenv ret_ids pdesc callee_pname loc
path (Tabulation.exe_function_call callee_attrs)
@ -1646,7 +1646,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa
L.d_str "Instruction "; Sil.d_instr instr; L.d_ln ();
let prop', fav_normal = pre_process_prop prop in
let res_list =
run_with_abs_val_equal_zero (* no exp abstraction during sym exe *)
Config.run_with_abs_val_equal_zero (* no exp abstraction during sym exe *)
(fun () -> sym_exec tenv pdesc instr prop' path)
() in
let res_list_nojunk =
@ -1663,7 +1663,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa
Paths.PathSet.from_renamed_list results
with exn when Exceptions.handle_exception exn && !Config.footprint ->
handle_exn exn; (* calls State.mark_instr_fail *)
if !Config.nonstop
if Config.nonstop
then
(* in nonstop mode treat the instruction as skip *)
(Paths.PathSet.from_renamed_list [(prop, path)])

@ -336,7 +336,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
match deref_err_list with
| [] -> None
| deref_err :: _ ->
if !Config.angelic_execution then
if Config.angelic_execution then
(* In angelic mode, prefer to report Deref_null over other kinds of deref errors. this
* makes sure we report a NULL_DEREFERENCE instead of
a less interesting PRECONDITION_NOT_MET
@ -554,7 +554,7 @@ let prop_footprint_add_pi_sigma_starfld_sigma
let fav = Prop.sigma_fav [hpred] in
(* TODO (t4893479): make this check less angelic *)
if Sil.fav_exists fav
(fun id -> not (Ident.is_footprint id) && not !Config.angelic_execution)
(fun id -> not (Ident.is_footprint id) && not Config.angelic_execution)
then begin
L.d_warning "found hpred with non-footprint variable, dropping the spec";
L.d_ln (); Sil.d_hpred hpred; L.d_ln ();
@ -824,7 +824,7 @@ let add_param_taint proc_name formal_params prop param_nums =
(* add Auntaint attribute to a callee_pname precondition *)
let mk_pre pre formal_params callee_pname callee_attrs =
if !Config.taint_analysis then
if Config.taint_analysis then
add_tainting_att_param_list
(Prop.normalize pre)
(Taint.accepts_sensitive_params callee_pname (Some callee_attrs))
@ -902,10 +902,10 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
IList.map taint_retval posts
else posts in
let posts' =
if !Config.idempotent_getters && !Config.curr_language = Config.Java
if Config.idempotent_getters && !Config.curr_language = Config.Java
then mk_getter_idempotent posts
else posts in
if !Config.taint_analysis then mk_retval_tainted posts' else posts'
if Config.taint_analysis then mk_retval_tainted posts' else posts'
| _ -> posts
(** Check if actual_pre * missing_footprint |- false *)
@ -1025,7 +1025,7 @@ let exe_spec
Reporting.log_warning caller_pname exn in
let do_split () =
let missing_pi' =
if !Config.taint_analysis then
if Config.taint_analysis then
do_taint_check caller_pname callee_pname actual_pre missing_pi sub2
else missing_pi in
process_splitting
@ -1054,7 +1054,7 @@ let exe_spec
IList.iter log_check_exn checks;
let subbed_pre = (Prop.prop_sub sub1 actual_pre) in
match check_dereferences callee_pname subbed_pre sub2 spec_pre formal_params with
| Some (Deref_undef _, _) when !Config.angelic_execution ->
| Some (Deref_undef _, _) when Config.angelic_execution ->
let split = do_split () in
report_valid_res split
| Some (deref_error, desc) ->
@ -1249,7 +1249,7 @@ let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc result
IList.length (Procname.java_get_parameters pn_java) = 0
| _ ->
false in
(!Config.idempotent_getters &&
(Config.idempotent_getters &&
!Config.curr_language = Config.Java &&
is_likely_getter callee_pname)
|| returns_nullable ret_annot in

@ -154,7 +154,7 @@ let sinks = [
ret_type = "void";
params = [];
is_static = false;
language = Config.C_CPP
language = Config.Clang
}, [1]); (* it's instance method *)
] @ FbTaint.sinks
@ -166,7 +166,7 @@ let functions_with_tainted_params = [
ret_type = "BOOL";
params = [];
is_static = false; (* it's instance method *)
language = Config.C_CPP
language = Config.Clang
}, [2]);
(* actual specs *)
@ -180,7 +180,7 @@ let functions_with_tainted_params = [
ret_type = "BOOL";
params = [];
is_static = false; (* it's instance method *)
language = Config.C_CPP
language = Config.Clang
}, [2]);
] @ FbTaint.functions_with_tainted_params
@ -203,7 +203,7 @@ let objc_method_to_procname objc_method =
let method_str_to_pname method_str =
match method_str.language with
| Config.C_CPP ->
| Config.Clang ->
objc_method_to_procname method_str
| Config.Java ->
java_method_to_procname method_str

@ -362,8 +362,8 @@ let create_outfile fname =
None
(** operate on an outfile reference if it is not None *)
let do_outf outf_ref f =
match !outf_ref with
let do_outf outf_opt f =
match outf_opt with
| None -> ()
| Some outf ->
f outf
@ -464,238 +464,6 @@ let filename_to_relative root fname =
remainder
(* Type of command-line arguments before processing *)
type arg_list = (string * Arg.spec * string option * string) list
let arg_desc_filter options_to_keep =
IList.filter (function (option_name, _, _, _) -> IList.mem string_equal option_name options_to_keep)
(* Given a filename with a list of paths, convert it into a list of string iff they are absolute *)
let read_specs_dir_list_file fname =
let validate_path path =
if Filename.is_relative path then
failwith ("Failing because path " ^ path ^ " is not absolute") in
match read_file fname with
| Some pathlist ->
IList.iter validate_path pathlist;
pathlist
| None -> failwith ("cannot read file " ^ fname)
let base_arg_desc =
[
"-results_dir",
Arg.String (fun s -> Config.results_dir := s),
Some "dir",
"set the project results directory (default dir=" ^ Config.default_results_dir ^ ")";
"-coverage",
Arg.Unit (fun () -> Config.worklist_mode:= 2),
None,
"analysis mode to maximize coverage (can take longer)";
"-lib",
Arg.String (fun s -> Config.specs_library := filename_to_absolute s :: !Config.specs_library),
Some "dir",
"add dir to the list of directories to be searched for spec files";
"-specs-dir-list-file",
Arg.String (fun s -> Config.specs_library := (read_specs_dir_list_file s) @ !Config.specs_library),
Some "file",
"add the newline-separated directories listed in <file> to the list of directories to \
be searched for spec files";
"-models",
Arg.String (fun s -> Config.add_models (filename_to_absolute s)),
Some "zip file",
"add a zip file containing the models";
"-ziplib",
Arg.String (fun s -> Config.add_zip_library (filename_to_absolute s)),
Some "zip file",
"add a zip file containing library spec files";
"-project_root",
Arg.String (fun s -> Config.project_root := Some (filename_to_absolute s)),
Some "dir",
"root directory of the project";
"-infer_cache",
Arg.String (fun s -> Config.infer_cache := Some (filename_to_absolute s)),
Some "dir",
"Select a directory to contain the infer cache";
"-inferconfig_home",
Arg.String (fun s -> Config.inferconfig_home := Some s),
Some "dir",
"Path to the .inferconfig file";
]
let reserved_arg_desc =
[
"-absstruct",
Arg.Set_int Config.abs_struct,
Some "n",
"abstraction level for fields of structs (default n = 1)"
;
"-absval",
Arg.Set_int Config.abs_val,
Some "n",
"abstraction level for expressions (default n = 2)";
"-arraylevel",
Arg.Set_int Config.array_level,
Some "n",
"the level of treating the array indexing and pointer arithmetic (default n = 0)"
;
"-developer_mode",
Arg.Set Config.developer_mode,
None,
"reserved"
;
"-dotty",
Arg.Set Config.write_dotty,
None,
"produce dotty files in the results directory";
"-exit_node_bias",
Arg.Unit (fun () -> Config.worklist_mode:= 1),
None,
"nodes nearest the exit node are analyzed first";
"-html",
Arg.Set Config.write_html,
None,
"produce hmtl output in the results directory"
;
"-join_cond",
Arg.Set_int Config.join_cond,
Some "n",
"set the strength of the final information-loss check used by the join (default n=1)"
;
"-leak",
Arg.Set Config.allowleak,
None,
"forget leaks during abstraction"
;
"-monitor_prop_size",
Arg.Set Config.monitor_prop_size,
None,
"monitor size of props"
;
"-nelseg",
Arg.Set Config.nelseg,
None,
"use only nonempty lsegs"
;
"-noliveness",
Arg.Clear Config.liveness,
None,
"turn the dead program variable elimination off"
;
"-noprintdiff",
Arg.Clear Config.print_using_diff,
None,
"turn off highlighting diff w.r.t. previous prop in printing"
;
"-notest",
Arg.Clear Config.test,
None,
"turn test mode off"
;
"-only_footprint",
Arg.Set Config.only_footprint,
None,
"skip the re-execution phase"
;
"-print_types",
Arg.Set Config.print_types,
None,
"print types in symbolic heaps"
;
"-set_pp_margin",
Arg.Int (fun i -> F.set_margin i),
Some "n",
"set right margin for the pretty printing functions"
;
"-spec_abs_level",
Arg.Set_int Config.spec_abs_level,
Some "n",
"set the level of abstracting the postconditions of discovered specs (default n=1)"
;
"-trace_error",
Arg.Set Config.trace_error,
None,
"turn on tracing of error explanation"
;
"-trace_join",
Arg.Set Config.trace_join,
None,
"turn on tracing of join"
;
"-trace_rearrange",
Arg.Set Config.trace_rearrange,
None,
"turn on tracing of rearrangement"
;
"-visits_bias",
Arg.Unit (fun () -> Config.worklist_mode:= 2),
None,
"nodes visited fewer times are analyzed first"
;
]
module Arg = struct
include Arg
(** Custom version of Arg.aling so that keywords are on one line and documentation is on the next *)
let align arg_desc =
let do_arg (key, spec, doc) =
let first_space =
try
let index = String.index doc ' ' in
if String.get doc index = '=' then 0 else index
with Not_found -> 0 in
let len = String.length doc in
let doc1 = String.sub doc 0 first_space in
let doc2 = String.sub doc first_space (len - first_space) in
if len = 0 then (key, spec, doc)
else (key, spec, doc1 ^ "\n " ^ doc2) in
IList.map do_arg arg_desc
type aligned = (key * spec * doc)
(** Create a group of sorted command-line arguments *)
let create_options_desc double_minus title unsorted_desc =
let handle_double_minus (opname, spec, param_opt, text) = match param_opt with
| None ->
if double_minus then ("-"^opname, spec, " " ^ text)
else (opname, spec, " " ^ text)
| Some param ->
if double_minus then ("-"^opname, spec, "=" ^ param ^ " " ^ text)
else (opname, spec, param ^ " " ^ text) in
let unsorted_desc' = IList.map handle_double_minus unsorted_desc in
let dlist =
("", Arg.Unit (fun () -> ()), " \n " ^ title ^ "\n") ::
IList.sort (fun (x, _, _) (y, _, _) -> Pervasives.compare x y) unsorted_desc' in
align dlist
let env_to_argv env =
Str.split (Str.regexp ":") env
let prepend_to_argv args =
let cl_args = match Array.to_list Sys.argv with _ :: tl -> tl | [] -> [] in
Sys.executable_name :: args @ cl_args
let parse env_var spec anon usage =
let env_args = env_to_argv (try Unix.getenv env_var with Not_found -> "") in
let env_cl_args = prepend_to_argv env_args in
try
Arg.parse_argv (Array.of_list env_cl_args) spec anon usage
with
| Bad usage -> Pervasives.prerr_string usage; exit 2;
| Help usage -> Pervasives.print_string usage; exit 0;
end
(** flags for a procedure *)
type proc_flags = (string, string) Hashtbl.t
@ -767,26 +535,24 @@ let directory_iter f path =
type analyzer = Infer | Eradicate | Checkers | Tracing
let analyzers = [Infer; Eradicate; Checkers; Tracing]
let string_to_analyzer =
[("infer", Infer); ("eradicate", Eradicate); ("checkers", Checkers); ("tracing", Tracing)]
let analyzers = IList.map snd string_to_analyzer
let string_of_analyzer = function
| Infer -> "infer"
| Eradicate -> "eradicate"
| Checkers -> "checkers"
| Tracing -> "tracing"
let string_of_analyzer =
let analyzer_to_string = IList.map (fun (a,n) -> (n,a)) string_to_analyzer in
fun analyzer ->
IList.assoc ( = ) analyzer analyzer_to_string
exception Unknown_analyzer
let analyzer_of_string = function
| "infer" -> Infer
| "eradicate" -> Eradicate
| "checkers" -> Checkers
| "tracing" -> Tracing
| _ -> raise Unknown_analyzer
let analyzer_of_string name =
try IList.assoc string_equal name string_to_analyzer
with Not_found -> raise Unknown_analyzer
let string_crc_hex32 =
Config.string_crc_hex32 (* implemented in Config to avoid circularities *)
let string_crc_hex32 s = Digest.to_hex (Digest.string s)
let string_append_crc_cutoff ?(cutoff=100) ?(key="") name =
let name_up_to_cutoff =
@ -797,26 +563,3 @@ let string_append_crc_cutoff ?(cutoff=100) ?(key="") name =
let name_for_crc = name ^ key in
string_crc_hex32 name_for_crc in
name_up_to_cutoff ^ "." ^ crc_str
let set_reference_and_call_function reference value f x =
let saved = !reference in
let restore () =
reference := saved in
try
reference := value;
let res = f x in
restore ();
res
with
| exn ->
restore ();
raise exn
let run_in_re_execution_mode f x =
set_reference_and_call_function Config.footprint false f x
let run_in_footprint_mode f x =
set_reference_and_call_function Config.footprint true f x
let run_with_abs_val_equal_zero f x =
set_reference_and_call_function Config.abs_val 0 f x

@ -148,36 +148,6 @@ val pp_current_time : Format.formatter -> unit -> unit
(** Print the time in seconds elapsed since the beginning of the execution of the current command. *)
val pp_elapsed_time : Format.formatter -> unit -> unit
module Arg : sig
include module type of Arg with type spec = Arg.spec
(** type of aligned commend-line options *)
type aligned = private (key * spec * doc)
val align : (key * spec * doc) list -> aligned list
(** [parse env_var arg_desc anon_fun usage_msg] prepends the decoded value of environment variable
[env_var] to [Sys.argv] and then parses the result using the standard [Arg.parse]. Therefore
arguments passed on the command line supercede those specified in the environment variable.
WARNING: If an argument appears both in the environment variable and on the command line, it
will be interpreted twice. *)
val parse : string -> aligned list -> anon_fun -> usage_msg -> unit
val usage : aligned list -> usage_msg -> unit
(** [create_options_desc double_minus unsorted_desc title] creates a group of sorted command-line arguments.
[double_minus] is a booleand indicating whether the [-- option = nn] format or [- option n] format is to be used.
[title] is the title of this group of options.
It expects a list [opname, desc, param_opt, text] where
[opname] is the name of the option
[desc] is the Arg.spec
[param_opt] is the optional parameter to [opname]
[text] is the description of the option *)
val create_options_desc : bool -> string -> (string * Arg.spec * string option * string) list -> aligned list
end
(** Compute a 32-character hexadecimal crc using the Digest module *)
val string_crc_hex32 : string -> string
@ -229,23 +199,11 @@ type outfile =
val create_outfile : string -> outfile option
(** operate on an outfile reference if it is not None *)
val do_outf : outfile option ref -> (outfile -> unit) -> unit
val do_outf : outfile option -> (outfile -> unit) -> unit
(** close an outfile *)
val close_outf : outfile -> unit
(* Type of command-line arguments before processing *)
type arg_list = (string * Arg.spec * string option * string) list
(* Filter arguments by name, i.e. keep those whose name appears in the name list *)
val arg_desc_filter : string list -> arg_list -> arg_list
(** Basic command-line arguments *)
val base_arg_desc : arg_list
(** Reserved command-line arguments *)
val reserved_arg_desc : arg_list
(** flags for a procedure *)
type proc_flags = (string, string) Hashtbl.t
@ -282,25 +240,12 @@ val directory_iter : (string -> unit) -> string -> unit
(** Various kind of analyzers *)
type analyzer = Infer | Eradicate | Checkers | Tracing
(** Association list of analyzers and their names *)
val string_to_analyzer : (string * analyzer) list
(** List of analyzers *)
val analyzers: analyzer list
val string_of_analyzer: analyzer -> string
val analyzer_of_string: string -> analyzer
(** Call f x with Config.abs_val set to zero.
Restore the initial value also in case of exception. *)
val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b
(** Call f x with Config.footprint set to true.
Restore the initial value of footprint also in case of exception. *)
val run_in_footprint_mode : ('a -> 'b) -> 'a -> 'b
(** Call f x with Config.footprint set to false.
Restore the initial value of footprint also in case of exception. *)
val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b
(** [set_reference_and_call_function ref val f x] calls f x with ref set to val.
Restore the initial value also in case of exception. *)
val set_reference_and_call_function : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c

@ -24,33 +24,33 @@ let load_from_cache serializer zip_path cache_dir zip_library =
if not (Sys.file_exists to_path) then
begin
DB.create_path (Filename.dirname to_path);
let zip_channel = Config.zip_channel zip_library in
let lazy zip_channel = zip_library.Config.zip_channel in
let entry = Zip.find_entry zip_channel zip_path in
Zip.copy_entry_to_file zip_channel entry to_path
end;
DB.filename_from_string to_path in
match deserialize (extract absolute_path) with
| Some data when Config.is_models zip_library -> Some (data, DB.Models)
| Some data when zip_library.Config.models -> Some (data, DB.Models)
| Some data -> Some (data, DB.Spec_lib)
| None -> None
| exception Not_found -> None
let load_from_zip serializer zip_path zip_library =
let zip_channel = Config.zip_channel zip_library in
let lazy zip_channel = zip_library.Config.zip_channel in
let deserialize = Serialization.from_string serializer in
match deserialize (Zip.read_entry zip_channel (Zip.find_entry zip_channel zip_path)) with
| Some data when Config.is_models zip_library -> Some (data, DB.Models)
| Some data when zip_library.Config.models -> Some (data, DB.Models)
| Some data -> Some (data, DB.Spec_lib)
| None -> None
| exception Not_found -> None
let load_data serializer path zip_library =
let zip_path = Filename.concat Config.default_in_zip_results_dir path in
match !Config.infer_cache with
match Config.infer_cache with
| None ->
load_from_zip serializer zip_path zip_library
| Some infer_cache ->
let cache_dir = get_cache_dir infer_cache (Config.zip_filename zip_library) in
let cache_dir = get_cache_dir infer_cache zip_library.Config.zip_filename in
load_from_cache serializer zip_path cache_dir zip_library
(* Search path in the list of zip libraries and use a cache directory to save already
@ -62,4 +62,4 @@ let load serializer path =
let opt = load_data serializer path zip_library in
if Option.is_some opt then opt
else loop other_libraries in
loop (Config.get_zip_libraries ())
loop Config.zip_libraries

@ -15,7 +15,6 @@ module L = Logging
module F = Format
let verbose = false
let query = ref None
let parse_query s =
let buf = Lexing.from_string s in
@ -34,7 +33,7 @@ let parse_query s =
assert false
let query_ast =
lazy (match !query with None -> parse_query "x(y)" | Some s -> parse_query s)
lazy (match Config.code_query with None -> parse_query "x(y)" | Some s -> parse_query s)
module Err = struct
(** Update the summary with stats from the checker. *)

@ -12,5 +12,3 @@ open! Utils
(** Module for code queries. *)
val code_query_callback : Callbacks.proc_callback_t
val query : string option ref

@ -16,7 +16,7 @@ module F = Format
(** Flags to activate checkers. *)
let active_procedure_checkers () =
let checkers_enabled = Config.checkers_enabled () in
let checkers_enabled = Config.checkers_enabled in
let java_checkers =
let l =
@ -31,8 +31,8 @@ let active_procedure_checkers () =
Dataflow.callback_test_dataflow, false;
FragmentRetainsViewChecker.callback_fragment_retains_view, checkers_enabled;
SqlChecker.callback_sql, false;
Eradicate.callback_eradicate, !Config.eradicate;
CodeQuery.code_query_callback, !CodeQuery.query <> None;
Eradicate.callback_eradicate, Config.eradicate;
CodeQuery.code_query_callback, Config.code_query <> None;
Checkers.callback_check_field_access, false;
ImmutableChecker.callback_check_immutable_cast, checkers_enabled;
RepeatedCallsChecker.callback_check_repeated_calls, checkers_enabled;
@ -46,7 +46,7 @@ let active_procedure_checkers () =
Checkers.callback_print_c_method_calls, false;
CheckDeadCode.callback_check_dead_code, checkers_enabled;
] in
IList.map (fun (x, y) -> (x, y, Some Config.C_CPP)) l in
IList.map (fun (x, y) -> (x, y, Some Config.Clang)) l in
java_checkers @ c_cpp_checkers

@ -150,7 +150,7 @@ let unary_operation_instruction uoi e typ loc =
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
let exp = if General_utils.is_cpp_translation !CFrontend_config.language then
let exp = if General_utils.is_cpp_translation Config.clang_lang then
e
else
e_plus_1 in
@ -164,7 +164,7 @@ let unary_operation_instruction uoi e typ loc =
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in
let exp = if General_utils.is_cpp_translation !CFrontend_config.language then
let exp = if General_utils.is_cpp_translation Config.clang_lang then
e
else
e_minus_1 in

@ -34,16 +34,16 @@ let compute_icfg tenv ast =
| _ -> assert false (* NOTE: Assumes that an AST alsways starts with a TranslationUnitDecl *)
let register_perf_stats_report source_file =
let stats_dir = Filename.concat !Config.results_dir Config.frontend_stats_dir_name in
let stats_dir = Filename.concat Config.results_dir Config.frontend_stats_dir_name in
let abbrev_source_file = DB.source_file_encoding source_file in
let stats_file = Config.perf_stats_prefix ^ "_" ^ abbrev_source_file ^ ".json" in
DB.create_dir !Config.results_dir ;
DB.create_dir Config.results_dir ;
DB.create_dir stats_dir ;
PerfStats.register_report_at_exit (Filename.concat stats_dir stats_file)
let init_global_state source_file =
register_perf_stats_report source_file ;
Config.curr_language := Config.C_CPP;
Config.curr_language := Config.Clang;
DB.current_source := source_file;
DB.Results_dir.init ();
Ident.NameGenerator.reset ();
@ -74,8 +74,8 @@ let do_source_file source_file ast =
(*Printing.print_procedures cfg; *)
General_utils.sort_fields_tenv tenv;
Tenv.store_to_file tenv_file tenv;
if !CFrontend_config.stats_mode then Cfg.check_cfg_connectedness cfg;
if !CFrontend_config.stats_mode
|| !CFrontend_config.debug_mode || !CFrontend_config.testing_mode then
if Config.stats_mode then Cfg.check_cfg_connectedness cfg;
if Config.stats_mode
|| Config.debug_mode || Config.testing_mode then
(Dotty.print_icfg_dotty cfg [];
Cg.save_call_graph_dotty None Specs.get_specs call_graph)

@ -11,12 +11,6 @@ open! Utils
(** Module that contains constants and variables used in the frontend *)
let no_translate_libs = ref true
let testing_mode = ref false
let cxx_experimental = ref false
let array_with_objects_count_m = "arrayWithObjects:count:"
let object_at_indexed_subscript_m = "objectAtIndexedSubscript:"
@ -49,46 +43,12 @@ let free = "free"
let static = "static"
let source_file : string option ref = ref None
let ast_file : string option ref = ref None
let json = ref ""
let pointer_decl_index = ref Clang_ast_main.PointerMap.empty
let pointer_stmt_index = ref Clang_ast_main.PointerMap.empty
let debug_mode = ref false
let stats_mode = ref false
let models_mode = ref false
type lang =
| C
| CPP
| OBJC
| OBJCPP
let language = ref OBJC (* Default is objc, since it's the default for clang (at least in Mac OS) *)
let lang_from_string lang_string =
let lang =
if lang_string = "c" then C
else if lang_string = "objective-c" then OBJC
else if lang_string = "c++" then CPP
else if lang_string = "objective-c++" then OBJCPP
else assert false in
language := lang
let lang_to_string lang =
match lang with
| C -> "c"
| OBJC -> "objective-c"
| CPP -> "c++"
| OBJCPP -> "objective-c++"
let emtpy_name_category ="EMPTY_NAME_CATEGORY_FOR_"
let objc_object = "objc_object"

@ -13,36 +13,6 @@ open! Utils
val global_translation_unit_decls : Clang_ast_t.decl list ref
(** arguments of InferClang *)
val debug_mode : bool ref
val stats_mode : bool ref
val models_mode : bool ref
val source_file : string option ref
type lang =
| C
| CPP
| OBJC
| OBJCPP
val lang_from_string : string -> unit
val lang_to_string : lang -> string
val language : lang ref
val ast_file : string option ref
val no_translate_libs : bool ref
val testing_mode : bool ref
val cxx_experimental : bool ref
(** constants *)
val json : string ref

@ -27,7 +27,7 @@ module CFrontend_decl_funct(T: CModule_type.CTranslation) : CFrontend_decl =
struct
let model_exists procname =
Specs.summary_exists_in_models procname && not !CFrontend_config.models_mode
Specs.summary_exists_in_models procname && not Config.models_mode
(* Translates the method/function's body into nodes of the cfg. *)
let add_method tenv cg cfg class_decl_opt procname body has_return_param is_objc_method
@ -189,7 +189,7 @@ struct
| Some (ClassTemplateSpecializationDecl _ as d) ->
let class_name = CTypes_decl.get_record_name d in
let curr_class = CContext.ContextCls(class_name, None, []) in
if !CFrontend_config.cxx_experimental then
if Config.cxx_experimental then
process_methods tenv cg cfg curr_class [dec]
| Some dec ->
Printing.log_stats "Methods of %s skipped\n" (Ast_utils.string_of_decl dec)

@ -18,11 +18,11 @@ module F = Format
module Printing =
struct
let log_out fmt =
let pp = if !CFrontend_config.debug_mode then Format.fprintf else Format.ifprintf in
let pp = if Config.debug_mode then Format.fprintf else Format.ifprintf in
pp Format.std_formatter fmt
let log_err fmt =
let pp = if !CFrontend_config.debug_mode then Format.fprintf else Format.ifprintf in
let pp = if Config.debug_mode then Format.fprintf else Format.ifprintf in
pp Format.err_formatter fmt
@ -36,7 +36,7 @@ struct
let log_stats fmt =
let pp =
if !CFrontend_config.stats_mode || !CFrontend_config.debug_mode
if Config.stats_mode || Config.debug_mode
then Format.fprintf else Format.ifprintf in
pp Format.std_formatter fmt
@ -405,13 +405,13 @@ struct
| _ -> false
let is_objc () =
match !CFrontend_config.language with
| CFrontend_config.OBJC -> true
match Config.clang_lang with
| Config.OBJC -> true
| _ -> false
let is_objcpp () =
match !CFrontend_config.language with
| CFrontend_config.OBJCPP -> true
match Config.clang_lang with
| Config.OBJCPP -> true
| _ -> false
(*
@ -569,7 +569,7 @@ struct
let get_rel_file_path file_opt =
match file_opt with
| Some file ->
(match !Config.project_root with
(match Config.project_root with
| Some root ->
DB.source_file_to_rel_path (DB.rel_source_file_from_abs_path root file)
| None -> file)
@ -587,8 +587,8 @@ struct
| None -> "" in
let type_string =
match language with
| CFrontend_config.CPP
| CFrontend_config.OBJCPP -> Ast_utils.string_of_type_ptr tp
| Config.CPP
| Config.OBJCPP -> Ast_utils.string_of_type_ptr tp
| _ -> "" in
(* remove __restrict from type name to avoid mismatches. Clang allows to declare function*)
(* with __restrict parameters and then define it without (it mostly applies to models).*)
@ -644,10 +644,6 @@ struct
| None -> Pvar.mk (Mangled.from_string name_string) procname
let is_cpp_translation language =
language = CFrontend_config.CPP || language = CFrontend_config.OBJCPP
language = Config.CPP || language = Config.OBJCPP
end

@ -197,7 +197,7 @@ sig
val mk_procname_from_objc_method : string -> string -> Procname.objc_method_kind -> Procname.t
val mk_procname_from_function : string -> (Clang_ast_t.decl_info * Clang_ast_t.function_decl_info)
option -> Clang_ast_t.type_ptr -> CFrontend_config.lang -> Procname.t
option -> Clang_ast_t.type_ptr -> Config.clang_lang -> Procname.t
val mk_procname_from_cpp_method : string -> string -> Clang_ast_t.type_ptr -> Procname.t
@ -208,6 +208,6 @@ sig
val mk_sil_var : Clang_ast_t.named_decl_info -> var_info option -> Procname.t -> Procname.t ->
Pvar.t
val is_cpp_translation : CFrontend_config.lang -> bool
val is_cpp_translation : Config.clang_lang -> bool
end

@ -24,7 +24,7 @@ let source_file_from_path path =
"ERROR: Path %s is relative. Please pass an absolute path in the -c argument.@."
path;
exit 1);
match !Config.project_root with
match Config.project_root with
| Some root ->
(try
DB.rel_source_file_from_abs_path root path
@ -77,7 +77,7 @@ let clang_to_sil_location clang_loc procdesc_opt =
Location.{line; col; file; nLOC}
let file_in_project file =
match !Config.project_root with
match Config.project_root with
| Some root ->
let file_in_project = string_is_prefix root file in
let paths = Lazy.force Inferconfig.skip_translation_headers in
@ -96,7 +96,7 @@ let should_do_frontend_check (loc_start, _) =
let equal_current_source file =
DB.source_file_equal (source_file_from_path file) !DB.current_source in
equal_current_source file ||
(file_in_project file && not !CFrontend_config.testing_mode)
(file_in_project file && not Config.testing_mode)
(* We translate by default the instructions in the current file.*)
(* In C++ development, we also translate the headers that are part *)
@ -126,11 +126,11 @@ let should_translate (loc_start, loc_end) decl_trans_context =
|| map_file_of equal_current_source loc_end
|| map_file_of equal_current_source loc_start
|| file_in_models
|| (!CFrontend_config.cxx_experimental && decl_trans_context = `Translation && file_in_project
&& not (!CFrontend_config.testing_mode))
|| (Config.cxx_experimental && decl_trans_context = `Translation && file_in_project
&& not Config.testing_mode)
let should_translate_lib source_range decl_trans_context =
not !CFrontend_config.no_translate_libs
not Config.no_translate_libs
|| should_translate source_range decl_trans_context
let get_sil_location_from_range source_range prefer_first =

@ -17,91 +17,6 @@ module L = Logging
open CFrontend_utils
let arg_desc =
let desc =
(Utils.arg_desc_filter ["-results_dir"] base_arg_desc) @
[
"-c",
Arg.String (fun cfile -> CFrontend_config.source_file := Some cfile),
Some "cfile",
"C File to translate"
;
"-x",
Arg.String (fun lang -> CFrontend_config.lang_from_string lang),
Some "cfile",
"Language (c, objective-c, c++, objc-++)"
;
"-ast",
Arg.String (fun file -> CFrontend_config.ast_file := Some file),
Some "file",
"AST file for the translation"
;
"-dotty_no_cfg_libs",
Arg.Unit (fun _ -> Config.dotty_cfg_libs := false),
None,
"Prints the cfg of the code coming from the libraries"
;
"-no_headers",
Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := true),
None,
"Do not translate code in header files (default)"
;
"-headers",
Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := false),
None,
"Translate code in header files"
;
"-testing_mode",
Arg.Unit (fun _ -> CFrontend_config.testing_mode := true),
None,
"Mode for testing, where no headers are translated, \
and dot files are created"
;
"-debug",
Arg.Unit (fun _ -> CFrontend_config.debug_mode := true),
None,
"Enables debug mode"
;
"-stats",
Arg.Unit (fun _ -> CFrontend_config.stats_mode := true),
None,
"Enables stats mode"
;
"-project_root",
Arg.String (fun s ->
Config.project_root := Some (Utils.filename_to_absolute s)),
Some "dir",
"Toot directory of the project"
;
"-fobjc-arc",
Arg.Unit (fun _ -> Config.arc_mode := true),
None,
"Translate with Objective-C Automatic Reference Counting (ARC)"
;
"-models_mode",
Arg.Unit (fun _ -> CFrontend_config.models_mode := true),
None,
"Mode for computing the models"
;
"-cxx-experimental",
Arg.Unit (fun _ -> CFrontend_config.cxx_experimental := true),
None,
"Analyze C++ methods, still experimental"
;
"-inferconfig_home",
Arg.String (fun s -> Config.inferconfig_home := Some s),
Some "dir",
"Path to the .inferconfig file";
] in
Arg.create_options_desc false "Parsing Options" desc
let usage =
"\nUsage: InferClang -c C Files -ast AST Files -results_dir <output-dir> [options] \n"
let print_usage_exit () =
Arg.usage arg_desc usage;
exit(1)
let buffer_len = 16384
(* This function reads the json file in fname, validates it, and encoded in the AST data structure*)
@ -141,9 +56,6 @@ let do_run source_path ast_path =
CFrontend_config.json := ast_filename;
CLocation.check_source_file source_path;
let source_file = CLocation.source_file_from_path source_path in
(match !Config.inferconfig_home with
| Some _ -> ()
| None -> Config.inferconfig_home := !Config.project_root);
Printf.printf "Start translation of AST from %s\n" !CFrontend_config.json;
CFrontend.do_source_file source_file ast_decl;
Printf.printf "End translation AST file %s... OK!\n" !CFrontend_config.json;
@ -155,14 +67,9 @@ let do_run source_path ast_path =
raise exc
let () =
Arg.parse "INFERCLANG_ARGS" arg_desc (fun _ -> ()) usage ;
Config.print_types := true;
if Option.is_none !CFrontend_config.source_file then
(Printing.log_err "Incorrect command line arguments\n";
print_usage_exit ())
else
match !CFrontend_config.source_file with
| Some path ->
do_run path !CFrontend_config.ast_file
| None ->
assert false
match Config.source_file with
| Some path ->
do_run path Config.ast_file
| None ->
Printing.log_err "Incorrect command line arguments\n";
Config.print_usage_exit ()

@ -20,7 +20,7 @@ type method_signature = {
loc : Clang_ast_t.source_range;
is_instance : bool;
is_cpp_virtual : bool;
language : CFrontend_config.lang;
language : Config.clang_lang;
pointer_to_parent : Clang_ast_t.pointer option;
pointer_to_property_opt : Clang_ast_t.pointer option; (* If set then method is a getter/setter *)
return_param_typ : Sil.typ option;

@ -31,7 +31,7 @@ val ms_is_instance : method_signature -> bool
val ms_is_cpp_virtual : method_signature -> bool
val ms_get_lang : method_signature -> CFrontend_config.lang
val ms_get_lang : method_signature -> Config.clang_lang
val ms_get_pointer_to_parent : method_signature -> Clang_ast_t.pointer option
@ -45,7 +45,7 @@ val ms_is_setter : method_signature -> bool
val make_ms : Procname.t -> (string * Clang_ast_t.type_ptr) list -> Clang_ast_t.type_ptr
-> Clang_ast_t.attribute list -> Clang_ast_t.source_range -> bool -> ?is_cpp_virtual:bool
-> CFrontend_config.lang -> Clang_ast_t.pointer option -> Clang_ast_t.pointer option
-> Config.clang_lang -> Clang_ast_t.pointer option -> Clang_ast_t.pointer option
-> Sil.typ option -> method_signature
val replace_name_ms : method_signature -> Procname.t -> method_signature

@ -29,7 +29,7 @@ type method_call_type =
| MCStatic
type function_method_decl_info =
| Func_decl_info of Clang_ast_t.function_decl_info * Clang_ast_t.type_ptr * CFrontend_config.lang
| Func_decl_info of Clang_ast_t.function_decl_info * Clang_ast_t.type_ptr * Config.clang_lang
| Cpp_Meth_decl_info of Clang_ast_t.function_decl_info * Clang_ast_t.cxx_method_decl_info * string * Clang_ast_t.type_ptr
| ObjC_Meth_decl_info of Clang_ast_t.obj_c_method_decl_info * string
| Block_decl_info of Clang_ast_t.block_decl_info * Clang_ast_t.type_ptr * CContext.t
@ -92,9 +92,9 @@ let get_param_decls function_method_decl_info =
let get_language function_method_decl_info =
match function_method_decl_info with
| Func_decl_info (_, _, language) -> language
| Cpp_Meth_decl_info _ -> CFrontend_config.CPP
| ObjC_Meth_decl_info _ -> CFrontend_config.OBJC
| Block_decl_info _ -> CFrontend_config.OBJC
| Cpp_Meth_decl_info _ -> Config.CPP
| ObjC_Meth_decl_info _ -> Config.OBJC
| Block_decl_info _ -> Config.OBJC
let is_cpp_virtual function_method_decl_info =
match function_method_decl_info with
@ -155,7 +155,7 @@ let method_signature_of_decl tenv meth_decl block_data_opt =
match meth_decl, block_data_opt with
| FunctionDecl (decl_info, name_info, tp, fdi), _ ->
let name = Ast_utils.get_qualified_name name_info in
let language = !CFrontend_config.language in
let language = Config.clang_lang in
let func_decl = Func_decl_info (fdi, tp, language) in
let function_info = Some (decl_info, fdi) in
let procname = General_utils.mk_procname_from_function name function_info tp language in
@ -306,9 +306,9 @@ let get_formal_parameters tenv ms =
| (name, raw_type):: pl' ->
let should_add_pointer name ms =
let is_objc_self = name = CFrontend_config.self &&
CMethod_signature.ms_get_lang ms = CFrontend_config.OBJC in
CMethod_signature.ms_get_lang ms = Config.OBJC in
let is_cxx_this = name = CFrontend_config.this &&
CMethod_signature.ms_get_lang ms = CFrontend_config.CPP in
CMethod_signature.ms_get_lang ms = Config.CPP in
(is_objc_self && CMethod_signature.ms_is_instance ms) || is_cxx_this in
let tp = if should_add_pointer name ms then
(Ast_expressions.create_pointer_type raw_type)
@ -366,7 +366,7 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method =
let method_annotation =
sil_method_annotation_of_args (CMethod_signature.ms_get_args ms) in
let is_cpp_inst_method = CMethod_signature.ms_is_instance ms
&& CMethod_signature.ms_get_lang ms = CFrontend_config.CPP in
&& CMethod_signature.ms_get_lang ms = Config.CPP in
let create_new_procdesc () =
let formals = get_formal_parameters tenv ms in
let captured_str =
@ -381,7 +381,7 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method =
let captured' = IList.map (fun (var, t) -> (Pvar.get_name var, t)) captured in
let procdesc =
let proc_attributes =
{ (ProcAttributes.default proc_name Config.C_CPP) with
{ (ProcAttributes.default proc_name Config.Clang) with
ProcAttributes.captured = captured';
ProcAttributes.objc_accessor = get_objc_property_accessor tenv ms;
formals;
@ -419,7 +419,7 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt =
| None -> Sil.Tvoid, []) in
let loc = Location.dummy in
let proc_attributes =
{ (ProcAttributes.default proc_name Config.C_CPP) with
{ (ProcAttributes.default proc_name Config.Clang) with
ProcAttributes.formals;
is_objc_instance_method = is_objc_inst_method;
loc;
@ -439,7 +439,7 @@ let create_procdesc_with_pointer context pointer class_name_opt name tp =
| Some class_name ->
General_utils.mk_procname_from_cpp_method class_name name tp
| None ->
General_utils.mk_procname_from_function name None tp !CFrontend_config.language in
General_utils.mk_procname_from_function name None tp Config.clang_lang in
create_external_procdesc context.cfg callee_name false None;
callee_name
@ -449,7 +449,7 @@ let get_method_for_frontend_checks cfg cg loc =
match Cfg.Procdesc.find_from_name cfg proc_name with
| Some pdesc -> pdesc
| None ->
let attrs = { (ProcAttributes.default proc_name Config.C_CPP) with
let attrs = { (ProcAttributes.default proc_name Config.Clang) with
is_defined = true;
loc = loc;
} in
@ -465,7 +465,7 @@ let get_method_for_frontend_checks cfg cg loc =
let add_default_method_for_class class_name decl_info =
let loc = CLocation.get_sil_location_from_range decl_info.Clang_ast_t.di_source_range true in
let proc_name = Procname.get_default_objc_class_method class_name in
let attrs = { (ProcAttributes.default proc_name Config.C_CPP) with loc = loc; } in
let attrs = { (ProcAttributes.default proc_name Config.Clang) with loc = loc; } in
AttributesTable.store_attributes attrs
let get_procname_from_cpp_lambda context dec =

@ -58,7 +58,7 @@ struct
| Procname.ObjC_Cpp objc_cpp ->
let class_name = Procname.objc_cpp_get_class_name objc_cpp in
CTrans_models.get_predefined_model_method_signature class_name selector
General_utils.mk_procname_from_objc_method CFrontend_config.OBJC
General_utils.mk_procname_from_objc_method Config.OBJC
| _ ->
None in
match predefined_ms_opt, ms_opt with
@ -458,8 +458,8 @@ struct
(* As e.g. in fun_ptr = foo; *)
let non_mangled_func_name =
if name = CFrontend_config.malloc &&
(!CFrontend_config.language = CFrontend_config.OBJC ||
!CFrontend_config.language = CFrontend_config.OBJCPP) then
(Config.clang_lang = Config.OBJC ||
Config.clang_lang = Config.OBJCPP) then
ModelBuiltins.malloc_no_fail
else Procname.from_string_c_fun name in
let is_builtin = Builtin.is_registered non_mangled_func_name in
@ -771,7 +771,7 @@ struct
if (is_binary_assign_op binary_operator_info)
(* assignment operator result is lvalue in CPP, rvalue in C, *)
(* hence the difference *)
&& (not (General_utils.is_cpp_translation !CFrontend_config.language))
&& (not (General_utils.is_cpp_translation Config.clang_lang))
&& ((not creating_node) || (is_return_temp trans_state.continuation)) then (
(* We are in this case when an assignment is inside *)
(* another operator that creates a node. Eg. another *)

@ -29,6 +29,6 @@ val is_toll_free_bridging : Procname.t option -> bool
val get_predefined_model_method_signature : string -> string ->
(string -> string -> Procname.objc_method_kind -> Procname.t) ->
CFrontend_config.lang -> CMethod_signature.method_signature option
Config.clang_lang -> CMethod_signature.method_signature option
val is_dispatch_function_name : string -> (string * int) option

@ -46,7 +46,7 @@ let get_field_annotation fn typ =
let ia' =
(* TODO (t4968422) eliminate not !Config.eradicate check by marking fields as nullified *)
(* outside of Eradicate in some other way *)
if (Models.Inference.enabled || not !Config.eradicate)
if (Models.Inference.enabled || not Config.eradicate)
&& Models.Inference.field_is_marked fn
then Annotations.mk_ia Annotations.Nullable ia
else ia in

@ -21,7 +21,7 @@ let use_models = true
module Inference = struct
let enabled = false
let get_dir () = Filename.concat !Config.results_dir "eradicate"
let get_dir () = Filename.concat Config.results_dir "eradicate"
let field_get_dir_fname fn =
let fname = Ident.fieldname_to_string fn in

@ -209,7 +209,7 @@ let create_dummy_harness_file harness_name =
let write_harness_to_file harness_instrs harness_file =
let harness_file =
let harness_file_name = DB.source_file_to_string harness_file in
ref (create_outfile harness_file_name) in
create_outfile harness_file_name in
let pp_harness fmt = IList.iter (fun instr ->
Format.fprintf fmt "%a\n" (Sil.pp_instr pe_text) instr) harness_instrs in
do_outf harness_file (fun outf ->

@ -17,7 +17,7 @@ let is_suppress_warnings_annotated =
let matcher =
lazy
(let default_matcher = fun _ -> false in
match !Config.suppress_warnings_annotations with
match Config.suppress_warnings_annotations with
| Some f ->
(try
let m = Inferconfig.SuppressWarningsMatcher.load_matcher f in

@ -16,11 +16,6 @@ module L = Logging
let models_specs_filenames = ref StringSet.empty
let javac_verbose_out = ref ""
let set_verbose_out path =
javac_verbose_out := path
let models_jar = ref ""
@ -81,7 +76,7 @@ let java_source_file_from_path path =
if Filename.is_relative path then
failwith "Expect absolute path for java source files"
else
match !Config.project_root with
match Config.project_root with
| None -> DB.abs_source_file_from_path path
| Some project_root -> DB.rel_source_file_from_abs_path project_root path
@ -161,7 +156,7 @@ let add_source_file path map =
let load_sources_and_classes () =
let file_in = open_in !javac_verbose_out in
let file_in = open_in Config.javac_verbose_out in
let class_filename_re =
Str.regexp
"\\[wrote RegularFileObject\\[\\(.*\\)\\]\\]" in

@ -25,8 +25,6 @@ val add_models : string -> unit
(** Check if there is a model for the given procname *)
val is_model : Procname.t -> bool
val set_verbose_out: string -> unit
(** create a source file from an absolute path.
Source files are relative if the project root is specified and absolute otherwise *)
val java_source_file_from_path : string -> DB.source_file

@ -118,21 +118,11 @@ let class_code cl = "L"^cl
let errors_db_file = "errors.db"
let main_errors_file = "Java_frontend.errors"
let classpath : string option ref = ref None
let class_source_map : string option ref = ref None
(** {2 Flags } *)
(* the Sawja representation of the Java Bytecode will be printed *)
let html_mode = ref false
(* debug information will be printed *)
let debug_mode = ref false
(* The classes in the given jar file will be translated. No sources needed *)
let dependency_mode = ref false
(* The dynamic dispatch will be handled partially statically *)
let static_dispatch = ref false
@ -142,9 +132,3 @@ let init_count = ref 0
let normalize_string s =
let rexp = Str.regexp_string "$" in
Str.global_replace rexp "_" s
(* Translate the safety checks doen by the JVM *)
let translate_checks = ref false
(* Generate harness for Android code *)
let create_harness = ref false

@ -78,7 +78,7 @@ let add_cmethod never_null_matcher program icfg node cm is_static =
let tenv = icfg.JContext.tenv in
let cn, ms = JBasics.cms_split cm.Javalib.cm_class_method_signature in
let is_clinit = JBasics.ms_equal ms JBasics.clinit_signature in
if !JTrans.no_static_final = false
if Config.no_static_final = false
&& is_clinit
&& not (JTransStaticField.has_static_final_fields node) then
JUtils.log "\t\tskipping class initializer: %s@." (JBasics.ms_name ms)
@ -96,7 +96,7 @@ let add_cmethod never_null_matcher program icfg node cm is_static =
| None -> assert false in
let impl = JTrans.get_implementation cm in
let instrs, meth_kind =
if is_clinit && not !JTrans.no_static_final then
if is_clinit && not Config.no_static_final then
let instrs = JTransStaticField.static_field_init node cn (JBir.code impl) in
(instrs, JContext.Init)
else (JBir.code impl), JContext.Normal in
@ -126,7 +126,7 @@ let add_amethod program icfg am is_static =
let path_of_cached_classname cn =
let root_path = Filename.concat !Config.results_dir "classnames" in
let root_path = Filename.concat Config.results_dir "classnames" in
let package_path = IList.fold_left Filename.concat root_path (JBasics.cn_package cn) in
Filename.concat package_path ((JBasics.cn_simple_name cn)^".java")

@ -14,73 +14,8 @@ open Javalib_pack
module L = Logging
let arg_desc =
let options_to_keep = ["-results_dir"; "-project_root"] in
let desc =
(arg_desc_filter options_to_keep base_arg_desc) @
[
"-classpath",
Arg.String (fun classpath -> JConfig.classpath := Some classpath),
None,
"set the classpath"
;
"-class_source_map",
Arg.String (fun filename -> JConfig.class_source_map := Some filename),
None,
"path to class -> source map in JSON format"
;
"-models",
Arg.String (fun filename -> JClasspath.add_models filename),
Some "paths",
"set the path to the jar containing the models"
;
"-debug",
Arg.Unit (fun () -> JConfig.debug_mode := true),
None,
"write extra translation information"
;
"-dependencies",
Arg.Unit (fun _ -> JConfig.dependency_mode := true),
None,
"translate all the dependencies during the capture"
;
"-no-static_final",
Arg.Unit (fun () -> JTrans.no_static_final := true),
None,
"no special treatment for static final fields"
;
"-tracing",
Arg.Unit (fun () -> JConfig.translate_checks := true),
None,
"Translate JVM checks"
;
"-harness",
Arg.Unit (fun () -> JConfig.create_harness := true),
None,
"Create Android lifecycle harness"
;
"-verbose_out",
Arg.String (fun path -> JClasspath.set_verbose_out path),
None,
"Set the path to the javac verbose output"
;
"-suppress_warnings_out",
Arg.String (fun s -> Config.suppress_warnings_annotations := Some s),
Some "Path",
"Path to list of collected @SuppressWarnings annotations"
;
] in
Arg.create_options_desc false "Parsing Options" desc
let usage =
"Usage: InferJava -d compilation_dir -sources filename\n"
let print_usage_exit () =
Arg.usage arg_desc usage;
exit(1)
let () =
Arg.parse "INFERJAVA_ARGS" arg_desc (fun _ -> ()) usage;
(match Config.models_file with Some file -> JClasspath.add_models file | None -> ());
if Config.analyze_models && !JClasspath.models_jar <> "" then
failwith "Not expecting model file when analyzing the models";
if not Config.analyze_models && !JClasspath.models_jar = "" then
@ -88,10 +23,10 @@ let () =
let register_perf_stats_report source_file =
let stats_dir = Filename.concat !Config.results_dir Config.frontend_stats_dir_name in
let stats_dir = Filename.concat Config.results_dir Config.frontend_stats_dir_name in
let abbrev_source_file = DB.source_file_encoding source_file in
let stats_file = Config.perf_stats_prefix ^ "_" ^ abbrev_source_file ^ ".json" in
DB.create_dir !Config.results_dir ;
DB.create_dir Config.results_dir ;
DB.create_dir stats_dir ;
PerfStats.register_report_at_exit (Filename.concat stats_dir stats_file)
@ -115,14 +50,12 @@ let store_icfg tenv cg cfg program =
begin
let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
if !JConfig.create_harness then Harness.create_harness cfg cg tenv;
if Config.create_harness then Harness.create_harness cfg cg tenv;
Preanal.doit ~f_translate_typ:(Some f_translate_typ) cfg cg tenv;
Cg.store_to_file cg_file cg;
Cfg.store_cfg_to_file cfg_file true cfg;
if !JConfig.debug_mode then
if Config.debug_mode then
begin
Config.write_dotty := true;
Config.print_types := true;
Dotty.print_icfg_dotty cfg [];
Cg.save_call_graph_dotty None Specs.get_specs cg
end
@ -224,7 +157,7 @@ let do_all_files classpath sources classes =
translate_source_file basename (Some package, source_file) source_file)
source_files)
sources;
if !JConfig.dependency_mode then
if Config.dependency_mode then
capture_libs never_null_matcher linereader program tenv;
save_tenv tenv;
JClasspath.cleanup program;

@ -255,8 +255,6 @@ let update_init_loc cn ms loc_start =
try ignore(JBasics.ClassMap.find cn !init_loc_map)
with Not_found -> init_loc_map := (JBasics.ClassMap.add cn loc_start !init_loc_map)
let no_static_final = ref false
(** Creates a procedure description. *)
let create_local_procdesc program linereader cfg tenv node m =
let cn, ms = JBasics.cms_split (Javalib.get_class_method_signature m) in
@ -264,7 +262,7 @@ let create_local_procdesc program linereader cfg tenv node m =
if JBasics.ms_equal ms JBasics.clinit_signature then JContext.Init
else JContext.Normal in
if not (
!no_static_final = false &&
Config.no_static_final = false &&
meth_kind = JContext.Init &&
not (JTransStaticField.has_static_final_fields node))
then
@ -394,7 +392,7 @@ let rec get_method_procdesc program cfg tenv cn ms kind =
| Created status -> status
let use_static_final_fields context =
(not !no_static_final) && (JContext.get_meth_kind context) <> JContext.Init
(not Config.no_static_final) && (JContext.get_meth_kind context) <> JContext.Init
let builtin_new =
Sil.Const (Sil.Cfun ModelBuiltins.__new)
@ -570,7 +568,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
| I_Special -> false
| _ -> true in
match sil_obj_expr with
| Sil.Var _ when is_non_constructor_call && not !JConfig.translate_checks ->
| Sil.Var _ when is_non_constructor_call && not Config.report_runtime_exceptions ->
let obj_typ_no_ptr =
match sil_obj_type with
| Sil.Tptr (typ, _) -> typ
@ -992,7 +990,8 @@ let rec instruction context pc instr : translation =
Cg.add_edge cg caller_procname callee_procname;
Instr call_node
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks && is_this expr ->
| JBir.Check (JBir.CheckNullPointer expr)
when Config.report_runtime_exceptions && is_this expr ->
(* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *)
let (instrs, sil_expr, _) = expression context pc expr in
let this_not_null_node =
@ -1000,7 +999,7 @@ let rec instruction context pc instr : translation =
(Cfg.Node.Stmt_node "this not null") (instrs @ [assume_not_null loc sil_expr]) in
Instr this_not_null_node
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks ->
| JBir.Check (JBir.CheckNullPointer expr) when Config.report_runtime_exceptions ->
let (instrs, sil_expr, _) = expression context pc expr in
let not_null_node =
let sil_not_null = Sil.BinOp (Sil.Ne, sil_expr, Sil.exp_null) in
@ -1028,8 +1027,8 @@ let rec instruction context pc instr : translation =
create_node npe_kind npe_instrs in
Prune (not_null_node, throw_npe_node)
| JBir.Check (JBir.CheckArrayBound (array_expr, index_expr)) when !JConfig.translate_checks ->
| JBir.Check (JBir.CheckArrayBound (array_expr, index_expr))
when Config.report_runtime_exceptions ->
let instrs, _, sil_length_expr, sil_index_expr =
let array_instrs, sil_array_expr, _ =
expression context pc array_expr
@ -1084,7 +1083,7 @@ let rec instruction context pc instr : translation =
Prune (in_bound_node, throw_out_of_bound_node)
| JBir.Check (JBir.CheckCast (expr, object_type)) when !JConfig.translate_checks ->
| JBir.Check (JBir.CheckCast (expr, object_type)) when Config.report_runtime_exceptions ->
let sil_type = JTransType.expr_type context expr
and instrs, sil_expr, _ = expression context pc expr
and ret_id = Ident.create_fresh Ident.knormal

@ -13,9 +13,6 @@ open! Utils
open Javalib_pack
open Sawja_pack
(** If active, disable special treatment of static final fields. *)
val no_static_final : bool ref
(** Data structure for storing the results of the translation of an instruction. *)
type translation =
| Skip

@ -12,7 +12,7 @@ open! Utils
let rec log fmt =
if !JConfig.debug_mode then
if Config.debug_mode then
Logging.stdout fmt
else
Obj.magic log

@ -1,16 +0,0 @@
(*
* Copyright (c) 2015 - 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! Utils
(** arguments for InferLLVM *)
let debug_mode = ref false
let source_filename : string option ref = ref None

@ -1,16 +0,0 @@
(*
* Copyright (c) 2015 - 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! Utils
(** arguments for InferLLVM *)
val debug_mode : bool ref
val source_filename : string option ref

@ -9,41 +9,17 @@
open! Utils
let arg_desc =
let options_to_keep = ["-results_dir"; "-project_root"] in
let desc =
arg_desc_filter options_to_keep base_arg_desc @
[
"-c",
Arg.String (fun cfile -> LConfig.source_filename := Some cfile),
Some "cfile",
"C/C++ file being translated"
;
"-debug",
Arg.Unit (fun _ -> LConfig.debug_mode := true),
None,
"Enables debug mode"
;
] in
Arg.create_options_desc false "Parsing Options" desc
let usage = "Usage: InferLLVM -c <cfile> [options]\n"
let print_usage_exit () =
Arg.usage arg_desc usage;
exit(1)
let register_perf_stats_report source_file =
let stats_dir = Filename.concat !Config.results_dir Config.frontend_stats_dir_name in
let stats_dir = Filename.concat Config.results_dir Config.frontend_stats_dir_name in
let abbrev_source_file = DB.source_file_encoding source_file in
let stats_file = Config.perf_stats_prefix ^ "_" ^ abbrev_source_file ^ ".json" in
DB.create_dir !Config.results_dir ;
DB.create_dir Config.results_dir ;
DB.create_dir stats_dir ;
PerfStats.register_report_at_exit (Filename.concat stats_dir stats_file)
let init_global_state source_filename =
Config.curr_language := Config.C_CPP;
begin match !Config.project_root with
Config.curr_language := Config.Clang;
begin match Config.project_root with
| None -> DB.current_source := DB.abs_source_file_from_path source_filename
| Some project_root ->
DB.current_source := DB.rel_source_file_from_abs_path project_root
@ -62,10 +38,8 @@ let store_icfg tenv cg cfg =
Preanal.doit cfg cg tenv;
Cg.store_to_file cg_file cg;
Cfg.store_cfg_to_file cfg_file true cfg;
if !LConfig.debug_mode then
if Config.debug_mode then
begin
Config.write_dotty := true;
Config.print_types := true;
Dotty.print_icfg_dotty cfg [];
Cg.save_call_graph_dotty None Specs.get_specs cg
end
@ -76,9 +50,8 @@ let store_tenv tenv =
Tenv.store_to_file tenv_filename tenv
let () =
Arg.parse "INFERLLVM_ARGS" arg_desc (fun _ -> ()) usage;
begin match !LConfig.source_filename with
| None -> print_usage_exit ()
begin match Config.source_file with
| None -> Config.print_usage_exit ()
| Some source_filename -> init_global_state source_filename
end;
let lexbuf = Lexing.from_channel stdin in

@ -130,7 +130,7 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
| None -> Sil.Tvoid
| Some ret_tp -> trans_typ ret_tp in
let (proc_attrs : ProcAttributes.t) =
{ (ProcAttributes.default proc_name Config.C_CPP) with
{ (ProcAttributes.default proc_name Config.Clang) with
ProcAttributes.formals =
IList.map (fun (tp, name) -> (Mangled.from_string name, trans_typ tp)) params;
is_defined = true; (** is defined and not just declared *)

@ -277,6 +277,6 @@ let () =
let to_check = ref [] in
let add_file_to_check fname =
to_check := fname :: !to_check in
Arg.parse "CHECKCOPYRIGHT_ARGS" (Arg.align speclist) add_file_to_check usage_msg;
Arg.parse (Arg.align speclist) add_file_to_check usage_msg;
IList.iter check_copyright (IList.rev !to_check);
exit 0

Loading…
Cancel
Save