pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[ocamlformat] Upgrade to ocamlformat 0.5

Browse Source 
Summary:
Upgrade ocamlformat, and base which needs to be done in sync in order to build
ocamlformat, and the other deps can come for the ride.

Reviewed By: jvillard

Differential Revision: D7663537

fbshipit-source-id: 3e90970
master
Josh Berdine 7 years ago committed by Facebook Github Bot
parent 523c2f539b
commit 16988b0a7a
223 changed files with 2019 additions and 2058 deletions
Show Stats Download Patch File Download Diff File

2
.ocamlformat
Unescape View File

@ -1,3 +1,3 @@
margin 100
sparse true
version 0.4
version 0.5

4
Makefile
Unescape View File

@ -149,13 +149,13 @@ OCAMLFORMAT_EXE?=ocamlformat
fmt:
parallel $(OCAMLFORMAT_EXE) -i ::: $$(git diff --name-only $$(git merge-base origin/master HEAD) | grep "\.mli\?$$")
JBUILD_ML:=$(shell find * -name 'jbuild*.in' | grep -v workspace)
JBUILD_ML:=$(shell find * -name 'jbuild*.in' | grep -v workspace | grep -v sledge)
.PHONY: fmt_jbuild
fmt_jbuild:
parallel $(OCAMLFORMAT_EXE) -i ::: $(JBUILD_ML)
SRC_ML:=$(shell find * \( -name _build -or -name facebook-clang-plugins -or -path facebook/dependencies \) -not -prune -or -type f -and -name '*'.ml -or -name '*'.mli 2>/dev/null)
SRC_ML:=$(shell find * \( -name _build -or -name facebook-clang-plugins -or -path facebook/dependencies -or -path sledge/llvm \) -not -prune -or -type f -and -name '*'.ml -or -name '*'.mli 2>/dev/null)
.PHONY: fmt_all
fmt_all:

4
infer/src/IR/AccessExpression.ml
Unescape View File

@ -16,7 +16,7 @@ type t =
| ArrayOffset of t * Typ.t * t list
| AddressOf of t
| Dereference of t
[@@deriving compare]
[@@deriving compare]
(** convert to an AccessPath.t, ignoring AddressOf and Dereference for now *)
let rec to_access_path t =
@ -108,7 +108,7 @@ let rec normalize t =
match t with
| Base _ ->
t
| Dereference AddressOf t1 ->
| Dereference (AddressOf t1) ->
normalize t1
| FieldOffset (t1, fieldname) ->
let t1' = normalize t1 in

2
infer/src/IR/AccessExpression.mli
Unescape View File

@ -19,7 +19,7 @@ type t =
(* address of operator & *)
| Dereference of t
(* dereference operator * *)
[@@deriving compare]
[@@deriving compare]
val to_access_path : t -> AccessPath.t

4
infer/src/IR/AccessPath.ml
Unescape View File

@ -274,7 +274,7 @@ let inner_class_normalize p =
| Some
( ( (Var.ProgramVar pvar as root)
, ({desc= Tptr (({desc= Tstruct name} as cls), pkind)} as ptr) )
, (FieldAccess first) :: accesses )
, FieldAccess first :: accesses )
when Pvar.is_this pvar && Fieldname.Java.is_outer_instance first ->
Name.Java.get_outer_class name
|> Option.map ~f:(fun outer_name ->
@ -285,7 +285,7 @@ let inner_class_normalize p =
(* happens in ctrs only *)
| Some
( (Var.ProgramVar pvar, ({desc= Tptr (({desc= Tstruct name} as cls), pkind)} as ptr))
, (FieldAccess first) :: accesses )
, FieldAccess first :: accesses )
when is_synthetic_this pvar && Fieldname.Java.is_outer_instance first ->
Name.Java.get_outer_class name
|> Option.bind ~f:(fun outer_name ->

4
infer/src/IR/AccessPath.mli
Unescape View File

@ -16,7 +16,7 @@ type base = Var.t * Typ.t [@@deriving compare]
type access =
| ArrayAccess of Typ.t * t list (** array element type with list of access paths in index *)
| FieldAccess of Typ.Fieldname.t (** field name *)
[@@deriving compare]
[@@deriving compare]
(** root var, and a list of accesses. closest to the root var is first that is, x.f.g is
representedas (x, [f; g]) *)
@ -92,7 +92,7 @@ module Abs : sig
type t =
| Abstracted of raw (** abstraction of heap reachable from an access path, e.g. x.f* *)
| Exact of raw (** precise representation of an access path, e.g. x.f.g *)
[@@deriving compare]
[@@deriving compare]
val equal : t -> t -> bool

2
infer/src/IR/Annot.ml
Unescape View File

@ -19,7 +19,7 @@ type parameters = string list [@@deriving compare]
type t =
{ class_name: string (** name of the annotation *)
; parameters: parameters (** currently only one string parameter *) }
[@@deriving compare]
[@@deriving compare]
let volatile = {class_name= "volatile"; parameters= []}

2
infer/src/IR/Annot.mli
Unescape View File

@ -18,7 +18,7 @@ type parameters = string list
type t =
{ class_name: string (** name of the annotation *)
; parameters: parameters (** currently only one string parameter *) }
[@@deriving compare]
[@@deriving compare]
val volatile : t
(** annotation for fields marked with the "volatile" keyword *)

2
infer/src/IR/Binop.ml
Unescape View File

@ -36,7 +36,7 @@ type t =
| BOr (** inclusive-or *)
| LAnd (** logical and. Does not always evaluate both operands. *)
| LOr (** logical or. Does not always evaluate both operands. *)
[@@deriving compare]
[@@deriving compare]
let equal = [%compare.equal : t]

2
infer/src/IR/Binop.mli
Unescape View File

@ -36,7 +36,7 @@ type t =
| BOr (** inclusive-or *)
| LAnd (** logical and. Does not always evaluate both operands. *)
| LOr (** logical or. Does not always evaluate both operands. *)
[@@deriving compare]
[@@deriving compare]
val equal : t -> t -> bool

2
infer/src/IR/CallFlags.ml
Unescape View File

@ -22,7 +22,7 @@ type t =
; cf_is_objc_block: bool
; cf_targets: Typ.Procname.t list
; cf_with_block_parameters: bool }
[@@deriving compare]
[@@deriving compare]
let pp f cf =
if cf.cf_virtual then F.fprintf f " virtual" ;

2
infer/src/IR/CallFlags.mli
Unescape View File

@ -22,7 +22,7 @@ type t =
; cf_is_objc_block: bool
; cf_targets: Typ.Procname.t list
; cf_with_block_parameters: bool }
[@@deriving compare]
[@@deriving compare]
val pp : F.formatter -> t -> unit

12
infer/src/IR/Cfg.ml
Unescape View File

@ -49,7 +49,7 @@ let iter_all_nodes ?(sorted= false) f cfg =
~f:(fun desc_nodes node -> (pdesc, node) :: desc_nodes)
~init:desc_nodes (Procdesc.get_nodes pdesc) )
cfg []
|> List.sort ~cmp:[%compare : Procdesc.t * Procdesc.Node.t]
|> List.sort ~compare:[%compare : Procdesc.t * Procdesc.Node.t]
|> List.iter ~f:(fun (d, n) -> f d n)
@ -135,12 +135,12 @@ let inline_synthetic_method ret_id etl pdesc loc_call : Sil.instr option =
(* setter for static fields *)
let instr' = Sil.Store (Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, e1, loc_call) in
found instr instr'
| Sil.Call (ret_id', Exp.Const Const.Cfun pn, etl', _, cf), _, _
| Sil.Call (ret_id', Exp.Const (Const.Cfun pn), etl', _, cf), _, _
when Bool.equal (is_none ret_id) (is_none ret_id')
&& Int.equal (List.length etl') (List.length etl) ->
let instr' = Sil.Call (ret_id, Exp.Const (Const.Cfun pn), etl, loc_call, cf) in
found instr instr'
| Sil.Call (ret_id', Exp.Const Const.Cfun pn, etl', _, cf), _, _
| Sil.Call (ret_id', Exp.Const (Const.Cfun pn), etl', _, cf), _, _
when Bool.equal (is_none ret_id) (is_none ret_id')
&& Int.equal (List.length etl' + 1) (List.length etl) ->
let etl1 =
@ -163,7 +163,7 @@ let inline_synthetic_method ret_id etl pdesc loc_call : Sil.instr option =
(** Find synthetic (access or bridge) Java methods in the procedure and inline them in the cfg. *)
let proc_inline_synthetic_methods cfg pdesc : unit =
let instr_inline_synthetic_method = function
| Sil.Call (ret_id, Exp.Const Const.Cfun (Typ.Procname.Java java_pn as pn), etl, loc, _) -> (
| Sil.Call (ret_id, Exp.Const (Const.Cfun (Typ.Procname.Java java_pn as pn)), etl, loc, _) -> (
match Typ.Procname.Hash.find cfg pn with
| pd ->
let is_access = Typ.Procname.Java.is_access_method java_pn in
@ -172,7 +172,7 @@ let proc_inline_synthetic_methods cfg pdesc : unit =
let is_bridge = attributes.is_bridge_method in
if is_access || is_bridge || is_synthetic then inline_synthetic_method ret_id etl pd loc
else None
| exception Not_found ->
| exception Caml.Not_found ->
None )
| _ ->
None
@ -201,5 +201,5 @@ let inline_java_synthetic_methods cfg =
let pp_proc_signatures fmt cfg =
F.fprintf fmt "METHOD SIGNATURES@\n@." ;
let sorted_procs = List.sort ~cmp:Procdesc.compare (get_all_proc_descs cfg) in
let sorted_procs = List.sort ~compare:Procdesc.compare (get_all_proc_descs cfg) in
List.iter ~f:(fun pdesc -> F.fprintf fmt "%a@." Procdesc.pp_signature pdesc) sorted_procs

2
infer/src/IR/Const.ml
Unescape View File

@ -20,7 +20,7 @@ type t =
| Cstr of string (** string constants *)
| Cfloat of float (** float constants *)
| Cclass of Ident.name (** class constant *)
[@@deriving compare]
[@@deriving compare]
let equal = [%compare.equal : t]

2
infer/src/IR/Const.mli
Unescape View File

@ -21,7 +21,7 @@ type t =
| Cstr of string (** string constants *)
| Cfloat of float (** float constants *)
| Cclass of Ident.name (** class constant *)
[@@deriving compare]
[@@deriving compare]
val equal : t -> t -> bool

6
infer/src/IR/DecompiledExp.ml
Unescape View File

@ -50,7 +50,7 @@ let rec to_string = function
to_string de1 ^ "[" ^ to_string de2 ^ "]"
| Dbinop (op, de1, de2) ->
"(" ^ to_string de1 ^ Binop.str Pp.text op ^ to_string de2 ^ ")"
| Dconst Cfun pn
| Dconst (Cfun pn)
-> (
let procname_str = Typ.Procname.to_simplified_string pn in
match builtin_functions_to_string pn with
@ -78,7 +78,7 @@ let rec to_string = function
else Pp.comma_seq pp_arg fmt des
in
let pp_fun fmt = function
| Dconst Cfun pname ->
| Dconst (Cfun pname) ->
let s =
match pname with
| Typ.Procname.Java pname_java ->
@ -92,7 +92,7 @@ let rec to_string = function
in
let receiver, args' =
match args with
| (Dpvar pv) :: args' when isvirtual && Pvar.is_this pv ->
| Dpvar pv :: args' when isvirtual && Pvar.is_this pv ->
(None, args')
| a :: args' when isvirtual ->
(Some a, args')

10
infer/src/IR/Errlog.ml
Unescape View File

@ -59,9 +59,7 @@ let compute_local_exception_line loc_trace =
| _ ->
Continue (last_known_step_at_level_zero_opt', line_opt)
in
match List.fold_until ~init:(None, None) ~f:compute_local_exception_line loc_trace with
| Finished (_, line_opt) | Stopped_early line_opt ->
line_opt
List.fold_until ~init:(None, None) ~f:compute_local_exception_line ~finish:snd loc_trace
type node_id_key = {node_id: int; node_key: Caml.Digest.t}
@ -72,7 +70,7 @@ type err_key =
; err_name: IssueType.t
; err_desc: Localise.error_desc
; severity: string }
[@@deriving compare]
[@@deriving compare]
(** Data associated to a specific error *)
type err_data =
@ -223,7 +221,7 @@ let add_issue tbl err_key (err_datas: ErrDataSet.t) : bool =
else (
ErrLogHash.replace tbl err_key (ErrDataSet.union err_datas current_eds) ;
true )
with Not_found ->
with Caml.Not_found ->
ErrLogHash.add tbl err_key err_datas ;
true
@ -258,7 +256,7 @@ let log_issue procname ?clang_method_kind err_kind err_log loc (node_id, node_ke
in
let should_report =
Exceptions.equal_visibility error.visibility Exceptions.Exn_user
|| Config.developer_mode && exn_developer
|| (Config.developer_mode && exn_developer)
in
( if exn_developer then
let issue =

2
infer/src/IR/Errlog.mli
Unescape View File

@ -44,7 +44,7 @@ type err_key = private
; err_name: IssueType.t
; err_desc: Localise.error_desc
; severity: string }
[@@deriving compare]
[@@deriving compare]
(** Data associated to a specific error *)
type err_data = private

11
infer/src/IR/Exceptions.ml
Unescape View File

@ -17,7 +17,7 @@ type visibility =
| Exn_user (** always add to error log *)
| Exn_developer (** only add to error log in developer mode *)
| Exn_system (** never add to error log *)
[@@deriving compare]
[@@deriving compare]
let equal_visibility = [%compare.equal : visibility]
@ -69,8 +69,8 @@ exception Custom_error of string * Localise.error_desc
exception Dummy_exception of Localise.error_desc
exception Dangling_pointer_dereference of
PredSymb.dangling_kind option * Localise.error_desc * L.ocaml_pos
exception
Dangling_pointer_dereference of PredSymb.dangling_kind option * Localise.error_desc * L.ocaml_pos
exception Deallocate_stack_variable of Localise.error_desc
@ -98,8 +98,9 @@ exception Internal_error of Localise.error_desc
exception Java_runtime_exception of Typ.Name.t * string * Localise.error_desc
exception Leak of
bool * Sil.hpred * (visibility * Localise.error_desc) * bool * PredSymb.resource * L.ocaml_pos
exception
Leak of
bool * Sil.hpred * (visibility * Localise.error_desc) * bool * PredSymb.resource * L.ocaml_pos
exception Missing_fld of Typ.Fieldname.t * L.ocaml_pos

22
infer/src/IR/Exceptions.mli
Unescape View File

@ -17,7 +17,7 @@ type visibility =
| Exn_user (** always add to error log *)
| Exn_developer (** only add to error log in developer mode *)
| Exn_system (** never add to error log *)
[@@deriving compare]
[@@deriving compare]
val equal_visibility : visibility -> visibility -> bool
@ -67,8 +67,9 @@ exception Custom_error of string * Localise.error_desc
exception Dummy_exception of Localise.error_desc
exception Dangling_pointer_dereference of
PredSymb.dangling_kind option * Localise.error_desc * Logging.ocaml_pos
exception
Dangling_pointer_dereference of
PredSymb.dangling_kind option * Localise.error_desc * Logging.ocaml_pos
exception Deallocate_stack_variable of Localise.error_desc
@ -96,13 +97,14 @@ exception Internal_error of Localise.error_desc
exception Java_runtime_exception of Typ.Name.t * string * Localise.error_desc
exception Leak of
bool
* Sil.hpred
* (visibility * Localise.error_desc)
* bool
* PredSymb.resource
* Logging.ocaml_pos
exception
Leak of
bool
* Sil.hpred
* (visibility * Localise.error_desc)
* bool
* PredSymb.resource
* Logging.ocaml_pos
exception Missing_fld of Typ.Fieldname.t * Logging.ocaml_pos

6
infer/src/IR/Exp.ml
Unescape View File

@ -48,7 +48,7 @@ and t =
(** A field offset, the type is the surrounding struct type *)
| Lindex of t * t (** An array index offset: [exp1\[exp2\]] *)
| Sizeof of sizeof_data
[@@deriving compare]
[@@deriving compare]
let equal = [%compare.equal : t]
@ -74,11 +74,11 @@ module Hash = Hashtbl.Make (struct
let hash = hash
end)
let is_null_literal = function Const Cint n -> IntLit.isnull n | _ -> false
let is_null_literal = function Const (Cint n) -> IntLit.isnull n | _ -> false
let is_this = function Lvar pvar -> Pvar.is_this pvar | _ -> false
let is_zero = function Const Cint n -> IntLit.iszero n | _ -> false
let is_zero = function Const (Cint n) -> IntLit.iszero n | _ -> false
(** {2 Utility Functions for Expressions} *)

2
infer/src/IR/Exp.mli
Unescape View File

@ -42,7 +42,7 @@ and t =
(** A field offset, the type is the surrounding struct type *)
| Lindex of t * t (** An array index offset: [exp1\[exp2\]] *)
| Sizeof of sizeof_data
[@@deriving compare]
[@@deriving compare]
val equal : t -> t -> bool
(** Equality for expressions. *)

20
infer/src/IR/HilExp.ml
Unescape View File

@ -20,7 +20,7 @@ type t =
| Constant of Const.t
| Cast of Typ.t * t
| Sizeof of Typ.t * t option
[@@deriving compare]
[@@deriving compare]
let rec pp fmt = function
| AccessExpression access_expr ->
@ -34,7 +34,7 @@ let rec pp fmt = function
| Closure (pname, captured) ->
let pp_item fmt (base, exp) =
match exp with
| AccessExpression Base b when AccessPath.equal_base b base ->
| AccessExpression (Base b) when AccessPath.equal_base b base ->
F.fprintf fmt "%a captured" AccessPath.pp_base b
| _ ->
F.fprintf fmt "%a captured as %a" AccessPath.pp_base base pp exp
@ -70,19 +70,19 @@ let rec get_typ tenv = function
None )
| Exception t ->
get_typ tenv t
| Closure _ | Constant Cfun _ ->
| Closure _ | Constant (Cfun _) ->
(* We don't have a way to represent function types *)
None
| Constant Cint _ ->
| Constant (Cint _) ->
(* TODO: handle signedness *)
Some (Typ.mk (Typ.Tint Typ.IInt))
| Constant Cfloat _ ->
| Constant (Cfloat _) ->
Some (Typ.mk (Typ.Tfloat Typ.FFloat))
| Constant Cclass _ ->
| Constant (Cclass _) ->
(* TODO: this only happens in Java. We probably need to change it to `Cclass of Typ.Name.t`
to give a useful result here *)
None
| Constant Cstr _ ->
| Constant (Cstr _) ->
(* TODO: this will need to behave differently depending on whether we're in C++ or Java *)
None
| Cast (typ, _) ->
@ -171,7 +171,7 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ =
( Var (Ident.create_normal (Ident.string_to_name (Exp.to_string root_exp)) 0)
, fld
, root_exp_typ )) typ )
| Lindex (Const Cstr s, index_exp) ->
| Lindex (Const (Cstr s), index_exp) ->
(* indexed string literal (e.g., "foo"[1]). represent this by introducing a dummy variable
for the string literal. if you actually need to see the value of the string literal in the
analysis, you should probably be using SIL. this is unsound if the code modifies the
@ -201,11 +201,11 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ =
of_sil_ exp typ
let is_null_literal = function Constant Cint n -> IntLit.isnull n | _ -> false
let is_null_literal = function Constant (Cint n) -> IntLit.isnull n | _ -> false
let rec eval_arithmetic_binop op e1 e2 =
match (eval e1, eval e2) with
| Some Const.Cint i1, Some Const.Cint i2 ->
| Some (Const.Cint i1), Some (Const.Cint i2) ->
Some (Const.Cint (op i1 i2))
| _ ->
None

2
infer/src/IR/HilExp.mli
Unescape View File

@ -22,7 +22,7 @@ type t =
| Sizeof of Typ.t * t option
(** C-style sizeof(), and also used to treate a type as an expression. Refer to [Exp] module for
canonical documentation *)
[@@deriving compare]
[@@deriving compare]
val pp : F.formatter -> t -> unit

8
infer/src/IR/HilInstr.ml
Unescape View File

@ -24,7 +24,7 @@ type t =
| Assign of AccessExpression.t * HilExp.t * Location.t
| Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t
| Call of AccessPath.base option * call * HilExp.t list * CallFlags.t * Location.t
[@@deriving compare]
[@@deriving compare]
let pp fmt = function
| Assign (access_expr, exp, loc) ->
@ -67,7 +67,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ loc
| Call
( Some (ret_id, _)
, Const Cfun callee_pname
, Const (Cfun callee_pname)
, (target_exp, _) :: (Sizeof {typ= cast_typ}, _) :: _
, loc
, _ )
@ -96,7 +96,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
L.(die InternalError)
"Invalid pointer arithmetic expression %a used as LHS at %a" Exp.pp lhs_exp
Location.pp_file_pos loc )
| Constant Const.Cint i ->
| Constant (Const.Cint i) ->
(* this can happen in intentionally crashing code like *0xdeadbeef = 0 used for
debugging. doesn't really matter what we do here, so just create a dummy var *)
let dummy_base_var =
@ -112,7 +112,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
let hil_ret = Option.map ~f:(fun (ret_id, ret_typ) -> (Var.of_id ret_id, ret_typ)) ret_opt in
let hil_call =
match exp_of_sil call_exp (Typ.mk Tvoid) with
| Constant Cfun procname | Closure (procname, _) ->
| Constant (Cfun procname) | Closure (procname, _) ->
Direct procname
| AccessExpression access_expr ->
Indirect access_expr

2
infer/src/IR/HilInstr.mli
Unescape View File

@ -20,7 +20,7 @@ type t =
(** Assumed expression, true_branch boolean, source of the assume (conditional, ternary, etc.) *)
| Call of AccessPath.base option * call * HilExp.t list * CallFlags.t * Location.t
(** Var to hold the return if it exists, call expression, formals *)
[@@deriving compare]
[@@deriving compare]
val pp : F.formatter -> t -> unit

6
infer/src/IR/Ident.ml
Unescape View File

@ -54,7 +54,7 @@ type kind =
| KFootprint
| KNormal
| KPrimed
[@@deriving compare]
[@@deriving compare]
let kfootprint = KFootprint
@ -142,7 +142,7 @@ module NameGenerator = struct
let stamp = NameHash.find !name_map name in
NameHash.replace !name_map name (stamp + 1) ;
stamp + 1
with Not_found ->
with Caml.Not_found ->
NameHash.add !name_map name 0 ;
0
in
@ -155,7 +155,7 @@ module NameGenerator = struct
let curr_stamp = NameHash.find !name_map name in
let new_stamp = max curr_stamp stamp in
NameHash.replace !name_map name new_stamp
with Not_found -> NameHash.add !name_map name stamp
with Caml.Not_found -> NameHash.add !name_map name stamp
end
(** Name used for the return variable *)

10
infer/src/IR/Io_infer.ml
Unescape View File

@ -101,10 +101,7 @@ td.rowname { text-align:right; font-weight:bold; color:#444444; padding-right:2e
let open_out source path =
let full_fname = get_full_fname source path in
let fd =
Unix.openfile
(DB.filename_to_string full_fname)
~mode:Unix.([O_WRONLY; O_APPEND])
~perm:0o777
Unix.openfile (DB.filename_to_string full_fname) ~mode:Unix.[O_WRONLY; O_APPEND] ~perm:0o777
in
let outc = Unix.out_channel_of_descr fd in
let fmt = F.formatter_of_out_channel outc in
@ -156,8 +153,9 @@ td.rowname { text-align:right; font-weight:bold; color:#444444; padding-right:2e
in
F.asprintf
"<span class='%s'>%s_%d<span class='expansion'>node%d preds:%a succs:%a exn:%a \
%s%s</span></span>" style_class descr id id (Pp.seq F.pp_print_int) preds
(Pp.seq F.pp_print_int) succs (Pp.seq F.pp_print_int) exn description
%s%s</span></span>"
style_class descr id id (Pp.seq F.pp_print_int) preds (Pp.seq F.pp_print_int) succs
(Pp.seq F.pp_print_int) exn description
(if not isvisited then "\nNOT VISITED" else "")
in
pp_link ~path:(path_to_root @ ["nodes"; node_fname]) fmt node_text

28
infer/src/IR/LintIssues.ml
Unescape View File

@ -16,7 +16,7 @@ let errLogMap = ref Typ.Procname.Map.empty
let exists_issues () = not (Typ.Procname.Map.is_empty !errLogMap)
let get_err_log procname =
try Typ.Procname.Map.find procname !errLogMap with Not_found ->
try Typ.Procname.Map.find procname !errLogMap with Caml.Not_found ->
let errlog = Errlog.empty () in
errLogMap := Typ.Procname.Map.add procname errlog !errLogMap ;
errlog
@ -42,19 +42,19 @@ let load_issues_to_errlog_map dir =
let file = DB.filename_from_string (Filename.concat issues_dir issues_file) in
match load_issues file with
| Some map ->
errLogMap
:= Typ.Procname.Map.merge
(fun _ issues1 issues2 ->
match (issues1, issues2) with
| Some issues1, Some issues2 ->
Errlog.update issues1 issues2 ; Some issues1
| Some issues1, None ->
Some issues1
| None, Some issues2 ->
Some issues2
| None, None ->
None )
!errLogMap map
errLogMap :=
Typ.Procname.Map.merge
(fun _ issues1 issues2 ->
match (issues1, issues2) with
| Some issues1, Some issues2 ->
Errlog.update issues1 issues2 ; Some issues1
| Some issues1, None ->
Some issues1
| None, Some issues2 ->
Some issues2
| None, None ->
None )
!errLogMap map
| None ->
()
in

33
infer/src/IR/Localise.ml
Unescape View File

@ -59,9 +59,8 @@ module Tags = struct
let get tags tag = List.Assoc.find ~equal:String.equal tags tag
end
type error_desc =
{descriptions: string list; tags: Tags.t; dotty: string option}
[@@deriving compare]
type error_desc = {descriptions: string list; tags: Tags.t; dotty: string option}
[@@deriving compare]
(** empty error description *)
let no_desc : error_desc = {descriptions= []; tags= []; dotty= None}
@ -115,7 +114,7 @@ let error_desc_set_bucket err_desc bucket =
let error_desc_is_reportable_bucket err_desc =
let issue_bucket = error_desc_get_bucket err_desc in
let high_buckets = BucketLevel.([b1; b2]) in
let high_buckets = BucketLevel.[b1; b2] in
Option.value_map issue_bucket ~default:false ~f:(fun b ->
List.mem ~equal:String.equal high_buckets b )
@ -126,7 +125,9 @@ let get_value_line_tag tags =
let value = snd (List.find_exn ~f:(fun (tag, _) -> String.equal tag Tags.value) tags) in
let line = snd (List.find_exn ~f:(fun (tag, _) -> String.equal tag Tags.line) tags) in
Some [value; line]
with Not_found -> None
with
| Not_found_s _ | Caml.Not_found ->
None
(** extract from desc a value on which to apply polymorphic hash and equality *)
@ -260,7 +261,8 @@ let deref_str_nil_argument_in_variadic_method pn total_args arg_number =
let problem_str =
Printf.sprintf
"could be %s which results in a call to %s with %d arguments instead of %d (%s indicates \
that the last argument of this variadic %s has been reached)" nil_null
that the last argument of this variadic %s has been reached)"
nil_null
(Typ.Procname.to_simplified_string pn)
arg_number (total_args - 1) nil_null function_method
in
@ -390,8 +392,9 @@ let desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc =
"The field %a is annotated with %a, but the lock %a is not held during the access to the \
field %s. Since the current method is non-private, it can be called from outside the \
current class without synchronization. Consider wrapping the access in a %s block or \
making the method private." MF.pp_monospaced accessed_fld_str MF.pp_monospaced annot_str
MF.pp_monospaced guarded_by_str line_info syncronized_str
making the method private."
MF.pp_monospaced accessed_fld_str MF.pp_monospaced annot_str MF.pp_monospaced guarded_by_str
line_info syncronized_str
in
{no_desc with descriptions= [msg]}
@ -440,13 +443,13 @@ let access_desc access_opt =
match access_opt with
| None ->
[]
| Some Last_accessed (n, _) ->
| Some (Last_accessed (n, _)) ->
let line_str = string_of_int n in
["last accessed on line " ^ line_str]
| Some Last_assigned (n, _) ->
| Some (Last_assigned (n, _)) ->
let line_str = string_of_int n in
["last assigned on line " ^ line_str]
| Some Returned_from_call _ ->
| Some (Returned_from_call _) ->
[]
| Some Initialized_automatically ->
["initialized automatically"]
@ -455,7 +458,7 @@ let access_desc access_opt =
let dereference_string proc_name deref_str value_str access_opt loc =
let tags = deref_str.tags in
Tags.update tags Tags.value value_str ;
let is_call_access = match access_opt with Some Returned_from_call _ -> true | _ -> false in
let is_call_access = match access_opt with Some (Returned_from_call _) -> true | _ -> false in
let value_desc =
String.concat ~sep:""
[ (match deref_str.value_pre with Some s -> s ^ " " | _ -> "")
@ -662,14 +665,14 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
in
let typ_str =
match hpred_type_opt with
| Some Exp.Sizeof {typ= {desc= Tstruct name}} when Typ.Name.is_class name ->
| Some (Exp.Sizeof {typ= {desc= Tstruct name}}) when Typ.Name.is_class name ->
" of type " ^ MF.monospaced_to_string (Typ.Name.name name) ^ " "
| _ ->
" "
in
let desc_str =
match resource_opt with
| Some PredSymb.Rmemory _ ->
| Some (PredSymb.Rmemory _) ->
mem_dyn_allocated ^ to_ ^ value_str
| Some PredSymb.Rfile ->
"resource" ^ typ_str ^ "acquired" ^ to_ ^ value_str
@ -686,7 +689,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
let is_not_rxxx_after =
let rxxx =
match resource_opt with
| Some PredSymb.Rmemory _ ->
| Some (PredSymb.Rmemory _) ->
reachable
| Some PredSymb.Rfile | Some PredSymb.Rlock ->
released

5
infer/src/IR/Localise.mli
Unescape View File

@ -17,9 +17,8 @@ module Tags : sig
end
(** description field of error messages *)
type error_desc =
{descriptions: string list; tags: Tags.t; dotty: string option}
[@@deriving compare]
type error_desc = {descriptions: string list; tags: Tags.t; dotty: string option}
[@@deriving compare]
val no_desc : error_desc
(** empty error description *)

15
infer/src/IR/PredSymb.ml
Unescape View File

@ -14,9 +14,8 @@ open! IStd
module L = Logging
module F = Format
type func_attribute =
| FA_sentinel of int * int (** __attribute__((sentinel(int, int))) *)
[@@deriving compare]
type func_attribute = FA_sentinel of int * int (** __attribute__((sentinel(int, int))) *)
[@@deriving compare]
let pp_func_attribute fmt = function FA_sentinel (i, j) -> F.fprintf fmt "sentinel(%d,%d)" i j
@ -39,7 +38,7 @@ let string_of_access = function
(** Return the value of the FA_sentinel attribute in [attr_list] if it is found *)
let get_sentinel_func_attribute_value attr_list =
match attr_list with
| (FA_sentinel (sentinel, null_pos)) :: _ ->
| FA_sentinel (sentinel, null_pos) :: _ ->
Some (sentinel, null_pos)
| [] ->
None
@ -50,7 +49,7 @@ type mem_kind =
| Mnew (** memory allocated with new *)
| Mnew_array (** memory allocated with new[] *)
| Mobjc (** memory allocated with objective-c alloc *)
[@@deriving compare]
[@@deriving compare]
(** resource that can be allocated *)
type resource = Rmemory of mem_kind | Rfile | Rignore | Rlock [@@deriving compare]
@ -67,7 +66,7 @@ type dangling_kind =
(** pointer is dangling because it is the address
of a stack variable which went out of scope *)
| DAminusone (** pointer is -1 *)
[@@deriving compare]
[@@deriving compare]
(** position in a path: proc name, node id *)
type path_pos = Typ.Procname.t * int [@@deriving compare]
@ -124,7 +123,7 @@ type t =
| Aunsubscribed_observer
(** denotes an object unsubscribed from observers of a notification center *)
| Awont_leak (** value do not participate in memory leak analysis *)
[@@deriving compare]
[@@deriving compare]
let equal = [%compare.equal : t]
@ -163,7 +162,7 @@ type category =
| ACretval
| ACobserver
| ACwontleak
[@@deriving compare]
[@@deriving compare]
let equal_category = [%compare.equal : category]

6
infer/src/IR/PredSymb.mli
Unescape View File

@ -35,7 +35,7 @@ type mem_kind =
| Mnew (** memory allocated with new *)
| Mnew_array (** memory allocated with new[] *)
| Mobjc (** memory allocated with objective-c alloc *)
[@@deriving compare]
[@@deriving compare]
(** resource that can be allocated *)
type resource = Rmemory of mem_kind | Rfile | Rignore | Rlock [@@deriving compare]
@ -89,7 +89,7 @@ type t =
| Aunsubscribed_observer
(** denotes an object unsubscribed from observers of a notification center *)
| Awont_leak (** value do not participate in memory leak analysis *)
[@@deriving compare]
[@@deriving compare]
val equal : t -> t -> bool
@ -110,7 +110,7 @@ type category =
| ACretval
| ACobserver
| ACwontleak
[@@deriving compare]
[@@deriving compare]
val equal_category : category -> category -> bool

10
infer/src/IR/ProcAttributes.ml
Unescape View File

@ -31,7 +31,7 @@ type clang_method_kind =
| OBJC_CLASS
| BLOCK
| C_FUNCTION
[@@deriving compare]
[@@deriving compare]
let equal_clang_method_kind = [%compare.equal : clang_method_kind]
@ -51,10 +51,8 @@ let string_of_clang_method_kind = function
(** Type for ObjC accessors *)
type objc_accessor_type =
| Objc_getter of Typ.Struct.field
| Objc_setter of Typ.Struct.field
[@@deriving compare]
type objc_accessor_type = Objc_getter of Typ.Struct.field | Objc_setter of Typ.Struct.field
[@@deriving compare]
let kind_of_objc_accessor_type accessor =
match accessor with Objc_getter _ -> "getter" | Objc_setter _ -> "setter"
@ -114,7 +112,7 @@ type t =
; proc_name: Typ.Procname.t (** name of the procedure *)
; ret_type: Typ.t (** return type *)
; source_file_captured: SourceFile.t (** source file where the procedure was captured *) }
[@@deriving compare]
[@@deriving compare]
let default proc_name =
{ access= PredSymb.Default

12
infer/src/IR/ProcAttributes.mli
Unescape View File

@ -21,23 +21,21 @@ type clang_method_kind =
| OBJC_CLASS
| BLOCK
| C_FUNCTION
[@@deriving compare]
[@@deriving compare]
val equal_clang_method_kind : clang_method_kind -> clang_method_kind -> bool
val string_of_clang_method_kind : clang_method_kind -> string
type objc_accessor_type =
| Objc_getter of Typ.Struct.field
| Objc_setter of Typ.Struct.field
[@@deriving compare]
type objc_accessor_type = Objc_getter of Typ.Struct.field | Objc_setter of Typ.Struct.field
[@@deriving compare]
val kind_of_objc_accessor_type : objc_accessor_type -> string
type var_attribute =
| Modify_in_block
(* __block attribute of Objective-C variables, means that it will be modified inside a block *)
[@@deriving compare]
[@@deriving compare]
val var_attribute_equal : var_attribute -> var_attribute -> bool
(** Equality for var_attribute *)
@ -72,7 +70,7 @@ type t =
; proc_name: Typ.Procname.t (** name of the procedure *)
; ret_type: Typ.t (** return type *)
; source_file_captured: SourceFile.t (** source file where the procedure was captured *) }
[@@deriving compare]
[@@deriving compare]
val default : Typ.Procname.t -> t
(** Create a proc_attributes with default values. *)

28
infer/src/IR/Procdesc.ml
Unescape View File

@ -26,7 +26,7 @@ module Node = struct
| Join_node
| Prune_node of bool * Sil.if_kind * string (** (true/false branch, if_kind, comment) *)
| Skip_node of string
[@@deriving compare]
[@@deriving compare]
let equal_nodekind = [%compare.equal : nodekind]
@ -221,7 +221,7 @@ type t =
; mutable start_node: Node.t (** start node of this procedure *)
; mutable exit_node: Node.t (** exit node of this procedure *)
; mutable loop_heads: NodeSet.t option (** loop head nodes of this procedure *) }
[@@deriving compare]
[@@deriving compare]
let from_proc_attributes attributes =
let pname_opt = Some attributes.ProcAttributes.proc_name in
@ -428,9 +428,9 @@ let pp_variable_list fmt etl =
let pp_objc_accessor fmt accessor =
match accessor with
| Some ProcAttributes.Objc_getter field ->
| Some (ProcAttributes.Objc_getter field) ->
Format.fprintf fmt "Getter of %a, " (Typ.Struct.pp_field Pp.text) field
| Some ProcAttributes.Objc_setter field ->
| Some (ProcAttributes.Objc_setter field) ->
Format.fprintf fmt "Setter of %a, " (Typ.Struct.pp_field Pp.text) field
| None ->
()
@ -520,7 +520,7 @@ let convert_cfg ~callee_pdesc ~resolved_pdesc ~f_instr_list =
[]
| node :: other_node ->
let converted_node =
try NodeMap.find node !node_map with Not_found ->
try NodeMap.find node !node_map with Caml.Not_found ->
let new_node = convert_node node
and successors = Node.get_succs node
and exn_nodes = Node.get_exn node in
@ -553,7 +553,7 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions =
in
let subst_map = ref Ident.Map.empty in
let redirect_typename origin_id =
try Some (Ident.Map.find origin_id !subst_map) with Not_found -> None
try Some (Ident.Map.find origin_id !subst_map) with Caml.Not_found -> None
in
let convert_instr instrs = function
| Sil.Load
@ -562,7 +562,7 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions =
, {Typ.desc= Tptr ({desc= Tstruct origin_typename}, Pk_pointer)}
, loc ) ->
let specialized_typname =
try Mangled.Map.find (Pvar.get_name origin_pvar) substitutions with Not_found ->
try Mangled.Map.find (Pvar.get_name origin_pvar) substitutions with Caml.Not_found ->
origin_typename
in
subst_map := Ident.Map.add id specialized_typname !subst_map ;
@ -570,7 +570,7 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions =
| Sil.Load (id, (Exp.Var origin_id as origin_exp), ({Typ.desc= Tstruct _} as origin_typ), loc) ->
let updated_typ : Typ.t =
try Typ.mk ~default:origin_typ (Tstruct (Ident.Map.find origin_id !subst_map))
with Not_found -> origin_typ
with Caml.Not_found -> origin_typ
in
Sil.Load (id, convert_exp origin_exp, updated_typ, loc) :: instrs
| Sil.Load (id, origin_exp, origin_typ, loc) ->
@ -582,7 +582,7 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions =
set_instr :: instrs
| Sil.Call
( return_ids
, Exp.Const Const.Cfun Typ.Procname.Java callee_pname_java
, Exp.Const (Const.Cfun (Typ.Procname.Java callee_pname_java))
, (Exp.Var id, _) :: origin_args
, loc
, call_flags )
@ -715,7 +715,8 @@ let specialize_with_block_args_instrs resolved_pdesc substitutions =
in
let instrs = remove_temps_instrs :: call_instr :: load_instrs @ instrs in
(instrs, id_map)
with Not_found -> convert_generic_call return_ids (Exp.Var id) origin_args loc call_flags )
with Caml.Not_found ->
convert_generic_call return_ids (Exp.Var id) origin_args loc call_flags )
| Sil.Call (return_ids, origin_call_exp, origin_args, loc, call_flags) ->
convert_generic_call return_ids origin_call_exp origin_args loc call_flags
| Sil.Prune (origin_exp, loc, is_true_branch, if_kind) ->
@ -775,8 +776,8 @@ let specialize_with_block_args callee_pdesc pname_with_block_args block_args =
let _, captured = Mangled.Map.find param_name substitutions in
append_no_duplicates_formals_and_annot acc
(List.map captured ~f:(fun captured_var -> (captured_var, Annot.Item.empty)))
with Not_found -> append_no_duplicates_formals_and_annot acc [((param_name, typ), annot)]
)
with Caml.Not_found ->
append_no_duplicates_formals_and_annot acc [((param_name, typ), annot)] )
in
List.unzip new_formals_blocks_captured_vars_with_annots
in
@ -788,7 +789,8 @@ let specialize_with_block_args callee_pdesc pname_with_block_args block_args =
| None ->
Logging.die InternalError
"specialize_with_block_args ahould only be called with defined procedures, but we \
cannot find the captured file of procname %a" Typ.Procname.pp pname
cannot find the captured file of procname %a"
Typ.Procname.pp pname
in
let resolved_attributes =
{ callee_attributes with

2
infer/src/IR/Procdesc.mli
Unescape View File

@ -28,7 +28,7 @@ module Node : sig
| Join_node
| Prune_node of bool * Sil.if_kind * string (** (true/false branch, if_kind, comment) *)
| Skip_node of string
[@@deriving compare]
[@@deriving compare]
val equal_nodekind : nodekind -> nodekind -> bool

20
infer/src/IR/ProcnameDispatcher.ml
Unescape View File

@ -11,11 +11,13 @@ open! IStd
(** To be used in 'list_constraint *)
type accept_more
and end_of_list
and end_of_list
(** To be used in 'emptyness *)
type empty
and non_empty
and non_empty
(* Type shorthands *)
@ -344,11 +346,7 @@ module Common = struct
let any_typ
: ('f, 'f, 'captured_types, 'captured_types, 'markers, 'markers, accept_more) template_arg =
let eat_template_arg (f, captured_types, template_args) =
match template_args with
| (Typ.TType _) :: rest ->
Some (f, captured_types, rest)
| _ ->
None
match template_args with Typ.TType _ :: rest -> Some (f, captured_types, rest) | _ -> None
in
{eat_template_arg; add_marker= add_no_marker}
@ -367,7 +365,7 @@ module Common = struct
fun marker ->
let eat_template_arg (f, captured_types, template_args) =
match template_args with
| (Typ.TType ty) :: rest ->
| Typ.TType ty :: rest ->
let captured_types () = (ty, captured_types ()) in
Some (f ty, captured_types, rest)
| _ ->
@ -388,11 +386,7 @@ module Common = struct
, accept_more )
template_arg =
let eat_template_arg (f, captured_types, template_args) =
match template_args with
| (Typ.TInt i) :: rest ->
Some (f i, captured_types, rest)
| _ ->
None
match template_args with Typ.TInt i :: rest -> Some (f i, captured_types, rest) | _ -> None
in
{eat_template_arg; add_marker= add_no_marker}

4
infer/src/IR/Pvar.ml
Unescape View File

@ -28,7 +28,7 @@ type pvar_kind =
(** global variable: translation unit + is it compile constant? + is it POD? + is it a static
local? + is it a static global *)
| Seed_var (** variable used to store the initial value of formal parameters *)
[@@deriving compare]
[@@deriving compare]
(** Names for program variables. *)
type t = {pv_hash: int; pv_name: Mangled.t; pv_kind: pvar_kind} [@@deriving compare]
@ -153,7 +153,7 @@ let is_frontend_tmp pvar =
(* Check whether the program variable is a temporary one generated by Sawja, javac, or some other
bytecode/name generation pass. valid java identifiers cannot contain `$` *)
let is_bytecode_tmp name =
String.contains name '$' && not (String.contains name '_')
(String.contains name '$' && not (String.contains name '_'))
|| String.is_prefix ~prefix:"CatchVar" name
in
(* Check whether the program variable is generated by [mk_tmp] *)

46
infer/src/IR/Sil.ml
Unescape View File

@ -26,7 +26,7 @@ type if_kind =
| Ik_land_lor (** obtained from translation of && or || *)
| Ik_while
| Ik_switch
[@@deriving compare]
[@@deriving compare]
(** An instruction. *)
type instr =
@ -53,7 +53,7 @@ type instr =
| Abstract of Location.t (** apply abstraction *)
| Remove_temps of Ident.t list * Location.t (** remove temporaries *)
| Declare_locals of (Pvar.t * Typ.t) list * Location.t (** declare local variables *)
[@@deriving compare]
[@@deriving compare]
let equal_instr = [%compare.equal : instr]
@ -78,7 +78,7 @@ type atom =
| Aneq of Exp.t * Exp.t (** disequality *)
| Apred of PredSymb.t * Exp.t list (** predicate symbol applied to exps *)
| Anpred of PredSymb.t * Exp.t list (** negated predicate symbol applied to exps *)
[@@deriving compare]
[@@deriving compare]
let equal_atom = [%compare.equal : atom]
@ -94,7 +94,7 @@ let atom_has_local_addr a =
type lseg_kind =
| Lseg_NE (** nonempty (possibly circular) listseg *)
| Lseg_PE (** possibly empty (possibly circular) listseg *)
[@@deriving compare]
[@@deriving compare]
let equal_lseg_kind = [%compare.equal : lseg_kind]
@ -118,7 +118,7 @@ type inst =
| Itaint
| Iupdate of zero_flag * null_case_flag * int * PredSymb.path_pos
| Ireturn_from_call of int
[@@deriving compare]
[@@deriving compare]
let equal_inst = [%compare.equal : inst]
@ -134,7 +134,7 @@ type 'inst strexp0 =
For instance, x |->[10 | e1: v1] implies that e1 <= 9.
Second, if two indices appear in an array, they should be different.
For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. *)
[@@deriving compare]
[@@deriving compare]
type strexp = inst strexp0
@ -162,11 +162,11 @@ type 'inst hpred0 =
primed identifiers, and include all the free primed identifiers in body.
body should not contain any non - primed identifiers or program
variables (i.e. pvars). *)
[@@deriving compare]
[@@deriving compare]
and 'inst hpara0 =
{root: Ident.t; next: Ident.t; svars: Ident.t list; evars: Ident.t list; body: 'inst hpred0 list}
[@@deriving compare]
[@@deriving compare]
(** parameter for the higher-order doubly-linked list predicates.
Assume that all the free identifiers in body_dll should belong to
@ -178,7 +178,7 @@ and 'inst hpara_dll0 =
; svars_dll: Ident.t list
; evars_dll: Ident.t list
; body_dll: 'inst hpred0 list }
[@@deriving compare]
[@@deriving compare]
type hpred = inst hpred0
@ -434,10 +434,11 @@ let pp_instr pe0 f instr =
let add_with_block_parameters_flag instr =
match instr with
| Call (ret_id, Exp.Const Const.Cfun pname, arg_ts, loc, cf) ->
if List.exists ~f:(fun (exp, _) -> Exp.is_objc_block_closure exp) arg_ts
&& Typ.Procname.is_clang pname
(* to be extended to other methods *)
| Call (ret_id, Exp.Const (Const.Cfun pname), arg_ts, loc, cf) ->
if
List.exists ~f:(fun (exp, _) -> Exp.is_objc_block_closure exp) arg_ts
&& Typ.Procname.is_clang pname
(* to be extended to other methods *)
then
let cf' = {cf with cf_with_block_parameters= true} in
Call (ret_id, Exp.Const (Const.Cfun pname), arg_ts, loc, cf')
@ -459,7 +460,7 @@ let pp_instr_list pe fmt instrs =
let pp_atom pe0 f a =
let pe, changed = color_pre_wrapper pe0 f a in
( match a with
| Aeq (BinOp (op, e1, e2), Const Cint i) when IntLit.isone i ->
| Aeq (BinOp (op, e1, e2), Const (Cint i)) when IntLit.isone i ->
F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp (op, e1, e2))
| Aeq (e1, e2) ->
F.fprintf f "%a = %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2
@ -1085,8 +1086,9 @@ let hpred_free_vars h = Sequence.Generator.run (hpred_gen_free_vars h)
the prop. The function faults in the re - execution mode, as an internal check of the tool. *)
let array_clean_new_index footprint_part new_idx =
assert (not (footprint_part && not !Config.footprint)) ;
if footprint_part
&& Exp.free_vars new_idx |> Sequence.exists ~f:(fun id -> not (Ident.is_footprint id))
if
footprint_part
&& Exp.free_vars new_idx |> Sequence.exists ~f:(fun id -> not (Ident.is_footprint id))
then (
L.d_warning
( "Array index " ^ Exp.to_string new_idx
@ -1248,7 +1250,7 @@ let mem_sub id sub = List.exists ~f:(fun (id1, _) -> Ident.equal id id1) sub
(** Extend substitution and return [None] if not possible. *)
let extend_sub sub id exp : exp_subst option =
let compare (id1, _) (id2, _) = Ident.compare id1 id2 in
if mem_sub id sub then None else Some (List.merge ~cmp:compare sub [(id, exp)])
if mem_sub id sub then None else Some (List.merge ~compare sub [(id, exp)])
(** Free auxilary variables in the domain and range of the substitution. *)
@ -1506,7 +1508,9 @@ type sharing_env = {exph: Exp.t Exp.Hash.t; hpredh: hpred HpredInstHash.t}
let create_sharing_env () = {exph= Exp.Hash.create 3; hpredh= HpredInstHash.create 3}
(** Return a canonical representation of the exp *)
let exp_compact sh e = try Exp.Hash.find sh.exph e with Not_found -> Exp.Hash.add sh.exph e e ; e
let exp_compact sh e =
try Exp.Hash.find sh.exph e with Caml.Not_found -> Exp.Hash.add sh.exph e e ; e
let rec sexp_compact sh se =
match se with
@ -1533,7 +1537,7 @@ let hpred_compact_ sh hpred =
let hpred_compact sh hpred =
try HpredInstHash.find sh.hpredh hpred with Not_found ->
try HpredInstHash.find sh.hpredh hpred with Caml.Not_found ->
let hpred' = hpred_compact_ sh hpred in
HpredInstHash.add sh.hpredh hpred' hpred' ;
hpred'
@ -1570,9 +1574,9 @@ let exp_add_offsets exp offsets =
let rec f acc = function
| [] ->
acc
| (Off_fld (fld, typ)) :: offs' ->
| Off_fld (fld, typ) :: offs' ->
f (Exp.Lfield (acc, fld, typ)) offs'
| (Off_index e) :: offs' ->
| Off_index e :: offs' ->
f (Exp.Lindex (acc, e)) offs'
in
f exp offsets

18
infer/src/IR/Sil.mli
Unescape View File

@ -26,7 +26,7 @@ type if_kind =
| Ik_land_lor (** obtained from translation of && or || *)
| Ik_while
| Ik_switch
[@@deriving compare]
[@@deriving compare]
(** An instruction. *)
type instr =
@ -53,7 +53,7 @@ type instr =
| Abstract of Location.t (** apply abstraction *)
| Remove_temps of Ident.t list * Location.t (** remove temporaries *)
| Declare_locals of (Pvar.t * Typ.t) list * Location.t (** declare local variables *)
[@@deriving compare]
[@@deriving compare]
val equal_instr : instr -> instr -> bool
@ -73,7 +73,7 @@ type atom =
| Aneq of Exp.t * Exp.t (** disequality *)
| Apred of PredSymb.t * Exp.t list (** predicate symbol applied to exps *)
| Anpred of PredSymb.t * Exp.t list (** negated predicate symbol applied to exps *)
[@@deriving compare]
[@@deriving compare]
val equal_atom : atom -> atom -> bool
@ -83,7 +83,7 @@ val atom_has_local_addr : atom -> bool
type lseg_kind =
| Lseg_NE (** nonempty (possibly circular) listseg *)
| Lseg_PE (** possibly empty (possibly circular) listseg *)
[@@deriving compare]
[@@deriving compare]
val equal_lseg_kind : lseg_kind -> lseg_kind -> bool
@ -107,7 +107,7 @@ type inst =
| Itaint
| Iupdate of zero_flag * null_case_flag * int * PredSymb.path_pos
| Ireturn_from_call of int
[@@deriving compare]
[@@deriving compare]
val equal_inst : inst -> inst -> bool
@ -159,7 +159,7 @@ type 'inst strexp0 =
For instance, x |->[10 | e1: v1] implies that e1 <= 9.
Second, if two indices appear in an array, they should be different.
For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. *)
[@@deriving compare]
[@@deriving compare]
type strexp = inst strexp0
@ -191,11 +191,11 @@ type 'inst hpred0 =
primed identifiers, and include all the free primed identifiers in body.
body should not contain any non - primed identifiers or program
variables (i.e. pvars). *)
[@@deriving compare]
[@@deriving compare]
and 'inst hpara0 =
{root: Ident.t; next: Ident.t; svars: Ident.t list; evars: Ident.t list; body: 'inst hpred0 list}
[@@deriving compare]
[@@deriving compare]
(** parameter for the higher-order doubly-linked list predicates.
Assume that all the free identifiers in body_dll should belong to
@ -207,7 +207,7 @@ and 'inst hpara_dll0 =
; svars_dll: Ident.t list
; evars_dll: Ident.t list
; body_dll: 'inst hpred0 list }
[@@deriving compare]
[@@deriving compare]
type hpred = inst hpred0

14
infer/src/IR/Subtype.ml
Unescape View File

@ -19,10 +19,8 @@ let list_to_string list =
else "- {" ^ String.concat ~sep:", " (List.map ~f:Typ.Name.name list) ^ "}"
type t' =
| Exact (** denotes the current type only *)
| Subtypes of Typ.Name.t list
[@@deriving compare]
type t' = Exact (** denotes the current type only *) | Subtypes of Typ.Name.t list
[@@deriving compare]
let equal_modulo_flag (st1, _) (st2, _) = [%compare.equal : t'] st1 st2
@ -99,7 +97,7 @@ end)
let check_subtype =
let subtMap = ref SubtypesMap.empty in
fun tenv c1 c2 ->
( try SubtypesMap.find (c1, c2) !subtMap with Not_found ->
( try SubtypesMap.find (c1, c2) !subtMap with Caml.Not_found ->
let is_subt = check_subclass_tenv tenv c1 c2 in
subtMap := SubtypesMap.add (c1, c2) is_subt !subtMap ;
is_subt
@ -182,7 +180,7 @@ let normalize_subtypes t_opt c1 c2 flag1 flag2 =
| Exact ->
Some (t, new_flag)
| Subtypes l ->
Some (Subtypes (List.sort ~cmp:Typ.Name.compare l), new_flag) )
Some (Subtypes (List.sort ~compare:Typ.Name.compare l), new_flag) )
| None ->
None
@ -253,8 +251,8 @@ let get_subtypes tenv (c1, ((st1, flag1): t)) (c2, ((st2, flag2): t)) =
let l2' = updates_head tenv c1 l2 in
(Some (Subtypes (add_not_subtype tenv c1 l1 l2')), None)
else (None, Some st1)
else if (is_interface tenv c1 || is_known_subtype tenv c2 c1)
&& no_subtype_in_list tenv c2 l1
else if
(is_interface tenv c1 || is_known_subtype tenv c2 c1) && no_subtype_in_list tenv c2 l1
then
let l1' = updates_head tenv c2 l1 in
( Some (Subtypes (add_not_subtype tenv c2 l1' l2))

10
infer/src/IR/Tenv.ml
Unescape View File

@ -45,13 +45,13 @@ let mk_struct tenv ?default ?fields ?statics ?methods ?supers ?annots name =
(** Look up a name in the global type environment. *)
let lookup tenv name : Typ.Struct.t option =
try Some (TypenameHash.find tenv name) with Not_found ->
try Some (TypenameHash.find tenv name) with Caml.Not_found ->
(* ToDo: remove the following additional lookups once C/C++ interop is resolved *)
match (name : Typ.Name.t) with
| CStruct m -> (
try Some (TypenameHash.find tenv (CppClass (m, NoTemplate))) with Not_found -> None )
try Some (TypenameHash.find tenv (CppClass (m, NoTemplate))) with Caml.Not_found -> None )
| CppClass (m, NoTemplate) -> (
try Some (TypenameHash.find tenv (CStruct m)) with Not_found -> None )
try Some (TypenameHash.find tenv (CStruct m)) with Caml.Not_found -> None )
| _ ->
None
@ -65,7 +65,7 @@ let add_field tenv class_tn_name field =
match lookup tenv class_tn_name with
| Some ({fields} as struct_typ) ->
if not (List.mem ~equal:equal_fields fields field) then
let new_fields = List.merge [field] fields ~cmp:compare_fields in
let new_fields = List.merge [field] fields ~compare:compare_fields in
ignore (mk_struct tenv ~default:struct_typ ~fields:new_fields ~statics:[] class_tn_name)
| _ ->
()
@ -154,7 +154,7 @@ let language_is tenv lang =
match TypenameHash.iter (fun n -> raise (Found n)) tenv with
| () ->
false
| exception Found JavaClass _ ->
| exception Found (JavaClass _) ->
Language.equal lang Java
| exception Found _ ->
Language.equal lang Clang

48
infer/src/IR/Typ.ml
Unescape View File

@ -31,7 +31,7 @@ type ikind =
| IULongLong (** [unsigned long long] (or [unsigned int64_] on Microsoft Visual C) *)
| I128 (** [__int128_t] *)
| IU128 (** [__uint128_t] *)
[@@deriving compare]
[@@deriving compare]
let ikind_to_string = function
| IChar ->
@ -78,7 +78,7 @@ type fkind =
| FFloat (** [float] *)
| FDouble (** [double] *)
| FLongDouble (** [long double] *)
[@@deriving compare]
[@@deriving compare]
let fkind_to_string = function
| FFloat ->
@ -96,7 +96,7 @@ type ptr_kind =
| Pk_objc_weak (** Obj-C __weak pointer *)
| Pk_objc_unsafe_unretained (** Obj-C __unsafe_unretained pointer *)
| Pk_objc_autoreleasing (** Obj-C __autoreleasing pointer *)
[@@deriving compare]
[@@deriving compare]
let equal_ptr_kind = [%compare.equal : ptr_kind]
@ -129,7 +129,7 @@ module T = struct
| TVar of string (** type variable (ie. C++ template variables) *)
| Tarray of {elt: t; length: IntLit.t option; stride: IntLit.t option}
(** array type with statically fixed length and stride *)
[@@deriving compare]
[@@deriving compare]
and name =
| CStruct of QualifiedCppName.t
@ -138,20 +138,15 @@ module T = struct
| JavaClass of Mangled.t
| ObjcClass of QualifiedCppName.t
| ObjcProtocol of QualifiedCppName.t
[@@deriving compare]
[@@deriving compare]
and template_arg =
| TType of t
| TInt of Int64.t
| TNull
| TNullPtr
| TOpaque
[@@deriving compare]
and template_arg = TType of t | TInt of Int64.t | TNull | TNullPtr | TOpaque
[@@deriving compare]
and template_spec_info =
| NoTemplate
| Template of {mangled: string option; args: template_arg list}
[@@deriving compare]
[@@deriving compare]
let equal_desc = [%compare.equal : desc]
@ -555,12 +550,11 @@ module Procname = struct
(* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface *)
| Static
(* in Java, procedures called with invokestatic *)
[@@deriving compare]
[@@deriving compare]
(* TODO: use Mangled.t here *)
type java_type = Name.Java.Split.t =
{package: string option; type_name: string}
[@@deriving compare]
type java_type = Name.Java.Split.t = {package: string option; type_name: string}
[@@deriving compare]
(** Type of java procedure names. *)
type t =
@ -569,7 +563,7 @@ module Procname = struct
; class_name: Name.t
; return_type: java_type option (* option because constructors have no return type *)
; kind: kind }
[@@deriving compare]
[@@deriving compare]
let make class_name return_type method_name parameters kind =
{class_name; return_type; method_name; parameters; kind}
@ -743,7 +737,7 @@ module Procname = struct
| ObjCClassMethod
| ObjCInstanceMethod
| ObjCInternalMethod
[@@deriving compare]
[@@deriving compare]
type t =
{ method_name: string
@ -751,7 +745,7 @@ module Procname = struct
; kind: kind
; template_args: template_spec_info
; is_generic_model: bool }
[@@deriving compare]
[@@deriving compare]
let make class_name method_name kind template_args ~is_generic_model =
{class_name; method_name; kind; template_args; is_generic_model}
@ -831,7 +825,7 @@ module Procname = struct
; mangled: string option
; template_args: template_spec_info
; is_generic_model: bool }
[@@deriving compare]
[@@deriving compare]
(** Type of Objective C block names. *)
type block_name = string [@@deriving compare]
@ -844,7 +838,7 @@ module Procname = struct
| Block of block_name
| ObjC_Cpp of ObjC_Cpp.t
| WithBlockParameters of t * block_name list
[@@deriving compare]
[@@deriving compare]
let equal = [%compare.equal : t]
@ -1152,7 +1146,6 @@ module Procname = struct
let sexp_of_t p = Sexp.Atom (to_string p)
end )
()
let serialize pname =
@ -1174,10 +1167,8 @@ module Procname = struct
end
module Fieldname = struct
type t =
| Clang of {class_name: Name.t; field_name: string}
| Java of string
[@@deriving compare]
type t = Clang of {class_name: Name.t; field_name: string} | Java of string
[@@deriving compare]
let equal = [%compare.equal : t]
@ -1306,7 +1297,8 @@ module Struct = struct
\tmethods: {%a@\n\
\t}@\n\
\tannots: {%a@\n\
\t}" Name.pp name
\t}"
Name.pp name
(Pp.seq (pp_field pe))
fields
(Pp.seq (fun f n -> F.fprintf f "@\n\t\t%a" Name.pp n))

18
infer/src/IR/Typ.mli
Unescape View File

@ -29,7 +29,7 @@ type ikind =
| IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft Visual C) *)
| I128 (** [__int128_t] *)
| IU128 (** [__uint128_t] *)
[@@deriving compare]
[@@deriving compare]
val ikind_is_char : ikind -> bool
(** Check whether the integer kind is a char *)
@ -42,7 +42,7 @@ type fkind =
| FFloat (** [float] *)
| FDouble (** [double] *)
| FLongDouble (** [long double] *)
[@@deriving compare]
[@@deriving compare]
(** kind of pointer *)
type ptr_kind =
@ -51,7 +51,7 @@ type ptr_kind =
| Pk_objc_weak (** Obj-C __weak pointer *)
| Pk_objc_unsafe_unretained (** Obj-C __unsafe_unretained pointer *)
| Pk_objc_autoreleasing (** Obj-C __autoreleasing pointer *)
[@@deriving compare]
[@@deriving compare]
val equal_ptr_kind : ptr_kind -> ptr_kind -> bool
@ -80,7 +80,7 @@ and desc =
| TVar of string (** type variable (ie. C++ template variables) *)
| Tarray of {elt: t; length: IntLit.t option; stride: IntLit.t option}
(** array type with statically fixed length and stride *)
[@@deriving compare]
[@@deriving compare]
and name =
| CStruct of QualifiedCppName.t
@ -92,7 +92,7 @@ and name =
| JavaClass of Mangled.t
| ObjcClass of QualifiedCppName.t
| ObjcProtocol of QualifiedCppName.t
[@@deriving compare]
[@@deriving compare]
and template_arg = TType of t | TInt of Int64.t | TNull | TNullPtr | TOpaque [@@deriving compare]
@ -104,7 +104,7 @@ and template_spec_info =
mangling is not guaranteed to be unique to a single type. All the information in
the template arguments is also needed for uniqueness. *)
; args: template_arg list }
[@@deriving compare]
[@@deriving compare]
val mk : ?default:t -> ?quals:type_quals -> desc -> t
(** Create Typ.t from given desc. if [default] is passed then use its value to set other fields such as quals *)
@ -376,7 +376,7 @@ module Procname : sig
| ObjCClassMethod
| ObjCInstanceMethod
| ObjCInternalMethod
[@@deriving compare]
[@@deriving compare]
(** Type of Objective C and C++ procedure names: method signatures. *)
type t =
@ -385,7 +385,7 @@ module Procname : sig
; kind: kind
; template_args: template_spec_info
; is_generic_model: bool }
[@@deriving compare]
[@@deriving compare]
val make : Name.t -> string -> kind -> template_spec_info -> is_generic_model:bool -> t
(** Create an objc procedure name from a class_name and method_name. *)
@ -444,7 +444,7 @@ module Procname : sig
| Block of block_name
| ObjC_Cpp of ObjC_Cpp.t
| WithBlockParameters of t * block_name list
[@@deriving compare]
[@@deriving compare]
val block_name_of_procname : t -> block_name

2
infer/src/IR/Unop.ml
Unescape View File

@ -19,7 +19,7 @@ type t =
| Neg (** Unary minus *)
| BNot (** Bitwise complement (~) *)
| LNot (** Logical Not (!) *)
[@@deriving compare]
[@@deriving compare]
let equal = [%compare.equal : t]

2
infer/src/IR/Unop.mli
Unescape View File

@ -19,7 +19,7 @@ type t =
| Neg (** Unary minus *)
| BNot (** Bitwise complement (~) *)
| LNot (** Logical Not (!) *)
[@@deriving compare]
[@@deriving compare]
val equal : t -> t -> bool

4
infer/src/absint/AbstractDomain.ml
Unescape View File

@ -191,7 +191,7 @@ module MapOfPPMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
else
M.for_all
(fun k lhs_v ->
try ValueDomain.( <= ) ~lhs:lhs_v ~rhs:(M.find k rhs) with Not_found -> false )
try ValueDomain.( <= ) ~lhs:lhs_v ~rhs:(M.find k rhs) with Caml.Not_found -> false )
lhs
@ -241,7 +241,7 @@ module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S
if phys_equal lhs rhs then true
else
try M.for_all (fun k rhs_v -> ValueDomain.( <= ) ~lhs:(M.find k lhs) ~rhs:rhs_v) rhs
with Not_found -> false
with Caml.Not_found -> false
let join astate1 astate2 =

8
infer/src/absint/AbstractInterpreter.ml
Unescape View File

@ -49,9 +49,7 @@ struct
type invariant_map = Domain.astate state InvariantMap.t
(** extract the state of node [n] from [inv_map] *)
let extract_state node_id inv_map =
try Some (InvariantMap.find node_id inv_map) with Not_found -> None
let extract_state node_id inv_map = InvariantMap.find_opt node_id inv_map
(** extract the postcondition of node [n] from [inv_map] *)
let extract_post node_id inv_map =
@ -106,8 +104,8 @@ struct
if visit_count' > Config.max_widens then
L.(die InternalError)
"Exceeded max widening threshold %d while analyzing %a. Please check your widening \
operator or increase the threshold" Config.max_widens Typ.Procname.pp
(Procdesc.get_proc_name pdesc) ;
operator or increase the threshold"
Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ;
update_inv_map widened_pre visit_count' )
else
(* first time visiting this node *)

2
infer/src/absint/FormalMap.ml
Unescape View File

@ -32,7 +32,7 @@ let empty = AccessPath.BaseMap.empty
let is_formal = AccessPath.BaseMap.mem
let get_formal_index base t = try Some (AccessPath.BaseMap.find base t) with Not_found -> None
let get_formal_index base t = AccessPath.BaseMap.find_opt base t
let get_formal_base index t =
List.find ~f:(fun (_, i) -> Int.equal i index) (AccessPath.BaseMap.bindings t)

4
infer/src/absint/LowerHil.ml
Unescape View File

@ -48,9 +48,7 @@ struct
let exec_instr ((actual_state, id_map) as astate) extras node instr =
let f_resolve_id id =
try Some (IdAccessPathMapDomain.find id id_map) with Not_found -> None
in
let f_resolve_id id = IdAccessPathMapDomain.find_opt id id_map in
match
HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr
with

18
infer/src/absint/PatternMatch.ml
Unescape View File

@ -121,8 +121,8 @@ let get_vararg_type_names tenv (call_node: Procdesc.Node.t) (ivar: Pvar.t) : str
(* Is this the node creating ivar? *)
let rec initializes_array instrs =
match instrs with
| (Sil.Call (Some (t1, _), Exp.Const Const.Cfun pn, _, _, _))
:: (Sil.Store (Exp.Lvar iv, _, Exp.Var t2, _)) :: is ->
| Sil.Call (Some (t1, _), Exp.Const (Const.Cfun pn), _, _, _)
:: Sil.Store (Exp.Lvar iv, _, Exp.Var t2, _) :: is ->
Pvar.equal ivar iv && Ident.equal t1 t2
&& Typ.Procname.equal pn (Typ.Procname.from_string_c_fun "__new_array")
|| initializes_array is
@ -135,9 +135,9 @@ let get_vararg_type_names tenv (call_node: Procdesc.Node.t) (ivar: Pvar.t) : str
let added_type_name node =
let rec nvar_type_name nvar instrs =
match instrs with
| (Sil.Load (nv, Exp.Lfield (_, id, t), _, _)) :: _ when Ident.equal nv nvar ->
| Sil.Load (nv, Exp.Lfield (_, id, t), _, _) :: _ when Ident.equal nv nvar ->
get_field_type_name tenv t id
| (Sil.Load (nv, _, t, _)) :: _ when Ident.equal nv nvar ->
| Sil.Load (nv, _, t, _) :: _ when Ident.equal nv nvar ->
Some (get_type_name t)
| _ :: is ->
nvar_type_name nvar is
@ -146,10 +146,10 @@ let get_vararg_type_names tenv (call_node: Procdesc.Node.t) (ivar: Pvar.t) : str
in
let rec added_nvar array_nvar instrs =
match instrs with
| (Sil.Store (Exp.Lindex (Exp.Var iv, _), _, Exp.Var nvar, _)) :: _
| Sil.Store (Exp.Lindex (Exp.Var iv, _), _, Exp.Var nvar, _) :: _
when Ident.equal iv array_nvar ->
nvar_type_name nvar (Procdesc.Node.get_instrs node)
| (Sil.Store (Exp.Lindex (Exp.Var iv, _), _, Exp.Const c, _)) :: _
| Sil.Store (Exp.Lindex (Exp.Var iv, _), _, Exp.Const c, _) :: _
when Ident.equal iv array_nvar ->
Some (java_get_const_type_name c)
| _ :: is ->
@ -159,7 +159,7 @@ let get_vararg_type_names tenv (call_node: Procdesc.Node.t) (ivar: Pvar.t) : str
in
let rec array_nvar instrs =
match instrs with
| (Sil.Load (nv, Exp.Lvar iv, _, _)) :: _ when Pvar.equal iv ivar ->
| Sil.Load (nv, Exp.Lvar iv, _, _) :: _ when Pvar.equal iv ivar ->
added_nvar nv instrs
| _ :: is ->
array_nvar is
@ -176,7 +176,7 @@ let get_vararg_type_names tenv (call_node: Procdesc.Node.t) (ivar: Pvar.t) : str
| [n] -> (
match added_type_name node with Some name -> name :: type_names n | None -> type_names n )
| _ ->
raise Not_found
raise Caml.Not_found
in
List.rev (type_names call_node)
@ -263,7 +263,7 @@ let proc_calls resolve_attributes pdesc filter : (Typ.Procname.t * ProcAttribute
let res = ref [] in
let do_instruction _ instr =
match instr with
| Sil.Call (_, Exp.Const Const.Cfun callee_pn, _, _, _) -> (
| Sil.Call (_, Exp.Const (Const.Cfun callee_pn), _, _, _) -> (
match resolve_attributes callee_pn with
| Some callee_attributes ->
if filter callee_pn callee_attributes then res := (callee_pn, callee_attributes) :: !res

8
infer/src/absint/ProcCfg.ml
Unescape View File

@ -215,7 +215,7 @@ module Exceptional = struct
let add_exn_pred exn_preds_acc exn_succ_node =
let exn_succ_node_id = Procdesc.Node.get_id exn_succ_node in
let existing_exn_preds =
try Procdesc.IdMap.find exn_succ_node_id exn_preds_acc with Not_found -> []
try Procdesc.IdMap.find exn_succ_node_id exn_preds_acc with Caml.Not_found -> []
in
if not (List.mem ~equal:Procdesc.Node.equal existing_exn_preds n) then
(* don't add duplicates *)
@ -241,7 +241,7 @@ module Exceptional = struct
let normal_preds _ n = Procdesc.Node.get_preds n
let exceptional_preds (_, exn_pred_map) n =
try Procdesc.IdMap.find (Procdesc.Node.get_id n) exn_pred_map with Not_found -> []
try Procdesc.IdMap.find (Procdesc.Node.get_id n) exn_pred_map with Caml.Not_found -> []
(** get all normal and exceptional successors of [n]. *)
@ -251,7 +251,7 @@ module Exceptional = struct
| [] ->
normal_succs
| exceptional_succs ->
normal_succs @ exceptional_succs |> List.sort ~cmp:Procdesc.Node.compare
normal_succs @ exceptional_succs |> List.sort ~compare:Procdesc.Node.compare
|> List.remove_consecutive_duplicates ~equal:Procdesc.Node.equal
@ -262,7 +262,7 @@ module Exceptional = struct
| [] ->
normal_preds
| exceptional_preds ->
normal_preds @ exceptional_preds |> List.sort ~cmp:Procdesc.Node.compare
normal_preds @ exceptional_preds |> List.sort ~compare:Procdesc.Node.compare
|> List.remove_consecutive_duplicates ~equal:Procdesc.Node.equal

4
infer/src/absint/Scheduler.ml
Unescape View File

@ -77,7 +77,7 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
let schedule_succ worklist_acc node_to_schedule =
let id_to_schedule = CFG.id node_to_schedule in
let old_work =
try M.find id_to_schedule worklist_acc with Not_found ->
try M.find id_to_schedule worklist_acc with Caml.Not_found ->
WorkUnit.make t.cfg node_to_schedule
in
let new_work = WorkUnit.add_visited_pred t.cfg old_work node_id in
@ -106,7 +106,7 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
let node = WorkUnit.node max_priority_work in
let t' = {t with worklist= M.remove (CFG.id node) t.worklist} in
Some (node, WorkUnit.visited_preds max_priority_work, t')
with Not_found -> None
with Caml.Not_found -> None
let empty cfg = {worklist= M.empty; cfg}

13
infer/src/atd/InferCommand.ml
Unescape View File

@ -9,17 +9,8 @@
open Core
(* NOTE: All variants must be also added to `all_commands` below *)
type t =
| Analyze
| Capture
| Compile
| Diff
| Events
| Explore
| Report
| ReportDiff
| Run
[@@deriving compare]
type t = Analyze | Capture | Compile | Diff | Events | Explore | Report | ReportDiff | Run
[@@deriving compare]
let equal = [%compare.equal : t]

2
infer/src/atd/InferCommand.mli
Unescape View File

@ -22,7 +22,7 @@ type t =
| Report (** post-process infer results and reports *)
| ReportDiff (** compute the difference of two infer reports *)
| Run (** orchestrate the capture, analysis, and reporting of a compilation command *)
[@@deriving compare]
[@@deriving compare]
val of_string : string -> t

12
infer/src/backend/Differential.ml
Unescape View File

@ -15,9 +15,9 @@ module LocListSet = struct
type t = Location.t list [@@deriving compare]
end)
let mem s xs = not (List.is_empty xs) && mem (List.sort ~cmp:Location.compare xs) s
let mem s xs = not (List.is_empty xs) && mem (List.sort ~compare:Location.compare xs) s
let add s xs = if List.is_empty xs then s else add (List.sort ~cmp:Location.compare xs) s
let add s xs = if List.is_empty xs then s else add (List.sort ~compare:Location.compare xs) s
end
let is_duplicate_report end_locs reported_ends =
@ -25,21 +25,21 @@ let is_duplicate_report end_locs reported_ends =
let sort_by_decreasing_preference_to_report issues =
let cmp (x: Jsonbug_t.jsonbug) (y: Jsonbug_t.jsonbug) =
let compare (x: Jsonbug_t.jsonbug) (y: Jsonbug_t.jsonbug) =
let n = Int.compare (List.length x.bug_trace) (List.length y.bug_trace) in
if n <> 0 then n
else
let n = String.compare x.hash y.hash in
if n <> 0 then n else Pervasives.compare x y
in
List.sort ~cmp issues
List.sort ~compare issues
let sort_by_location issues =
let cmp (x: Jsonbug_t.jsonbug) (y: Jsonbug_t.jsonbug) =
let compare (x: Jsonbug_t.jsonbug) (y: Jsonbug_t.jsonbug) =
[%compare : string * int * int] (x.file, x.line, x.column) (y.file, y.line, y.column)
in
List.sort ~cmp issues
List.sort ~compare issues
let dedup (issues: Jsonbug_t.jsonbug list) =

33
infer/src/backend/DifferentialFilters.ml
Unescape View File

@ -33,13 +33,13 @@ module FileRenamings = struct
let current_opt = List.Assoc.find ~equal:String.equal l "current" in
let previous_opt = List.Assoc.find ~equal:String.equal l "previous" in
match (current_opt, previous_opt) with
| Some `String current, Some `String previous ->
| Some (`String current), Some (`String previous) ->
{current; previous}
| None, _ ->
raise (Yojson.Json_error "\"current\" field missing")
| Some _, None ->
raise (Yojson.Json_error "\"previous\" field missing")
| Some _, Some `String _ ->
| Some _, Some (`String _) ->
raise (Yojson.Json_error "\"current\" field is not a string")
| Some _, Some _ ->
raise (Yojson.Json_error "\"previous\" field is not a string") )
@ -48,8 +48,9 @@ module FileRenamings = struct
with Yojson.Json_error err ->
L.(die UserError)
"Error parsing file renamings: %s@\n\
Expected JSON object of the following form: '%s', but instead got: '%s'" err
"{\"current\": \"aaa.java\", \"previous\": \"BBB.java\"}" (Yojson.Basic.to_string assoc)
Expected JSON object of the following form: '%s', but instead got: '%s'"
err "{\"current\": \"aaa.java\", \"previous\": \"BBB.java\"}"
(Yojson.Basic.to_string assoc)
in
match j with
| `List json_renamings ->
@ -84,15 +85,17 @@ end
(** Returns a triple [(l1', dups, l2')] where [dups] is the set of elements of that are in the
intersection of [l1] and [l2] according to [cmd] and additionally satisfy [pred], and [lN'] is
[lN] minus [dups]. [dups] contains only one witness for each removed issue, taken from [l1]. *)
let relative_complements ~cmp ?(pred= fun _ -> true) l1 l2 =
let relative_complements ~compare ?(pred= fun _ -> true) l1 l2 =
let rec aux ((out_l1, dups, out_l2) as out) in_l1 in_l2 =
let is_last_seen_dup v = match dups with ld :: _ -> Int.equal (cmp ld v) 0 | [] -> false in
let is_last_seen_dup v =
match dups with ld :: _ -> Int.equal (compare ld v) 0 | [] -> false
in
match (in_l1, in_l2) with
| i :: is, f :: fs when Int.equal (cmp i f) 0 ->
| i :: is, f :: fs when Int.equal (compare i f) 0 ->
(* i = f *)
if pred i then aux (out_l1, i :: dups, out_l2) is fs
else aux (i :: out_l1, dups, f :: out_l2) is fs
| i :: is, f :: _ when cmp i f < 0 ->
| i :: is, f :: _ when compare i f < 0 ->
(* i < f *)
let out_l1' = if is_last_seen_dup i then out_l1 else i :: out_l1 in
aux (out_l1', dups, out_l2) is in_l2
@ -107,8 +110,8 @@ let relative_complements ~cmp ?(pred= fun _ -> true) l1 l2 =
| _, _ ->
(List.rev_append in_l1 out_l1, dups, List.rev_append in_l2 out_l2)
in
let l1_sorted = List.sort ~cmp l1 in
let l2_sorted = List.sort ~cmp l2 in
let l1_sorted = List.sort ~compare l1 in
let l2_sorted = List.sort ~compare l2 in
aux ([], [], []) l1_sorted l2_sorted
@ -122,7 +125,7 @@ let skip_duplicated_types_on_filenames renamings (diff: Differential.t) : Differ
in
String.compare f1 f2
in
let cmp ((issue1, _) as issue_with_previous_file1) ((issue2, _) as issue_with_previous_file2) =
let compare ((issue1, _) as issue_with_previous_file1) ((issue2, _) as issue_with_previous_file2) =
[%compare : Caml.Digest.t * string * issue_file_with_renaming]
(issue1.Jsonbug_t.node_key, issue1.Jsonbug_t.bug_type, issue_with_previous_file1)
(issue2.Jsonbug_t.node_key, issue2.Jsonbug_t.bug_type, issue_with_previous_file2)
@ -137,7 +140,7 @@ let skip_duplicated_types_on_filenames renamings (diff: Differential.t) : Differ
in
let fixed_normalized = List.map diff.fixed ~f:(fun f -> (f, None)) in
let introduced_normalized', preexisting', fixed_normalized' =
relative_complements ~cmp introduced_normalized fixed_normalized
relative_complements ~compare introduced_normalized fixed_normalized
in
let list_map_fst = List.map ~f:fst in
( list_map_fst introduced_normalized'
@ -185,7 +188,7 @@ let skip_anonymous_class_renamings (diff: Differential.t) : Differential.t =
*)
let string_of_procedure_id issue = DB.strip_crc issue.Jsonbug_t.procedure_id in
let extension fname = snd (Filename.split_extension fname) in
let cmp (i1: Jsonbug_t.jsonbug) (i2: Jsonbug_t.jsonbug) =
let compare (i1: Jsonbug_t.jsonbug) (i2: Jsonbug_t.jsonbug) =
[%compare : file_extension option * weak_hash * procedure_id]
(extension i1.file, (i1.kind, i1.bug_type, i1.file, i1.key), string_of_procedure_id i1)
(extension i2.file, (i2.kind, i2.bug_type, i2.file, i2.key), string_of_procedure_id i2)
@ -202,12 +205,12 @@ let skip_anonymous_class_renamings (diff: Differential.t) : Differential.t =
try
ignore (Str.search_forward java_anon_class_pattern issue.procedure_id 0) ;
true
with Not_found -> false
with Caml.Not_found -> false
in
is_java_file () && has_anonymous_class_token ()
in
let introduced, preexisting, fixed =
relative_complements ~cmp ~pred diff.introduced diff.fixed
relative_complements ~compare ~pred diff.introduced diff.fixed
in
{introduced; fixed; preexisting= preexisting @ diff.preexisting}

2
infer/src/backend/DifferentialFilters.mli
Unescape View File

@ -37,7 +37,7 @@ val do_filter :
module VISIBLE_FOR_TESTING_DO_NOT_USE_DIRECTLY : sig
val relative_complements :
cmp:('a -> 'a -> int) -> ?pred:('a -> bool) -> 'a list -> 'a list
compare:('a -> 'a -> int) -> ?pred:('a -> bool) -> 'a list -> 'a list
-> 'a list * 'a list * 'a list
val skip_duplicated_types_on_filenames : FileRenamings.t -> Differential.t -> Differential.t

26
infer/src/backend/InferPrint.ml
Unescape View File

@ -229,9 +229,10 @@ module IssuesJson = struct
let should_report_source_file =
not (SourceFile.is_infer_model source_file) || Config.debug_mode || Config.debug_exceptions
in
if key.in_footprint && error_filter source_file key.err_desc key.err_name
&& should_report_source_file
&& should_report key.err_kind key.err_name key.err_desc err_data.err_class
if
key.in_footprint && error_filter source_file key.err_desc key.err_name
&& should_report_source_file
&& should_report key.err_kind key.err_name key.err_desc err_data.err_class
then (
let kind = Exceptions.err_kind_string key.err_kind in
let bug_type = key.err_name.IssueType.unique_id in
@ -366,8 +367,9 @@ module IssuesTxt = struct
| None ->
err_data.loc.Location.file
in
if key.in_footprint && error_filter source_file key.err_desc key.err_name
&& (not Config.filtering || String.is_empty (censored_reason key.err_name source_file))
if
key.in_footprint && error_filter source_file key.err_desc key.err_name
&& (not Config.filtering || String.is_empty (censored_reason key.err_name source_file))
then
Exceptions.pp_err ~node_key:err_data.node_id_key.node_key err_data.loc key.err_kind
key.err_name key.err_desc None fmt ()
@ -420,7 +422,7 @@ module Stats = struct
let process_loc loc stats =
try Hashtbl.find stats.files loc.Location.file with Not_found ->
try Hashtbl.find stats.files loc.Location.file with Caml.Not_found ->
Hashtbl.add stats.files loc.Location.file ()
@ -493,7 +495,7 @@ module Stats = struct
let is_verified = specs <> [] && not is_defective in
let is_checked = not (is_defective || is_verified) in
let is_timeout =
match Specs.(summary.stats.stats_failure) with None | Some FKcrash _ -> false | _ -> true
match Specs.(summary.stats.stats_failure) with None | Some (FKcrash _) -> false | _ -> true
in
stats.nprocs <- stats.nprocs + 1 ;
stats.nspecs <- stats.nspecs + List.length specs ;
@ -609,7 +611,7 @@ module Issue = struct
type t =
{proc_name: proc_name_; proc_location: Location.t; err_key: Errlog.err_key; err_data: err_data_}
[@@deriving compare]
[@@deriving compare]
(* If two issues are identical except for their procnames, they are probably duplicate reports on
two different instantiations of the same template. We don't want to spam users by reporting
@ -798,7 +800,7 @@ let pp_json_report_by_report_kind formats_by_report_kind fname =
in
let sorted_report =
let report = Jsonbug_j.report_of_string (String.concat ~sep:"\n" report_lines) in
List.sort ~cmp:tests_jsonbug_compare report
List.sort ~compare:tests_jsonbug_compare report
in
let pp_report_by_report_kind (report_kind, format_list) =
match (report_kind, format_list) with
@ -861,7 +863,7 @@ let spec_files_from_cmdline () =
(** Create an iterator which loads spec files one at a time *)
let get_summary_iterator () =
let sorted_spec_files = List.sort ~cmp:String.compare (spec_files_from_cmdline ()) in
let sorted_spec_files = List.sort ~compare:String.compare (spec_files_from_cmdline ()) in
let do_spec f fname =
match Specs.load_summary (DB.filename_from_string fname) with
| None ->
@ -954,8 +956,8 @@ let pp_summary_and_issues formats_by_report_kind issue_formats =
let iterate_summaries = get_summary_iterator () in
let all_issues = ref [] in
iterate_summaries (fun summary ->
all_issues
:= process_summary filters formats_by_report_kind linereader stats summary !all_issues ) ;
all_issues :=
process_summary filters formats_by_report_kind linereader stats summary !all_issues ) ;
List.iter
~f:(fun ({Issue.proc_name} as issue) ->
let error_filter = error_filter filters proc_name in

7
infer/src/backend/crashcontext.ml
Unescape View File

@ -73,8 +73,9 @@ let collect_all_summaries root_summaries_dir stacktrace_file stacktraces_dir =
Utils.directory_fold
(fun summaries path ->
(* check if the file is a JSON file under the crashcontext dir *)
if Sys.is_directory path <> `Yes && Filename.check_suffix path "json"
&& String.is_suffix ~suffix:"crashcontext" (Filename.dirname path)
if
Sys.is_directory path <> `Yes && Filename.check_suffix path "json"
&& String.is_suffix ~suffix:"crashcontext" (Filename.dirname path)
then path :: summaries
else summaries )
[] root_summaries_dir
@ -108,7 +109,7 @@ let collect_all_summaries root_summaries_dir stacktrace_file stacktraces_dir =
(* trace_fold runs immediately after trace_file_matcher in the
DB.fold_paths_matching statement below, so we don't need to
call Str.string_match again. *)
| Not_found
| Caml.Not_found
-> assert false
in
let input_output_file_pairs =

20
infer/src/backend/dotty.ml
Unescape View File

@ -35,7 +35,7 @@ type kind_of_links =
| LinkToSSL
| LinkToDLL
| LinkRetainCycle
[@@deriving compare]
[@@deriving compare]
(* coordinate identifies a node using two dimension: id is an numerical identifier of the node,*)
(* lambda identifies in which hpred parameter id lays in*)
@ -45,7 +45,7 @@ type coordinate = {id: int; lambda: int} [@@deriving compare]
(* useful for having nodes from within a struct and/or to inside a struct *)
type link =
{kind: kind_of_links; src: coordinate; src_fld: string; trg: coordinate; trg_fld: string}
[@@deriving compare]
[@@deriving compare]
let equal_link = [%compare.equal : link]
@ -218,7 +218,7 @@ let rec look_up_for_back_pointer e dotnodes lambda =
match dotnodes with
| [] ->
[]
| (Dotdllseg (coo, _, _, _, e4, _, _, _)) :: dotnodes' ->
| Dotdllseg (coo, _, _, _, e4, _, _, _) :: dotnodes' ->
if Exp.equal e e4 && Int.equal lambda coo.lambda then [coo.id + 1]
else look_up_for_back_pointer e dotnodes' lambda
| _ :: dotnodes' ->
@ -312,7 +312,7 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
match l with
| [] ->
[]
| (Dotdangling (coo, e, color)) :: l' ->
| Dotdangling (coo, e, color) :: l' ->
if List.exists ~f:(Exp.equal e) seen_exp then filter_duplicate l' seen_exp
else Dotdangling (coo, e, color) :: filter_duplicate l' (e :: seen_exp)
| box :: l' ->
@ -381,7 +381,7 @@ let rec dotty_mk_node pe sigma =
let set_exps_neq_zero pi =
let f = function
| Sil.Aneq (e, Exp.Const Const.Cint i) when IntLit.iszero i ->
| Sil.Aneq (e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
exps_neq_zero := e :: !exps_neq_zero
| _ ->
()
@ -396,7 +396,7 @@ let box_dangling e =
~f:(fun b -> match b with Dotdangling (_, e', _) -> Exp.equal e e' | _ -> false)
!dangling_dotboxes
in
match entry_e with [] -> None | (Dotdangling (coo, _, _)) :: _ -> Some coo.id | _ -> None
match entry_e with [] -> None | Dotdangling (coo, _, _) :: _ -> Some coo.id | _ -> None
(* NOTE: this cannot be possible since entry_e can be composed only by Dotdangling, see def of entry_e*)
@ -423,7 +423,7 @@ let compute_fields_struct sigma =
match s with
| [] ->
()
| (Sil.Hpointsto (_, se, _)) :: s' ->
| Sil.Hpointsto (_, se, _) :: s' ->
do_strexp se false ; fs s'
| _ :: s' ->
fs s'
@ -437,7 +437,7 @@ let compute_struct_exp_nodes sigma =
match s with
| [] ->
()
| (Sil.Hpointsto (e, Sil.Estruct _, _)) :: s' ->
| Sil.Hpointsto (e, Sil.Estruct _, _) :: s' ->
struct_exp_nodes := e :: !struct_exp_nodes ;
sen s'
| _ :: s' ->
@ -490,7 +490,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
[]
| Some n' ->
[(LinkStructToExp, Typ.Fieldname.to_string fn, n', "")] )
| [node] | [(Dotpointsto _); node] | [node; (Dotpointsto _)] ->
| [node] | [Dotpointsto _; node] | [node; Dotpointsto _] ->
let n = get_coordinate_id node in
if List.mem ~equal:Exp.equal !struct_exp_nodes e then
let e_no_special_char = strip_special_chars (Exp.to_string e) in
@ -536,7 +536,7 @@ let rec compute_target_array_elements dotnodes list_elements p f lambda =
[]
| Some n' ->
[(LinkArrayToExp, Exp.to_string idx, n', "")] )
| [node] | [(Dotpointsto _); node] | [node; (Dotpointsto _)] ->
| [node] | [Dotpointsto _; node] | [node; Dotpointsto _] ->
let n = get_coordinate_id node in
if List.mem ~equal:Exp.equal !struct_exp_nodes e then
let e_no_special_char = strip_special_chars (Exp.to_string e) in

69
infer/src/backend/errdesc.ml
Unescape View File

@ -55,7 +55,7 @@ let is_special_field matcher field_name_opt field =
let hpred_is_open_resource tenv prop = function
| Sil.Hpointsto (e, _, _) -> (
match Attribute.get_resource tenv prop e with
| Some Apred (Aresource {ra_kind= Racquire; ra_res= res}, _) ->
| Some (Apred (Aresource {ra_kind= Racquire; ra_res= res}, _)) ->
Some res
| _ ->
None )
@ -133,7 +133,7 @@ let find_program_variable_assignment node pvar : (Procdesc.Node.t * Ident.t) opt
let find_struct_by_value_assignment node pvar =
if Pvar.is_frontend_tmp pvar then
let find_instr node = function
| Sil.Call (_, Const Cfun pname, args, loc, cf) -> (
| Sil.Call (_, Const (Cfun pname), args, loc, cf) -> (
match List.last args with
| Some (Exp.Lvar last_arg, _) when Pvar.equal pvar last_arg ->
Some (node, pname, loc, cf)
@ -162,7 +162,7 @@ let find_ident_assignment node id : (Procdesc.Node.t * Exp.t) option =
let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option =
let find_instr n =
let filter = function
| Sil.Store (Exp.Lvar pvar_, _, Exp.Const Const.Cint i, _) when Pvar.equal pvar pvar_ ->
| Sil.Store (Exp.Lvar pvar_, _, Exp.Const (Const.Cint i), _) when Pvar.equal pvar pvar_ ->
IntLit.iszero i <> true_branch
| _ ->
false
@ -188,14 +188,14 @@ let rec find_normal_variable_load_ tenv (seen: Exp.Set.t) node id : DExp.t optio
Sil.d_exp e ;
L.d_ln () ) ;
exp_lv_dexp_ tenv seen node e
| Sil.Call (Some (id0, _), Exp.Const Const.Cfun pn, (e, _) :: _, _, _)
| Sil.Call (Some (id0, _), Exp.Const (Const.Cfun pn), (e, _) :: _, _, _)
when Ident.equal id id0 && Typ.Procname.equal pn (Typ.Procname.from_string_c_fun "__cast") ->
if verbose then (
L.d_str "find_normal_variable_load cast on " ;
Sil.d_exp e ;
L.d_ln () ) ;
exp_rv_dexp_ tenv seen node e
| Sil.Call (Some (id0, _), (Exp.Const Const.Cfun pname as fun_exp), args, loc, call_flags)
| Sil.Call (Some (id0, _), (Exp.Const (Const.Cfun pname) as fun_exp), args, loc, call_flags)
when Ident.equal id id0 ->
if verbose then (
L.d_str "find_normal_variable_load function call " ;
@ -447,9 +447,9 @@ let leak_from_list_abstraction hpred prop =
let hpred_type = function
| Sil.Hpointsto (_, _, texp) ->
Some texp
| Sil.Hlseg (_, {Sil.body= [(Sil.Hpointsto (_, _, texp))]}, _, _, _) ->
| Sil.Hlseg (_, {Sil.body= [Sil.Hpointsto (_, _, texp)]}, _, _, _) ->
Some texp
| Sil.Hdllseg (_, {Sil.body_dll= [(Sil.Hpointsto (_, _, texp))]}, _, _, _, _, _) ->
| Sil.Hdllseg (_, {Sil.body_dll= [Sil.Hpointsto (_, _, texp)]}, _, _, _, _, _) ->
Some texp
| _ ->
None
@ -513,7 +513,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
in
let res_action_opt, resource_opt, vpath =
match alloc_att_opt with
| Some PredSymb.Aresource ({ra_kind= Racquire} as ra) ->
| Some (PredSymb.Aresource ({ra_kind= Racquire} as ra)) ->
(Some ra, Some ra.ra_res, ra.ra_vpath)
| _ ->
(None, None, None)
@ -524,9 +524,9 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(Pvar.is_local pvar || Pvar.is_global pvar) && not (Pvar.is_frontend_tmp pvar)
&&
match (hpred_typ_opt, find_typ_without_ptr prop pvar) with
| Some Exp.Sizeof {typ= t1}, Some Exp.Sizeof {typ= {Typ.desc= Tptr (t2, _)}} ->
| Some (Exp.Sizeof {typ= t1}), Some (Exp.Sizeof {typ= {Typ.desc= Tptr (t2, _)}}) ->
Typ.equal t1 t2
| Some Exp.Sizeof {typ= {Typ.desc= Tint _}}, Some Exp.Sizeof {typ= {Typ.desc= Tint _}}
| Some (Exp.Sizeof {typ= {Typ.desc= Tint _}}), Some (Exp.Sizeof {typ= {Typ.desc= Tint _}})
when is_file ->
(* must be a file opened with "open" *)
true
@ -540,7 +540,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
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
| Some (Sil.Nullify (pvar, _)) when check_pvar pvar
-> (
if verbose then (
L.d_str "explain_leak: current instruction is Nullify for pvar " ;
@ -551,7 +551,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
Some (DExp.to_string de)
| _ ->
None )
| Some Sil.Abstract _ ->
| Some (Sil.Abstract _) ->
if verbose then (
L.d_str "explain_leak: current instruction is Abstract" ;
L.d_ln () ) ;
@ -570,7 +570,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
List.filter ~f:(fun pvar -> not (Pvar.is_frontend_tmp pvar)) nullify_pvars
in
value_str_from_pvars_vpath nullify_pvars_notmp vpath
| Some Sil.Store (lexp, _, _, _) when is_none vpath
| Some (Sil.Store (lexp, _, _, _)) when is_none vpath
-> (
if verbose then (
L.d_str "explain_leak: current instruction Set for " ;
@ -686,7 +686,7 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
when Pvar.is_local pv || Pvar.is_global pv || Pvar.is_seed pv ->
do_sexp sigma_acc' sigma_todo' (Exp.Lvar pv) sexp texp
| Sil.Hpointsto (Exp.Var id, sexp, texp)
when Ident.is_normal id || Ident.is_footprint id && substituted_from_normal id ->
when Ident.is_normal id || (Ident.is_footprint id && substituted_from_normal id) ->
do_sexp sigma_acc' sigma_todo' (Exp.Var id) sexp texp
| _ ->
(None, None)
@ -738,7 +738,7 @@ let explain_dexp_access prop dexp is_nullable =
let sexpo_to_inst = function
| None ->
None
| Some Sil.Eexp (_, inst) ->
| Some (Sil.Eexp (_, inst)) ->
Some inst
| Some se ->
if verbose then (
@ -783,7 +783,7 @@ let explain_dexp_access prop dexp is_nullable =
match (lookup de1, lookup de2) with
| None, _ | _, None ->
None
| Some Sil.Earray (_, esel, _), Some Sil.Eexp (e, _) ->
| Some (Sil.Earray (_, esel, _)), Some (Sil.Eexp (e, _)) ->
lookup_esel esel e
| Some se1, Some se2 ->
if verbose then (
@ -797,7 +797,7 @@ let explain_dexp_access prop dexp is_nullable =
match lookup (DExp.Dpvaraddr pvar) with
| None ->
None
| Some Sil.Estruct (fsel, _) ->
| Some (Sil.Estruct (fsel, _)) ->
lookup_fld fsel f
| Some _ ->
if verbose then (
@ -808,7 +808,7 @@ let explain_dexp_access prop dexp is_nullable =
match lookup (DExp.Dderef de1) with
| None ->
None
| Some Sil.Estruct (fsel, _) ->
| Some (Sil.Estruct (fsel, _)) ->
lookup_fld fsel f
| Some _ ->
if verbose then (
@ -819,9 +819,9 @@ let explain_dexp_access prop dexp is_nullable =
match lookup de1 with
| None ->
None
| Some Sil.Estruct (fsel, _) ->
| Some (Sil.Estruct (fsel, _)) ->
lookup_fld fsel f
| Some (Sil.Eexp (Const Cfun _, _) as fun_strexp) ->
| Some (Sil.Eexp (Const (Cfun _), _) as fun_strexp) ->
Some fun_strexp
| Some _ ->
if verbose then (
@ -832,7 +832,7 @@ let explain_dexp_access prop dexp is_nullable =
if verbose then ( L.d_str "lookup: found Dpvar " ; L.d_ln () ) ;
find_ptsto (Exp.Lvar pvar)
| DExp.Dderef de -> (
match lookup de with None -> None | Some Sil.Eexp (e, _) -> find_ptsto e | Some _ -> None )
match lookup de with None -> None | Some (Sil.Eexp (e, _)) -> find_ptsto e | Some _ -> None )
| DExp.Dbinop (Binop.PlusPI, DExp.Dpvar _, DExp.Dconst _) as de ->
if verbose then L.d_strln ("lookup: case )pvar + constant) " ^ DExp.to_string de) ;
None
@ -901,7 +901,7 @@ let create_dereference_desc proc_name tenv ?(use_buckets= false) ?(outermost_arr
let value_str, access_opt = explain_dereference_access outermost_array is_nullable de_opt prop in
let access_opt' =
match access_opt with
| Some Localise.Last_accessed _ when outermost_array ->
| Some (Localise.Last_accessed _) when outermost_array ->
None (* don't report last accessed for arrays *)
| _ ->
access_opt
@ -910,23 +910,24 @@ let create_dereference_desc proc_name tenv ?(use_buckets= false) ?(outermost_arr
let desc =
if Language.curr_language_is Clang && not is_premature_nil then
match de_opt with
| Some DExp.Dpvar pvar | Some DExp.Dpvaraddr pvar -> (
| Some (DExp.Dpvar pvar) | Some (DExp.Dpvaraddr pvar) -> (
match Attribute.get_objc_null tenv prop (Exp.Lvar pvar) with
| Some Apred (Aobjc_null, [_; vfs]) ->
| Some (Apred (Aobjc_null, [_; vfs])) ->
Localise.parameter_field_not_null_checked_desc desc vfs
| _ ->
desc )
| Some DExp.Dretcall (Dconst Cfun pname, this_dexp :: _, loc, _) ->
| Some (DExp.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _)) ->
if is_mutex_method pname then
Localise.desc_double_lock (Some pname) (DExp.to_string this_dexp) loc
else if is_vector_method pname then
Localise.desc_empty_vector_access (Some pname) (DExp.to_string this_dexp) loc
else desc
| Some DExp.Darrow (dexp, fieldname) | Some DExp.Ddot (dexp, fieldname) ->
| Some (DExp.Darrow (dexp, fieldname)) | Some (DExp.Ddot (dexp, fieldname)) ->
if is_special_field mutex_matcher (Some "null_if_locked") fieldname then
Localise.desc_double_lock None (DExp.to_string dexp) loc
else if is_special_field vector_matcher (Some "beginPtr") fieldname
|| is_special_field vector_matcher (Some "endPtr") fieldname
else if
is_special_field vector_matcher (Some "beginPtr") fieldname
|| is_special_field vector_matcher (Some "endPtr") fieldname
then Localise.desc_empty_vector_access None (DExp.to_string dexp) loc
else desc
| _ ->
@ -998,19 +999,19 @@ let explain_access_ proc_name tenv ?(use_buckets= false) ?(outermost_array= fals
loc =
let find_exp_dereferenced () =
match State.get_instr () with
| Some Sil.Store (e, _, _, _) ->
| Some (Sil.Store (e, _, _, _)) ->
if verbose then (
L.d_str "explain_dereference Sil.Store " ;
Sil.d_exp e ;
L.d_ln () ) ;
Some e
| Some Sil.Load (_, e, _, _) ->
| Some (Sil.Load (_, e, _, _)) ->
if verbose then (
L.d_str "explain_dereference Binop.Leteref " ;
Sil.d_exp e ;
L.d_ln () ) ;
Some e
| Some Sil.Call (_, Exp.Const Const.Cfun fn, [(e, _)], _, _)
| Some (Sil.Call (_, Exp.Const (Const.Cfun fn), [(e, _)], _, _))
when List.exists ~f:(Typ.Procname.equal fn)
[BuiltinDecl.free; BuiltinDecl.__delete; BuiltinDecl.__delete_array] ->
if verbose then (
@ -1018,7 +1019,7 @@ let explain_access_ proc_name tenv ?(use_buckets= false) ?(outermost_array= fals
Sil.d_exp e ;
L.d_ln () ) ;
Some e
| Some Sil.Call (_, (Exp.Var _ as e), _, _, _) ->
| Some (Sil.Call (_, (Exp.Var _ as e), _, _, _)) ->
if verbose then (
L.d_str "explain_dereference Sil.Call " ;
Sil.d_exp e ;
@ -1082,7 +1083,7 @@ let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n p
let node = State.get_node () in
let loc = State.get_loc () in
match State.get_instr () with
| Some Sil.Call (_, _, args, _, _) -> (
| Some (Sil.Call (_, _, args, _, _)) -> (
try
let arg = fst (List.nth_exn args (n - 1)) in
let dexp_opt = exp_rv_dexp tenv node arg in
@ -1208,7 +1209,7 @@ let explain_unreachable_code_after loc = Localise.desc_unreachable_code_after lo
let explain_stack_variable_address_escape loc pvar addr_dexp_opt =
let addr_dexp_str =
match addr_dexp_opt with
| Some DExp.Dpvar pv
| Some (DExp.Dpvar pv)
when Pvar.is_local pv && Mangled.equal (Pvar.get_name pv) Ident.name_return ->
Some "the caller via a return"
| Some dexp ->

12
infer/src/backend/exe_env.ml
Unescape View File

@ -32,7 +32,7 @@ let create_file_data table source =
match SourceFile.Hash.find table source with
| file_data ->
file_data
| exception Not_found ->
| exception Caml.Not_found ->
let file_data = new_file_data source in
SourceFile.Hash.add table source file_data ;
file_data
@ -44,7 +44,7 @@ type t =
; source_file: SourceFile.t (** source file being analyzed *) }
let get_file_data exe_env pname =
try Some (Typ.Procname.Hash.find exe_env.proc_map pname) with Not_found ->
try Some (Typ.Procname.Hash.find exe_env.proc_map pname) with Caml.Not_found ->
let source_file_opt =
match Attributes.load pname with
| None ->
@ -114,12 +114,8 @@ let get_cfg exe_env pname =
(** return the proc desc associated to the procedure *)
let get_proc_desc exe_env pname =
match get_cfg exe_env pname with
| Some cfg -> (
match Typ.Procname.Hash.find cfg pname with
| proc_desc ->
Some proc_desc
| exception Not_found ->
None )
| Some cfg ->
Typ.Procname.Hash.find_opt cfg pname
| None ->
None

20
infer/src/backend/inferconfig.ml
Unescape View File

@ -41,7 +41,7 @@ let is_matching patterns source_file =
let path = SourceFile.to_rel_path source_file in
List.exists
~f:(fun pattern ->
try Int.equal (Str.search_forward pattern path 0) 0 with Not_found -> false )
try Int.equal (Str.search_forward pattern path 0) 0 with Caml.Not_found -> false )
patterns
@ -61,7 +61,7 @@ module FileContainsStringMatcher = struct
let file_contains regexp file_in =
let rec loop () =
try Str.search_forward regexp (In_channel.input_line_exn file_in) 0 >= 0 with
| Not_found ->
| Caml.Not_found ->
loop ()
| End_of_file ->
false
@ -75,7 +75,7 @@ module FileContainsStringMatcher = struct
let source_map = ref SourceFile.Map.empty in
let regexp = Str.regexp (String.concat ~sep:"\\|" s_patterns) in
fun source_file ->
try SourceFile.Map.find source_file !source_map with Not_found ->
try SourceFile.Map.find source_file !source_map with Caml.Not_found ->
try
let file_in = In_channel.create (SourceFile.to_abs_path source_file) in
let pattern_found = file_contains regexp file_in in
@ -103,7 +103,11 @@ module FileOrProcMatcher = struct
let pattern_map =
List.fold
~f:(fun map pattern ->
let previous = try String.Map.find_exn map pattern.class_name with Not_found -> [] in
let previous =
try String.Map.find_exn map pattern.class_name with
| Not_found_s _ | Caml.Not_found ->
[]
in
String.Map.set ~key:pattern.class_name ~data:(pattern :: previous) map )
~init:String.Map.empty m_patterns
in
@ -116,7 +120,9 @@ module FileOrProcMatcher = struct
~f:(fun p ->
match p.method_name with None -> true | Some m -> String.equal m method_name )
class_patterns
with Not_found -> false
with
| Not_found_s _ | Caml.Not_found ->
false
in
fun _ proc_name ->
match proc_name with Typ.Procname.Java pname_java -> do_java pname_java | _ -> false
@ -245,9 +251,9 @@ let patterns_of_json_with_key (json_key, json) =
List.fold ~f:loop ~init:default_source_contains assoc
in
match detect_pattern assoc with
| Ok Method_pattern (language, _) ->
| Ok (Method_pattern (language, _)) ->
Ok (Method_pattern (language, create_method_pattern assoc))
| Ok Source_contains (language, _) ->
| Ok (Source_contains (language, _)) ->
Ok (Source_contains (language, create_string_contains assoc))
| Error _ as error ->
error

4
infer/src/backend/ondemand.ml
Unescape View File

@ -177,7 +177,7 @@ let analyze_proc_desc ~caller_pdesc callee_pdesc =
if is_active callee_pname then None
else
let cache = Lazy.force cached_results in
try Typ.Procname.Hash.find cache callee_pname with Not_found ->
try Typ.Procname.Hash.find cache callee_pname with Caml.Not_found ->
let summary_option =
let proc_attributes = Procdesc.get_attributes callee_pdesc in
if should_be_analyzed callee_pname proc_attributes then
@ -194,7 +194,7 @@ let analyze_proc_name ?caller_pdesc callee_pname =
if is_active callee_pname then None
else
let cache = Lazy.force cached_results in
try Typ.Procname.Hash.find cache callee_pname with Not_found ->
try Typ.Procname.Hash.find cache callee_pname with Caml.Not_found ->
let summary_option =
let callbacks = Option.value_exn !callbacks_ref in
if procedure_should_be_analyzed callee_pname then

21
infer/src/backend/printer.ml
Unescape View File

@ -46,7 +46,7 @@ module LineReader = struct
let file_data (hash: t) fname =
try Some (Hashtbl.find hash fname) with Not_found ->
try Some (Hashtbl.find hash fname) with Caml.Not_found ->
try
let lines_arr = read_file (SourceFile.to_abs_path fname) in
Hashtbl.add hash fname lines_arr ; Some lines_arr
@ -330,10 +330,11 @@ let force_delayed_prints () =
(** Start a session, and create a new html fine for the node if it does not exist yet *)
let start_session ~pp_name node (loc: Location.t) proc_name session source =
let node_id = Procdesc.Node.get_id node in
if NodesHtml.start_node
(node_id :> int)
loc proc_name (Procdesc.Node.get_preds node) (Procdesc.Node.get_succs node)
(Procdesc.Node.get_exn node) source
if
NodesHtml.start_node
(node_id :> int)
loc proc_name (Procdesc.Node.get_preds node) (Procdesc.Node.get_succs node)
(Procdesc.Node.get_exn node) source
then
F.fprintf !curr_html_formatter "%a<LISTING>%a</LISTING>%a" Io_infer.Html.pp_start_color
Pp.Green
@ -371,7 +372,7 @@ let write_proc_html pdesc =
if Config.write_html then (
let pname = Procdesc.get_proc_name pdesc in
let source = (Procdesc.get_loc pdesc).file in
let nodes = List.sort ~cmp:Procdesc.Node.compare (Procdesc.get_nodes pdesc) in
let nodes = List.sort ~compare:Procdesc.Node.compare (Procdesc.get_nodes pdesc) in
let linenum = (Procdesc.Node.get_loc (List.hd_exn nodes)).Location.line in
let fd, fmt =
Io_infer.Html.create (DB.Results_dir.Abs_source_dir source) [Typ.Procname.to_filename pname]
@ -400,7 +401,7 @@ let create_table_err_per_line err_log =
try
let set = Hashtbl.find err_per_line err_data.loc.Location.line in
Hashtbl.replace err_per_line err_data.loc.Location.line (String.Set.add set err_str)
with Not_found ->
with Caml.Not_found ->
Hashtbl.add err_per_line err_data.loc.Location.line (String.Set.singleton err_str)
in
Errlog.iter add_err err_log ; err_per_line
@ -415,7 +416,7 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro
let proc_name = Procdesc.get_proc_name proc_desc in
let process_node n =
let lnum = (Procdesc.Node.get_loc n).Location.line in
let curr_nodes = try Hashtbl.find table_nodes_at_linenum lnum with Not_found -> [] in
let curr_nodes = try Hashtbl.find table_nodes_at_linenum lnum with Caml.Not_found -> [] in
Hashtbl.replace table_nodes_at_linenum lnum (n :: curr_nodes)
in
let proc_loc = Procdesc.get_loc proc_desc in
@ -459,13 +460,13 @@ let write_html_file linereader filename procs =
raise End_of_file
in
let nodes_at_linenum =
try Hashtbl.find table_nodes_at_linenum line_number with Not_found -> []
try Hashtbl.find table_nodes_at_linenum line_number with Caml.Not_found -> []
in
let errors_at_linenum =
try
let errset = Hashtbl.find table_err_per_line line_number in
String.Set.elements errset
with Not_found -> []
with Caml.Not_found -> []
in
F.fprintf fmt "<tr><td class=\"num\" id=\"LINE%d\">%d</td><td class=\"line\">%s " line_number
line_number line_html ;

4
infer/src/backend/reporting.ml
Unescape View File

@ -75,8 +75,8 @@ let log_issue_deprecated ?(store_summary= false) err_kind proc_name ?loc ?node_i
| None ->
L.(die InternalError)
"Trying to report error on procedure %a, but cannot because no summary exists for this \
procedure. Did you mean to log the error on the caller of %a instead?" Typ.Procname.pp
proc_name Typ.Procname.pp proc_name
procedure. Did you mean to log the error on the caller of %a instead?"
Typ.Procname.pp proc_name Typ.Procname.pp proc_name
let log_error = log_issue_from_summary Exceptions.Kerror

12
infer/src/backend/specs.ml
Unescape View File

@ -27,10 +27,8 @@ module Jprop = struct
let compare_id_ _ _ = 0
(** Remember when a prop is obtained as the join of two other props; the first parameter is an id *)
type 'a t =
| Prop of id_ * 'a Prop.t
| Joined of id_ * 'a Prop.t * 'a t * 'a t
[@@deriving compare]
type 'a t = Prop of id_ * 'a Prop.t | Joined of id_ * 'a Prop.t * 'a t * 'a t
[@@deriving compare]
(** Comparison for joined_prop *)
let compare jp1 jp2 = compare (fun _ _ -> 0) jp1 jp2
@ -79,9 +77,9 @@ module Jprop = struct
let rec pp_seq_newline f = function
| [] ->
()
| [(Prop (n, p))] ->
| [Prop (n, p)] ->
F.fprintf f "PROP %d:@\n%a" n (Prop.pp_prop pe) p
| [(Joined (n, p, p1, p2))] ->
| [Joined (n, p, p1, p2)] ->
if not shallow then F.fprintf f "%a@\n" pp_seq_newline [p1] ;
if not shallow then F.fprintf f "%a@\n" pp_seq_newline [p2] ;
F.fprintf f "PROP %d (join of %d,%d):@\n%a" n (get_id p1) (get_id p2) (Prop.pp_prop pe) p
@ -555,7 +553,7 @@ let load_summary_to_spec_table =
let get_summary proc_name =
try Some (Typ.Procname.Hash.find spec_tbl proc_name) with Not_found ->
try Some (Typ.Procname.Hash.find spec_tbl proc_name) with Caml.Not_found ->
load_summary_to_spec_table proc_name

41
infer/src/base/CommandDoc.ml
Unescape View File

@ -54,7 +54,7 @@ let analyze =
~synopsis:{|$(b,infer) $(b,analyze) $(i,[options])
$(b,infer) $(i,[options])|}
~description:[`P "Analyze the files captured in the project results directory and report."]
~see_also:InferCommand.([Report; Run])
~see_also:InferCommand.[Report; Run]
let capture =
@ -78,7 +78,7 @@ $(b,infer) $(b,capture) $(i,[--no-xcpretty]) $(i,[options]) $(b,--) $(b,xcodebui
intercepts calls to the compiler to read source files, translate them into infer's \
intermediate representation, and store the result of the translation in the results \
directory." ]
~see_also:InferCommand.([Analyze; Compile; Run])
~see_also:InferCommand.[Analyze; Compile; Run]
let compile =
@ -112,7 +112,7 @@ let compile =
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ..
infer capture --compilation-database compile_commands.json|}
]
~see_also:InferCommand.([Capture])
~see_also:InferCommand.[Capture]
let diff =
@ -120,7 +120,7 @@ let diff =
~short_description:"Report the difference between two versions of a project"
~synopsis:"$(b,infer) $(b,diff) $(i,[options])"
~description:[`P "EXPERIMENTAL AND IN NO WAY READY TO USE"]
~see_also:InferCommand.([ReportDiff; Run])
~see_also:InferCommand.[ReportDiff; Run]
let explore =
@ -136,7 +136,7 @@ $(b,infer) $(b,explore) $(b,--procedures) $(i,[options])|}
; `P
"If $(b,--procedures) is passed, print information about each procedure captured by \
infer." ]
~see_also:InferCommand.([Report; Run])
~see_also:InferCommand.[Report; Run]
let infer =
@ -174,9 +174,9 @@ $(b,infer) $(i,[options])|}
variable, then from the command line. Options in $(b,%s) take precedence over \
options in $(b,%s), and options passed on the command line take precedence over \
options in $(b,%s). See the $(i,%s) and $(i,%s) sections of this manual for more \
information." inferconfig_file CLOpt.args_env_var CLOpt.args_env_var
inferconfig_file CLOpt.args_env_var Cmdliner.Manpage.s_environment
Cmdliner.Manpage.s_files)
information."
inferconfig_file CLOpt.args_env_var CLOpt.args_env_var inferconfig_file
CLOpt.args_env_var Cmdliner.Manpage.s_environment Cmdliner.Manpage.s_files)
; `P
"Options can be specified inside an argument file $(i,file) by passing \
$(b,@)$(i,file) as argument. The format is one option per line, and enclosing single \
@ -196,8 +196,9 @@ $(b,infer) $(i,[options])|}
"Extra arguments may be passed to all infer commands using the $(b,%s) environment \
variable (see the $(i,%s) section). $(b,%s) is expected to contain a string of \
%c-separated options. For instance, calling `%s=--debug^--print-logs infer` is \
equivalent to calling `infer --debug --print-logs`." CLOpt.args_env_var
Cmdliner.Manpage.s_options CLOpt.args_env_var CLOpt.env_var_sep CLOpt.args_env_var)
equivalent to calling `infer --debug --print-logs`."
CLOpt.args_env_var Cmdliner.Manpage.s_options CLOpt.args_env_var CLOpt.env_var_sep
CLOpt.args_env_var)
; `P
(Printf.sprintf "$(b,%s): Tells infer where to find the %s file. (See the %s section)"
inferconfig_env_var inferconfig_file Cmdliner.Manpage.s_files)
@ -205,13 +206,15 @@ $(b,infer) $(i,[options])|}
(Printf.sprintf
"If $(b,%s) is set to \"1\", then infer commands will exit with an error code in \
some cases when otherwise a simple warning would be emitted on stderr, for instance \
if a deprecated form of an option is used." CLOpt.strict_mode_env_var) ]
if a deprecated form of an option is used."
CLOpt.strict_mode_env_var) ]
~files:
[ `P
(Printf.sprintf
"$(b,%s) can be used to store infer options. Its format is that of a JSON record, \
where fields are infer long-form options, without their leading \"--\", and values \
depend on the type of the option:" inferconfig_file)
depend on the type of the option:"
inferconfig_file)
; `Noblank
; `P "- for switches options, the value is a JSON boolean (true or false, without quotes)"
; `Noblank
@ -222,13 +225,15 @@ $(b,infer) $(i,[options])|}
; `P
(Printf.sprintf
"- path options have string values, and are interpreted relative to the location of \
the %s file" inferconfig_file)
the %s file"
inferconfig_file)
; `Noblank
; `P "- cumulative options are JSON arrays of the appropriate type"
; `P
(Printf.sprintf
"Infer will look for an $(b,%s) file in the current directory, then its parent, \
etc., stopping at the first $(b,%s) file found." inferconfig_file inferconfig_file)
etc., stopping at the first $(b,%s) file found."
inferconfig_file inferconfig_file)
; `P "Example:"
; `Pre
{| {
@ -248,7 +253,7 @@ let report =
; `P
"If no specs file are passed on the command line, process all the .specs in the results \
directory." ]
~see_also:InferCommand.([ReportDiff; Run])
~see_also:InferCommand.[ReportDiff; Run]
let reportdiff =
@ -272,7 +277,7 @@ let reportdiff =
"- $(b,preexisting.json) contains the issues found in both $(i,previous) and \
$(i,current)."
; `P "All three files follow the same format as normal infer reports." ]
~see_also:InferCommand.([Report])
~see_also:InferCommand.[Report]
let events =
@ -283,7 +288,7 @@ let events =
[ `P
"Emit to stdout one JSON object per line, each describing a logged event happened \
during the execution of Infer" ]
~see_also:InferCommand.([Report; Run])
~see_also:InferCommand.[Report; Run]
let run =
@ -298,7 +303,7 @@ $(b,infer) $(i,[options]) $(b,--) $(i,compile command)|}
following sequence of commands:"
; `Pre {|$(b,infer) $(b,capture) $(i,[options])
$(b,infer) $(b,analyze) $(i,[options])|} ]
~see_also:InferCommand.([Analyze; Capture; Report])
~see_also:InferCommand.[Analyze; Capture; Report]
let command_to_data =

30
infer/src/base/CommandLineOption.ml
Unescape View File

@ -153,7 +153,8 @@ let check_no_duplicates desc_list =
| _ :: tl ->
check_for_duplicates_ tl
in
check_for_duplicates_ (List.sort ~cmp:(fun (x, _, _) (y, _, _) -> String.compare x y) desc_list)
check_for_duplicates_
(List.sort ~compare:(fun (x, _, _) (y, _, _) -> String.compare x y) desc_list)
let parse_mode_desc_lists = List.map ~f:(fun parse_mode -> (parse_mode, ref [])) all_parse_modes
@ -192,7 +193,7 @@ let add parse_mode sections desc =
let sections =
List.Assoc.find_exn ~equal:InferCommand.equal help_sections_desc_lists command
in
let prev_contents = try SectionMap.find section !sections with Not_found -> [] in
let prev_contents = try SectionMap.find section !sections with Caml.Not_found -> [] in
sections := SectionMap.add section (desc :: prev_contents) !sections
in
List.iter sections ~f:add_to_section ;
@ -219,7 +220,7 @@ let add parse_mode sections desc =
in
(* in the help of `infer` itself, show in which specific commands the option is used *)
let commands =
List.map ~f:fst sections |> List.sort ~cmp:InferCommand.compare
List.map ~f:fst sections |> List.sort ~compare:InferCommand.compare
|> List.remove_consecutive_duplicates ~equal:InferCommand.equal
|> List.map ~f:(fun cmd ->
let exe = InferCommand.to_exe_name cmd in
@ -620,7 +621,7 @@ let normalize_desc_list speclist =
let lower_norm s = String.lowercase @@ norm s in
String.compare (lower_norm x) (lower_norm y)
in
let sort speclist = List.sort ~cmp:compare_specs speclist in
let sort speclist = List.sort ~compare:compare_specs speclist in
sort speclist
@ -677,9 +678,9 @@ let set_curr_speclist_for_parse_mode ~usage parse_mode =
let full_desc_list =
List.Assoc.find_exn ~equal:equal_parse_mode parse_mode_desc_lists parse_mode
in
curr_speclist
:= normalize_desc_list !full_desc_list |> List.map ~f:xdesc |> add_or_suppress_help
|> to_arg_speclist ;
curr_speclist :=
normalize_desc_list !full_desc_list |> List.map ~f:xdesc |> add_or_suppress_help
|> to_arg_speclist ;
assert (check_no_duplicates !curr_speclist) ;
curr_usage
@ -712,7 +713,7 @@ let mk_subcommand command ?on_unknown_arg:(on_unknown = `Reject) ~name ?deprecat
?in_help command_doc =
let switch () =
curr_command := Some command ;
anon_arg_action := {(!anon_arg_action) with on_unknown}
anon_arg_action := {!anon_arg_action with on_unknown}
in
( match deprecated_long with
| Some long ->
@ -750,8 +751,9 @@ let anon_fun arg =
if !anon_arg_action.parse_argfiles && String.is_prefix arg ~prefix:"@" then
(* stop parsing the current args and go look in that argfile *)
raise (SubArguments (args_from_argfile arg))
else if !anon_arg_action.parse_subcommands
&& List.Assoc.mem !subcommand_actions ~equal:String.equal arg
else if
!anon_arg_action.parse_subcommands
&& List.Assoc.mem !subcommand_actions ~equal:String.equal arg
then
let command_switch = List.Assoc.find_exn !subcommand_actions ~equal:String.equal arg in
match (!curr_command, is_originator) with
@ -796,7 +798,7 @@ let decode_inferconfig_to_argv path =
in
decode_json ~inferconfig_dir json_val @ result
with
| Not_found ->
| Not_found_s _ | Caml.Not_found ->
warnf "WARNING: while reading config file %s:@\nUnknown option %s@." path key ;
result
| YBU.Type_error (msg, json) ->
@ -816,9 +818,9 @@ let encode_argv_to_env argv =
~f:(fun arg ->
not (String.contains arg env_var_sep)
||
(warnf "WARNING: Ignoring unsupported option containing '%c' character: %s@\n" env_var_sep
arg ;
false) )
( warnf "WARNING: Ignoring unsupported option containing '%c' character: %s@\n"
env_var_sep arg ;
false ) )
argv)

2
infer/src/base/CommandLineOption.mli
Unescape View File

@ -18,7 +18,7 @@ type parse_mode =
| InferCommand (** parse arguments as arguments for infer *)
| Javac (** parse arguments passed to the Java compiler *)
| NoParse (** all arguments are anonymous arguments, no parsing is attempted *)
[@@deriving compare]
[@@deriving compare]
val is_originator : bool

279
infer/src/base/Config.ml
Unescape View File

@ -18,13 +18,8 @@ module F = Format
module CLOpt = CommandLineOption
module L = Die
type analyzer =
| CaptureOnly
| CompileOnly
| Checkers
| Crashcontext
| Linters
[@@deriving compare]
type analyzer = CaptureOnly | CompileOnly | Checkers | Crashcontext | Linters
[@@deriving compare]
let equal_analyzer = [%compare.equal : analyzer]
@ -83,7 +78,7 @@ type compilation_database_dependencies =
(* get the compilation database of the dependencies up to depth n
by [Deps (Some n)], or all by [Deps None] *)
| NoDeps
[@@deriving compare]
[@@deriving compare]
type build_system =
| BAnalyze
@ -98,7 +93,7 @@ type build_system =
| BNdk
| BPython
| BXcode
[@@deriving compare]
[@@deriving compare]
let equal_build_system = [%compare.equal : build_system]
@ -131,8 +126,9 @@ let build_system_exe_assoc =
let build_system_of_exe_name name =
try List.Assoc.find_exn ~equal:String.equal (List.Assoc.inverse build_system_exe_assoc) name
with Not_found -> L.(die InternalError) "Unsupported build command %s" name
try List.Assoc.find_exn ~equal:String.equal (List.Assoc.inverse build_system_exe_assoc) name with
| Not_found_s _ | Caml.Not_found ->
L.(die InternalError) "Unsupported build command %s" name
let string_of_build_system build_system =
@ -606,7 +602,7 @@ and ( analysis_blacklist_files_containing_options
(let long = "<analyzer>-" ^ suffix in
CLOpt.mk_string_list ~long ~meta
~f:(fun _ -> raise (Arg.Bad "invalid option"))
~in_help:InferCommand.([(Report, manual_generic); (Run, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic); (Run, manual_generic)]
help) ;
List.map ~f:(fun (name, analyzer) -> (analyzer, mk_option analyzer name)) string_to_analyzer
in
@ -614,11 +610,13 @@ and ( analysis_blacklist_files_containing_options
~deprecated_suffix:["blacklist_files_containing"]
~help:
"blacklist files containing the specified string for the given analyzer (see \
$(b,--analyzer) for valid values)" ~meta:"string"
$(b,--analyzer) for valid values)"
~meta:"string"
, mk_filtering_options ~suffix:"blacklist-path-regex" ~deprecated_suffix:["blacklist"]
~help:
"blacklist the analysis of files whose relative path matches the specified OCaml-style \
regex (to whitelist: $(b,--<analyzer>-whitelist-path-regex))" ~meta:"path_regex"
regex (to whitelist: $(b,--<analyzer>-whitelist-path-regex))"
~meta:"path_regex"
, mk_filtering_options ~suffix:"whitelist-path-regex" ~deprecated_suffix:["whitelist"] ~help:""
~meta:"path_regex"
, mk_filtering_options ~suffix:"suppress-errors" ~deprecated_suffix:["suppress_errors"]
@ -643,7 +641,7 @@ and analyzer =
()
in
CLOpt.mk_symbol_opt ~deprecated:["analyzer"] ~long:"analyzer" ~short:'a'
~in_help:InferCommand.([(Analyze, manual_generic); (Run, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic); (Run, manual_generic)]
{|Specify which analyzer to run (only one at a time is supported):
- $(b,biabduction): run the bi-abduction based checker only, in particular to check for memory errors
- $(b,checkers): run the default checkers, including the bi-abduction based checker for memory errors (default)
@ -661,7 +659,8 @@ and analyzer =
CLOpt.warnf
"WARNING: The analyzer '%s' is deprecated, use the '%s' subcommand instead:@\n\
@\n \
infer %s ..." analyzer_str analyzer_str analyzer_str ;
infer %s ..."
analyzer_str analyzer_str analyzer_str ;
x
| _ as x ->
x)
@ -692,7 +691,7 @@ and ( annotation_reachability
let mk_checker ?(default= false) ?(deprecated= []) ~long doc =
let var =
CLOpt.mk_bool ~long
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
~default ~deprecated doc
in
all_checkers := (var, long, doc, default) :: !all_checkers ;
@ -749,7 +748,7 @@ and ( annotation_reachability
let mk_only (var, long, doc, _) =
let _ : bool ref =
CLOpt.mk_bool_group ~long:(long ^ "-only")
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
~f:(fun b ->
disable_all_checkers () ;
var := b ;
@ -765,7 +764,7 @@ and ( annotation_reachability
List.iter ~f:mk_only !all_checkers ;
let _default_checkers : bool ref =
CLOpt.mk_bool_group ~long:"default-checkers"
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
~default:true
( "Default checkers: "
^ ( List.rev_filter_map
@ -807,7 +806,7 @@ and ( annotation_reachability
and annotation_reachability_custom_pairs =
CLOpt.mk_json ~long:"annotation-reachability-custom-pairs"
~in_help:InferCommand.([(Analyze, manual_java)])
~in_help:InferCommand.[(Analyze, manual_java)]
{|Specify custom sources/sink for the annotation reachability checker
Example format: for custom annotations com.my.annotation.{Source1,Source2,Sink1}
{ "sources" : ["Source1", "Source2"], "sink" : "Sink1" }|}
@ -815,7 +814,7 @@ Example format: for custom annotations com.my.annotation.{Source1,Source2,Sink1}
and append_buck_flavors =
CLOpt.mk_string_list ~long:"append-buck-flavors"
~in_help:InferCommand.([(Capture, manual_buck_flavors)])
~in_help:InferCommand.[(Capture, manual_buck_flavors)]
"Additional Buck flavors to append to targets discovered by the \
$(b,--buck-compilation-database) option."
@ -831,13 +830,13 @@ and array_level =
and blacklist =
CLOpt.mk_string_opt ~deprecated:["-blacklist-regex"; "-blacklist"] ~long:"buck-blacklist"
~in_help:InferCommand.([(Run, manual_buck_flavors); (Capture, manual_buck_flavors)])
~in_help:InferCommand.[(Run, manual_buck_flavors); (Capture, manual_buck_flavors)]
~meta:"regex" "Skip analysis of files matched by the specified regular expression"
and bootclasspath =
CLOpt.mk_string_opt ~long:"bootclasspath"
~in_help:InferCommand.([(Capture, manual_java)])
~in_help:InferCommand.[(Capture, manual_java)]
"Specify the Java bootclasspath"
@ -846,27 +845,28 @@ and buck = CLOpt.mk_bool ~long:"buck" ""
and buck_build_args =
CLOpt.mk_string_list ~long:"Xbuck"
~in_help:InferCommand.([(Capture, manual_buck_flavors)])
~in_help:InferCommand.[(Capture, manual_buck_flavors)]
"Pass values as command-line arguments to invocations of $(i,`buck build`)"
and buck_compilation_database_depth =
CLOpt.mk_int_opt ~long:"buck-compilation-database-depth"
~in_help:InferCommand.([(Capture, manual_buck_compilation_db)])
~in_help:InferCommand.[(Capture, manual_buck_compilation_db)]
"Depth of dependencies used by the $(b,--buck-compilation-database deps) option. By default, \
all recursive dependencies are captured." ~meta:"int"
all recursive dependencies are captured."
~meta:"int"
and buck_compilation_database =
CLOpt.mk_symbol_opt ~long:"buck-compilation-database" ~deprecated:["-use-compilation-database"]
~in_help:InferCommand.([(Capture, manual_buck_compilation_db)])
~in_help:InferCommand.[(Capture, manual_buck_compilation_db)]
"Buck integration using the compilation database, with or without dependencies."
~symbols:[("no-deps", `NoDeps); ("deps", `DepsTmp)]
and buck_out =
CLOpt.mk_path_opt ~long:"buck-out"
~in_help:InferCommand.([(Capture, manual_buck_java)])
~in_help:InferCommand.[(Capture, manual_buck_java)]
~meta:"dir" "Specify the root directory of buck-out"
@ -877,7 +877,7 @@ and capture =
and changed_files_index =
CLOpt.mk_path_opt ~long:"changed-files-index"
~in_help:InferCommand.([(Analyze, manual_generic); (Diff, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic); (Diff, manual_generic)]
~meta:"file"
"Specify the file containing the list of source files from which reactive analysis should \
start. Source files should be specified relative to project root or be absolute"
@ -890,7 +890,7 @@ and check_version =
and clang_biniou_file =
CLOpt.mk_path_opt ~long:"clang-biniou-file"
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
~meta:"file" "Specify a file containing the AST of the program, in biniou format"
@ -898,7 +898,7 @@ and clang_compilation_dbs = ref []
and clang_frontend_action =
CLOpt.mk_symbol_opt ~long:"" ~deprecated:["-clang-frontend-action"]
~in_help:InferCommand.([(Capture, manual_clang); (Run, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang); (Run, manual_clang)]
(* doc only shows up in deprecation warnings *)
"use --capture and --linters instead" ~symbols:clang_frontend_action_symbols
@ -927,21 +927,21 @@ and cluster =
and compilation_database =
CLOpt.mk_path_list ~long:"compilation-database" ~deprecated:["-clang-compilation-db-files"]
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
"File that contain compilation commands (can be specified multiple times)"
and compilation_database_escaped =
CLOpt.mk_path_list ~long:"compilation-database-escaped"
~deprecated:["-clang-compilation-db-files-escaped"]
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
"File that contain compilation commands where all entries are escaped for the shell, eg \
coming from Xcode (can be specified multiple times)"
and compute_analytics =
CLOpt.mk_bool ~long:"compute-analytics" ~default:false
~in_help:InferCommand.([(Capture, manual_clang); (Run, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang); (Run, manual_clang)]
"Emit analytics as info-level issues, like component kit line count and component kit file \
cyclomatic complexity"
@ -950,14 +950,14 @@ and compute_analytics =
If a procedure was changed beforehand, keep the changed marking. *)
and continue =
CLOpt.mk_bool ~deprecated:["continue"] ~long:"continue"
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
"Continue the capture for the reactive analysis, increasing the changed files/procedures. (If \
a procedure was changed beforehand, keep the changed marking.)"
and current_to_previous_script =
CLOpt.mk_string_opt ~long:"current-to-previous-script"
~in_help:InferCommand.([(Diff, manual_generic)])
~in_help:InferCommand.[(Diff, manual_generic)]
~meta:"shell"
"Specify a script to checkout a previous version of the project to compare against, assuming \
we are on the current version already."
@ -965,7 +965,7 @@ and current_to_previous_script =
and cxx_infer_headers =
CLOpt.mk_bool ~long:"cxx-infer-headers" ~default:false
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
"Include C++ header models during compilation. Infer swaps some C++ headers for its own in \
order to get a better model of, eg, the standard library. This can sometimes cause \
compilation failures."
@ -973,14 +973,14 @@ and cxx_infer_headers =
and cxx_scope_guards =
CLOpt.mk_json ~long:"cxx-scope-guards"
~in_help:InferCommand.([(Analyze, manual_clang)])
~in_help:InferCommand.[(Analyze, manual_clang)]
"Specify scope guard classes that can be read only by destructors without being reported as \
dead stores."
and cxx =
CLOpt.mk_bool ~long:"cxx" ~default:true
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
"Analyze C++ methods"
@ -1012,7 +1012,7 @@ and ( bo_debug
in
let bo_debug =
CLOpt.mk_int ~default:0 ~long:"bo-debug"
~in_help:InferCommand.([(Analyze, manual_buffer_overrun)])
~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
"Debug level for buffer-overrun checker (0-4)"
and debug_level_analysis =
CLOpt.mk_int ~long:"debug-level-analysis" ~default:0 ~in_help:all_generic_manuals
@ -1030,7 +1030,7 @@ and ( bo_debug
"Show internal exceptions"
and filtering =
CLOpt.mk_bool ~deprecated_no:["nf"] ~long:"filtering" ~short:'f' ~default:true
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
"Do not show the experimental and blacklisted issue types"
and only_cheap_debug =
CLOpt.mk_bool ~long:"only-cheap-debug" ~default:true "Disable expensive debugging output"
@ -1041,7 +1041,7 @@ and ( bo_debug
CLOpt.mk_bool ~long:"print-types" ~default:false "Print types in symbolic heaps"
and keep_going =
CLOpt.mk_bool ~deprecated_no:["-no-failures-allowed"] ~long:"keep-going"
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
"Keep going when the analysis encounters a failure"
and reports_include_ml_loc =
CLOpt.mk_bool ~deprecated:["with_infer_src_loc"] ~long:"reports-include-ml-loc"
@ -1090,32 +1090,33 @@ and ( bo_debug
CLOpt.mk_bool_group ~long:"debug-exceptions"
"Generate lightweight debugging information: just print the internal exceptions during \
analysis (also sets $(b,--developer-mode), $(b,--no-filtering), $(b,--print-buckets), \
$(b,--reports-include-ml-loc))" [developer_mode; print_buckets; reports_include_ml_loc]
[filtering; keep_going]
$(b,--reports-include-ml-loc))"
[developer_mode; print_buckets; reports_include_ml_loc] [filtering; keep_going]
and default_linters =
CLOpt.mk_bool ~long:"default-linters"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
~default:true "Use the default linters for the analysis."
and frontend_tests =
CLOpt.mk_bool_group ~long:"frontend-tests"
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
"Save filename.ext.test.dot with the cfg in dotty format for frontend tests (also sets \
$(b,--print-types))" [print_types] []
$(b,--print-types))"
[print_types] []
and models_mode =
CLOpt.mk_bool_group ~long:"models-mode" "Mode for analyzing the models" [] [keep_going]
and print_logs =
CLOpt.mk_bool ~long:"print-logs"
~in_help:
InferCommand.(
InferCommand.
[ (Analyze, manual_generic)
; (Capture, manual_generic)
; (Run, manual_generic)
; (Report, manual_generic) ])
; (Report, manual_generic) ]
"Also log messages to stdout and stderr"
in
let linters_developer_mode =
CLOpt.mk_bool_group ~long:"linters-developer-mode"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
"Debug mode for developing new linters. (Sets the analyzer to $(b,linters); also sets \
$(b,--debug), $(b,--debug-level-linters 2), $(b,--developer-mode), and unsets \
$(b,--allowed-failures) and $(b,--default-linters)."
@ -1150,14 +1151,14 @@ and ( bo_debug
and dependencies =
CLOpt.mk_bool ~deprecated:["dependencies"] ~long:"dependencies"
~in_help:InferCommand.([(Capture, manual_java)])
~in_help:InferCommand.[(Capture, manual_java)]
"Translate all the dependencies during the capture. The classes in the given jar file will be \
translated. No sources needed."
and differential_filter_files =
CLOpt.mk_string_opt ~long:"differential-filter-files"
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
"Specify the file containing the list of source files for which a differential report is \
desired. Source files should be specified relative to project root or be absolute"
@ -1179,7 +1180,7 @@ and () =
let issue = IssueType.from_string issue_id in
IssueType.set_enabled issue b ; issue_id )
?default ~meta:"issue_type"
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
doc
in
()
@ -1196,10 +1197,8 @@ and () =
issue types. This option provides fine-grained filtering over which types of issue should \
be reported once the checkers have run. In particular, note that disabling issue types \
does not make the corresponding checker not run.\n \
By default, the following issue types are disabled: %s.\n\
\n \
See also $(b,--report-issue-type).\n\
"
By default, the following issue types are disabled: %s.\n\n \
See also $(b,--report-issue-type).\n"
(String.concat ~sep:", " disabled_issues_ids)) ;
mk true ~long:"enable-issue-type" ~deprecated:["enable_checks"; "-enable-checks"]
"Show reports coming from this type of issue. By default, all issue types are enabled except \
@ -1214,7 +1213,7 @@ and dotty_cfg_libs =
and dump_duplicate_symbols =
CLOpt.mk_bool ~long:"dump-duplicate-symbols"
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
"Dump all symbols with the same name that are defined in more than one file."
@ -1248,7 +1247,7 @@ and eradicate_verbose =
and external_java_packages =
CLOpt.mk_string_list ~long:"external-java-packages"
~in_help:InferCommand.([(Analyze, manual_java)])
~in_help:InferCommand.[(Analyze, manual_java)]
~meta:"prefix"
"Specify a list of Java package prefixes for external Java packages. If set, the analysis \
will not report non-actionable warnings on those packages."
@ -1256,7 +1255,7 @@ and external_java_packages =
and fail_on_bug =
CLOpt.mk_bool ~deprecated:["-fail-on-bug"] ~long:"fail-on-issue" ~default:false
~in_help:InferCommand.([(Run, manual_generic)])
~in_help:InferCommand.[(Run, manual_generic)]
(Printf.sprintf "Exit with error code %d if Infer found something to report"
fail_on_issue_exit_code)
@ -1269,7 +1268,7 @@ and fcp_syntax_only = CLOpt.mk_bool ~long:"fcp-syntax-only" "Skip creation of ob
and file_renamings =
CLOpt.mk_path_opt ~long:"file-renamings"
~in_help:InferCommand.([(ReportDiff, manual_generic)])
~in_help:InferCommand.[(ReportDiff, manual_generic)]
"JSON with a list of file renamings to use while computing differential reports"
@ -1279,7 +1278,7 @@ and filter_paths =
and filter_report =
CLOpt.mk_string_list ~long:"filter-report"
~in_help:InferCommand.([(Report, manual_generic); (Run, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic); (Run, manual_generic)]
"Specify a filter for issues to report. If multiple filters are specified, they are applied \
in the order in which they are specified. Each filter is applied to each issue detected, and \
only issues which are accepted by all filters are reported. Each filter is of the form: \
@ -1294,7 +1293,7 @@ and filter_report =
and flavors =
CLOpt.mk_bool ~deprecated:["-use-flavors"] ~long:"flavors"
~in_help:InferCommand.([(Capture, manual_buck_flavors)])
~in_help:InferCommand.[(Capture, manual_buck_flavors)]
"Buck integration using Buck flavors (clang only), eg $(i,`infer --flavors -- buck build \
//foo:bar#infer`)"
@ -1302,11 +1301,11 @@ and flavors =
and force_delete_results_dir =
CLOpt.mk_bool ~long:"force-delete-results-dir" ~default:false
~in_help:
InferCommand.(
InferCommand.
[ (Capture, manual_generic)
; (Compile, manual_generic)
; (Diff, manual_generic)
; (Run, manual_generic) ])
; (Run, manual_generic) ]
"Do not refuse to delete the results directory if it doesn't look like an infer results \
directory."
@ -1314,7 +1313,7 @@ and force_delete_results_dir =
and force_integration =
CLOpt.mk_symbol_opt ~long:"force-integration" ~meta:"command"
~symbols:(List.Assoc.inverse build_system_exe_assoc)
~in_help:InferCommand.([(Capture, manual_generic); (Run, manual_generic)])
~in_help:InferCommand.[(Capture, manual_generic); (Run, manual_generic)]
(Printf.sprintf
"Proceed as if the first argument after $(b,--) was $(i,command). Possible values: %s."
( List.map build_system_exe_assoc ~f:(fun (_, s) -> Printf.sprintf "$(i,%s)" s)
@ -1323,7 +1322,7 @@ and force_integration =
and from_json_report =
CLOpt.mk_path_opt ~long:"from-json-report"
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
~meta:"report.json"
"Load analysis results from a report file (default is to load the results from the specs \
files generated by the analysis)."
@ -1336,7 +1335,7 @@ and frontend_stats =
and gen_previous_build_command_script =
CLOpt.mk_string_opt ~long:"gen-previous-build-command-script"
~in_help:InferCommand.([(Diff, manual_generic)])
~in_help:InferCommand.[(Diff, manual_generic)]
~meta:"shell"
"Specify a script that outputs the build command to capture in the previous version of the \
project. The script should output the command on stdout. For example \"echo make\"."
@ -1344,13 +1343,13 @@ and gen_previous_build_command_script =
and generated_classes =
CLOpt.mk_path_opt ~long:"generated-classes"
~in_help:InferCommand.([(Capture, manual_java)])
~in_help:InferCommand.[(Capture, manual_java)]
"Specify where to load the generated class files"
and headers =
CLOpt.mk_bool ~deprecated:["headers"; "hd"] ~deprecated_no:["no_headers"; "nhd"] ~long:"headers"
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
"Analyze code in header files"
@ -1376,7 +1375,7 @@ and help_format =
and html =
CLOpt.mk_bool ~long:"html"
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Generate html report."
@ -1398,20 +1397,20 @@ and infer_cache =
and iphoneos_target_sdk_version =
CLOpt.mk_string_opt ~long:"iphoneos-target-sdk-version"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
"Specify the target SDK version to use for iphoneos"
and iphoneos_target_sdk_version_path_regex =
CLOpt.mk_string_list ~long:"iphoneos-target-sdk-version-path-regex"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
"To pass a specific target SDK version to use for iphoneos in a particular path, with the \
format path:version (can be specified multiple times)"
and issues_fields =
CLOpt.mk_symbol_seq ~long:"issues-fields"
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
~default:
[ `Issue_field_file
; `Issue_field_procedure
@ -1424,13 +1423,13 @@ and issues_fields =
and issues_tests =
CLOpt.mk_path_opt ~long:"issues-tests"
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
~meta:"file" "Write a list of issues in a format suitable for tests to $(i,file)"
and issues_txt =
CLOpt.mk_path_opt ~deprecated:["bugs_txt"] ~long:"issues-txt"
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
~meta:"file" "Write a list of issues in text format to $(i,file) (default: infer-out/bugs.txt)"
@ -1442,7 +1441,7 @@ and iterations =
and java_jar_compiler =
CLOpt.mk_path_opt ~long:"java-jar-compiler"
~in_help:InferCommand.([(Capture, manual_java)])
~in_help:InferCommand.[(Capture, manual_java)]
~meta:"path" "Specify the Java compiler jar used to generate the bytecode"
@ -1450,7 +1449,7 @@ and job_id = CLOpt.mk_string_opt ~long:"job-id" "Specify the job ID of this Infe
and jobs =
CLOpt.mk_int ~deprecated:["-multicore"] ~long:"jobs" ~short:'j' ~default:ncpu
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
~meta:"int" "Run the specified number of analysis jobs simultaneously"
@ -1464,7 +1463,7 @@ and join_cond =
and log_events =
CLOpt.mk_bool ~long:"log-events"
~in_help:InferCommand.([(Run, manual_generic)])
~in_help:InferCommand.[(Run, manual_generic)]
"Turn on the feature that logs events in a machine-readable format"
@ -1475,21 +1474,21 @@ and log_file =
and linter =
CLOpt.mk_string_opt ~long:"linter"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
"From the linters available, only run this one linter. (Useful together with \
$(b,--linters-developer-mode))"
and linters_def_file =
CLOpt.mk_path_list ~default:[] ~long:"linters-def-file"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
~meta:"file" "Specify the file containing linters definition (e.g. 'linters.al')"
and linters_def_folder =
let linters_def_folder =
CLOpt.mk_path_list ~default:[] ~long:"linters-def-folder"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
~meta:"dir" "Specify the folder containing linters files with extension .al"
in
let () =
@ -1502,7 +1501,7 @@ and linters_def_folder =
and linters_doc_url =
CLOpt.mk_string_list ~long:"linters-doc-url"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
"Specify custom documentation URL for some linter that overrides the default one. Useful if \
your project has specific ways of fixing a lint error that is not true in general or public \
info. Format: linter_name:doc_url."
@ -1510,20 +1509,20 @@ and linters_doc_url =
and linters_ignore_clang_failures =
CLOpt.mk_bool ~long:"linters-ignore-clang-failures"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
~default:false "Continue linting files even if some compilation fails."
and linters_validate_syntax_only =
CLOpt.mk_bool ~long:"linters-validate-syntax-only"
~in_help:InferCommand.([(Capture, manual_clang_linters)])
~in_help:InferCommand.[(Capture, manual_clang_linters)]
~default:false
"Validate syntax of AL files, then emit possible errors in JSON format to stdout"
and load_average =
CLOpt.mk_float_opt ~long:"load-average" ~short:'l'
~in_help:InferCommand.([(Capture, manual_generic)])
~in_help:InferCommand.[(Capture, manual_generic)]
~meta:"float"
"Do not start new parallel jobs if the load average is greater than that specified (Buck and \
make only)"
@ -1536,21 +1535,21 @@ and margin =
and max_nesting =
CLOpt.mk_int_opt ~long:"max-nesting"
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Level of nested procedure calls to show. Trace elements beyond the maximum nesting level are \
skipped. If omitted, all levels are shown."
and merge =
CLOpt.mk_bool ~deprecated:["merge"] ~long:"merge"
~in_help:InferCommand.([(Analyze, manual_buck_flavors)])
~in_help:InferCommand.[(Analyze, manual_buck_flavors)]
"Merge the captured results directories specified in the dependency file"
and ml_buckets =
CLOpt.mk_symbol_seq ~deprecated:["ml_buckets"; "-ml_buckets"] ~long:"ml-buckets"
~default:[`MLeak_cf]
~in_help:InferCommand.([(Analyze, manual_clang)])
~in_help:InferCommand.[(Analyze, manual_clang)]
{|Specify the memory leak buckets to be checked in C++:
- $(b,cpp) from C++ code
|}
@ -1579,7 +1578,7 @@ and only_footprint =
and only_show =
CLOpt.mk_bool ~long:"only-show"
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Show the list of reports and exit"
@ -1626,7 +1625,7 @@ and per_procedure_parallelism =
and pmd_xml =
CLOpt.mk_bool ~long:"pmd-xml"
~in_help:InferCommand.([(Run, manual_generic)])
~in_help:InferCommand.[(Run, manual_generic)]
"Output issues in (PMD) XML format"
@ -1637,7 +1636,7 @@ and precondition_stats =
and previous_to_current_script =
CLOpt.mk_string_opt ~long:"previous-to-current-script"
~in_help:InferCommand.([(Diff, manual_generic)])
~in_help:InferCommand.[(Diff, manual_generic)]
~meta:"shell"
"Specify a script to checkout the current version of the project. The project is supposed to \
already be at that current version when running $(b,infer diff); the script is used after \
@ -1647,7 +1646,7 @@ and previous_to_current_script =
and print_active_checkers =
CLOpt.mk_bool ~long:"print-active-checkers"
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
"Print the active checkers before starting the analysis"
@ -1658,7 +1657,7 @@ and print_builtins =
and print_log_identifier =
CLOpt.mk_bool ~long:"print-log-identifier"
~in_help:InferCommand.([(Run, manual_generic)])
~in_help:InferCommand.[(Run, manual_generic)]
"Print the unique identifier that is common to all logged events"
@ -1669,19 +1668,19 @@ and print_using_diff =
and procedures =
CLOpt.mk_bool ~long:"procedures"
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Print functions and methods discovered by infer"
and procedures_attributes =
CLOpt.mk_bool ~long:"procedures-attributes"
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Print the attributes of each procedure in the output of $(b,--procedures)"
and procedures_definedness =
CLOpt.mk_bool ~long:"procedures-definedness" ~default:true
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Include procedures definedness in the output of $(b,--procedures), i.e. whether the \
procedure definition was found, or only the procedure declaration, or the procedure is an \
auto-generated Objective-C accessor"
@ -1689,7 +1688,7 @@ and procedures_definedness =
and procedures_filter =
CLOpt.mk_string_opt ~long:"procedures-filter" ~meta:"filter"
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"With $(b,--procedures), only print functions and methods (procedures) matching the specified \
$(i,filter). A procedure filter is of the form $(i,path_pattern:procedure_name). Patterns \
are interpreted by SQLite: use $(b,_) to match any one character and $(b,%) to match any \
@ -1699,7 +1698,7 @@ and procedures_filter =
and procedures_name =
CLOpt.mk_bool ~long:"procedures-name"
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Include procedures names in the output of $(b,--procedures)"
@ -1712,7 +1711,7 @@ and procedures_per_process =
and procedures_source_file =
CLOpt.mk_bool ~long:"procedures-source-file" ~default:true
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Include the source file in which the procedure definition or declaration was found in the \
output of $(b,--procedures)"
@ -1725,7 +1724,7 @@ and procs_csv =
and progress_bar =
CLOpt.mk_bool ~deprecated:["pb"] ~deprecated_no:["no_progress_bar"; "npb"] ~short:'p'
~long:"progress-bar" ~default:true
~in_help:InferCommand.([(Run, manual_generic)])
~in_help:InferCommand.[(Run, manual_generic)]
"Show a progress bar"
@ -1733,41 +1732,41 @@ and project_root =
CLOpt.mk_path ~deprecated:["project_root"; "-project_root"; "pr"] ~long:"project-root" ~short:'C'
~default:CLOpt.init_work_dir
~in_help:
InferCommand.(
InferCommand.
[ (Analyze, manual_generic)
; (Capture, manual_generic)
; (Run, manual_generic)
; (Report, manual_generic) ])
; (Report, manual_generic) ]
~meta:"dir" "Specify the root directory of the project"
and quandary_endpoints =
CLOpt.mk_json ~long:"quandary-endpoints"
~in_help:InferCommand.([(Analyze, manual_quandary)])
~in_help:InferCommand.[(Analyze, manual_quandary)]
"Specify endpoint classes for Quandary"
and quandary_sanitizers =
CLOpt.mk_json ~long:"quandary-sanitizers"
~in_help:InferCommand.([(Analyze, manual_quandary)])
~in_help:InferCommand.[(Analyze, manual_quandary)]
"Specify custom sanitizers for Quandary"
and quandary_sources =
CLOpt.mk_json ~long:"quandary-sources"
~in_help:InferCommand.([(Analyze, manual_quandary)])
~in_help:InferCommand.[(Analyze, manual_quandary)]
"Specify custom sources for Quandary"
and quandary_sinks =
CLOpt.mk_json ~long:"quandary-sinks"
~in_help:InferCommand.([(Analyze, manual_quandary)])
~in_help:InferCommand.[(Analyze, manual_quandary)]
"Specify custom sinks for Quandary"
and quiet =
CLOpt.mk_bool ~long:"quiet" ~short:'q' ~default:false
~in_help:InferCommand.([(Analyze, manual_generic); (Report, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic); (Report, manual_generic)]
"Do not print specs on standard output (default: only print for the $(b,report) command)"
@ -1778,7 +1777,7 @@ and racerd_use_path_stability =
and reactive =
CLOpt.mk_bool ~deprecated:["reactive"] ~long:"reactive" ~short:'r'
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
"Reactive mode: the analysis starts from the files captured since the $(i,infer) command \
started"
@ -1790,13 +1789,13 @@ and reactive_capture =
and report =
CLOpt.mk_bool ~long:"report" ~default:true
~in_help:InferCommand.([(Analyze, manual_generic); (Run, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic); (Run, manual_generic)]
"Run the reporting phase once the analysis has completed"
and report_current =
CLOpt.mk_path_opt ~long:"report-current"
~in_help:InferCommand.([(ReportDiff, manual_generic)])
~in_help:InferCommand.[(ReportDiff, manual_generic)]
"report of the latest revision"
@ -1804,7 +1803,7 @@ and report_custom_error = CLOpt.mk_bool ~long:"report-custom-error" ""
and report_formatter =
CLOpt.mk_symbol ~long:"report-formatter"
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
~default:`Phabricator_formatter
~symbols:[("none", `No_formatter); ("phabricator", `Phabricator_formatter)]
~eq:PolyVariantEqual.( = ) "Which formatter to use when emitting the report"
@ -1812,7 +1811,7 @@ and report_formatter =
and report_hook =
CLOpt.mk_string_opt ~long:"report-hook"
~in_help:InferCommand.([(Analyze, manual_generic); (Run, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic); (Run, manual_generic)]
~default:(lib_dir ^/ "python" ^/ "report.py")
~meta:"script"
"Specify a script to be executed after the analysis results are written. This script will be \
@ -1822,13 +1821,13 @@ and report_hook =
and report_previous =
CLOpt.mk_path_opt ~long:"report-previous"
~in_help:InferCommand.([(ReportDiff, manual_generic)])
~in_help:InferCommand.[(ReportDiff, manual_generic)]
"Report of the base revision to use for comparison"
and rest =
CLOpt.mk_rest_actions
~in_help:InferCommand.([(Capture, manual_generic); (Run, manual_generic)])
~in_help:InferCommand.[(Capture, manual_generic); (Run, manual_generic)]
"Stop argument processing, use remaining arguments as a build command" ~usage:exe_usage
(fun build_exe ->
match Filename.basename build_exe with "java" | "javac" -> CLOpt.Javac | _ -> CLOpt.NoParse
@ -1839,12 +1838,12 @@ and results_dir =
CLOpt.mk_path ~deprecated:["results_dir"; "-out"] ~long:"results-dir" ~short:'o'
~default:(CLOpt.init_work_dir ^/ "infer-out")
~in_help:
InferCommand.(
InferCommand.
[ (Analyze, manual_generic)
; (Capture, manual_generic)
; (Explore, manual_generic)
; (Run, manual_generic)
; (Report, manual_generic) ])
; (Report, manual_generic) ]
~meta:"dir" "Write results and internal files in the specified directory"
@ -1855,45 +1854,45 @@ and seconds_per_iteration =
and select =
CLOpt.mk_int_opt ~long:"select" ~meta:"N"
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"Select bug number $(i,N). If omitted, prompt for input."
and siof_safe_methods =
CLOpt.mk_string_list ~long:"siof-safe-methods"
~in_help:InferCommand.([(Analyze, manual_siof)])
~in_help:InferCommand.[(Analyze, manual_siof)]
"Methods that are SIOF-safe; \"foo::bar\" will match \"foo::bar()\", \"foo<int>::bar()\", \
etc. (can be specified multiple times)"
and skip_analysis_in_path =
CLOpt.mk_string_list ~deprecated:["-skip-clang-analysis-in-path"] ~long:"skip-analysis-in-path"
~in_help:InferCommand.([(Capture, manual_generic); (Run, manual_generic)])
~in_help:InferCommand.[(Capture, manual_generic); (Run, manual_generic)]
~meta:"path_prefix_OCaml_regex"
"Ignore files whose path matches the given prefix (can be specified multiple times)"
and skip_analysis_in_path_skips_compilation =
CLOpt.mk_bool ~long:"skip-analysis-in-path-skips-compilation"
~in_help:InferCommand.([(Report, manual_generic)])
~in_help:InferCommand.[(Report, manual_generic)]
~default:false "Whether paths in --skip-analysis-in-path should be compiled or not"
and skip_duplicated_types =
CLOpt.mk_bool ~long:"skip-duplicated-types" ~default:true
~in_help:InferCommand.([(ReportDiff, manual_generic)])
~in_help:InferCommand.[(ReportDiff, manual_generic)]
"Skip fixed-then-introduced duplicated types while computing differential reports"
and skip_translation_headers =
CLOpt.mk_string_list ~deprecated:["skip_translation_headers"] ~long:"skip-translation-headers"
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
~meta:"path_prefix" "Ignore headers whose path matches the given prefix"
and source_preview =
CLOpt.mk_bool ~long:"source-preview" ~default:true
~in_help:InferCommand.([(Explore, manual_generic)])
~in_help:InferCommand.[(Explore, manual_generic)]
"print code excerpts around trace elements"
@ -1931,7 +1930,7 @@ and specs_library =
~f:(fun file ->
specs_library := read_specs_dir_list_file file @ !specs_library ;
"" )
~in_help:InferCommand.([(Analyze, manual_generic)])
~in_help:InferCommand.[(Analyze, manual_generic)]
~meta:"file" ""
in
specs_library
@ -1952,7 +1951,7 @@ and sqlite_vfs =
and stacktrace =
CLOpt.mk_path_opt ~deprecated:["st"] ~long:"stacktrace"
~in_help:InferCommand.([(Analyze, manual_crashcontext)])
~in_help:InferCommand.[(Analyze, manual_crashcontext)]
~meta:"file"
"File path containing a json-encoded Java crash stacktrace. Used to guide the analysis (only \
with '-a crashcontext'). See tests/codetoanalyze/java/crashcontext/*.json for examples of \
@ -1961,7 +1960,7 @@ and stacktrace =
and stacktraces_dir =
CLOpt.mk_path_opt ~long:"stacktraces-dir"
~in_help:InferCommand.([(Analyze, manual_crashcontext)])
~in_help:InferCommand.[(Analyze, manual_crashcontext)]
~meta:"dir"
"Directory path containing multiple json-encoded Java crash stacktraces. Used to guide the \
analysis (only with '-a crashcontext'). See tests/codetoanalyze/java/crashcontext/*.json \
@ -1996,7 +1995,7 @@ and testing_mode =
and threadsafe_aliases =
CLOpt.mk_json ~long:"threadsafe-aliases"
~in_help:InferCommand.([(Analyze, manual_racerd)])
~in_help:InferCommand.[(Analyze, manual_racerd)]
"Specify custom annotations that should be considered aliases of @ThreadSafe"
@ -2044,17 +2043,17 @@ and uninit_interproc =
and unsafe_malloc =
CLOpt.mk_bool ~long:"unsafe-malloc"
~in_help:InferCommand.([(Analyze, manual_clang)])
~in_help:InferCommand.[(Analyze, manual_clang)]
"Assume that malloc(3) never returns null."
and version =
let var = ref `None in
CLOpt.mk_set var `Full ~deprecated:["version"] ~long:"version"
~in_help:InferCommand.([(Run, manual_generic)])
~in_help:InferCommand.[(Run, manual_generic)]
"Print version information and exit" ;
CLOpt.mk_set var `Json ~deprecated:["version_json"] ~long:"version-json"
~in_help:InferCommand.([(Run, manual_generic)])
~in_help:InferCommand.[(Run, manual_generic)]
"Print version information in json format and exit" ;
CLOpt.mk_set var `Vcs ~long:"version-vcs" "Print version control system commit and exit" ;
var
@ -2076,13 +2075,13 @@ and worklist_mode =
and xcode_developer_dir =
CLOpt.mk_path_opt ~long:"xcode-developer-dir"
~in_help:InferCommand.([(Capture, manual_buck_flavors)])
~in_help:InferCommand.[(Capture, manual_buck_flavors)]
~meta:"XCODE_DEVELOPER_DIR" "Specify the path to Xcode developer directory"
and xcpretty =
CLOpt.mk_bool ~long:"xcpretty" ~default:false
~in_help:InferCommand.([(Capture, manual_clang)])
~in_help:InferCommand.[(Capture, manual_clang)]
"Infer will use xcpretty together with xcodebuild to analyze an iOS app. xcpretty just needs \
to be in the path, infer command is still just $(i,`infer -- <xcodebuild command>`)."
@ -2258,9 +2257,9 @@ let post_parsing_initialization command_opt =
in
if is_none !symops_per_iteration then symops_per_iteration := symops_timeout ;
if is_none !seconds_per_iteration then seconds_per_iteration := seconds_timeout ;
clang_compilation_dbs
:= List.rev_map ~f:(fun x -> `Raw x) !compilation_database
|> List.rev_map_append ~f:(fun x -> `Escaped x) !compilation_database_escaped ;
clang_compilation_dbs :=
List.rev_map ~f:(fun x -> `Raw x) !compilation_database
|> List.rev_map_append ~f:(fun x -> `Escaped x) !compilation_database_escaped ;
(* set analyzer mode to linters in linters developer mode *)
if !linters_developer_mode then linters := true ;
if !default_linters then linters_def_file := linters_def_default_file :: !linters_def_file ;
@ -2305,7 +2304,8 @@ let process_iphoneos_target_sdk_version_path_regex args =
| None ->
L.(die UserError)
"Incorrect format for the option iphoneos-target-sdk_version-path-regex. The correct \
format is path:version but got %s" arg
format is path:version but got %s"
arg
in
List.map ~f:process_iphoneos_target_sdk_version_path_regex args
@ -2320,7 +2320,8 @@ let process_linters_doc_url args =
| None ->
L.(die UserError)
"Incorrect format for the option linters-doc-url. The correct format is linter:doc_url \
but got %s" arg
but got %s"
arg
in
List.map ~f:linters_doc_url args
@ -2825,7 +2826,7 @@ let dynamic_dispatch =
a call to unknown code and true triggers lazy dynamic dispatch. The latter mode follows the \
JVM semantics and creates procedure descriptions during symbolic execution using the type \
information found in the abstract state"
~in_help:InferCommand.([(Analyze, manual_java)])
~in_help:InferCommand.[(Analyze, manual_java)]
let dynamic_dispatch = !dynamic_dispatch

13
infer/src/base/Config.mli
Unescape View File

@ -14,13 +14,8 @@ module CLOpt = CommandLineOption
(** Configuration values: either constant, determined at compile time, or set at startup
time by system calls, environment variables, or command line options *)
type analyzer =
| CaptureOnly
| CompileOnly
| Checkers
| Crashcontext
| Linters
[@@deriving compare]
type analyzer = CaptureOnly | CompileOnly | Checkers | Crashcontext | Linters
[@@deriving compare]
val equal_analyzer : analyzer -> analyzer -> bool
@ -36,7 +31,7 @@ type compilation_database_dependencies =
(** get the compilation database of the dependencies up to depth n
by [Deps (Some n)], or all by [Deps None] *)
| NoDeps
[@@deriving compare]
[@@deriving compare]
type build_system =
| BAnalyze
@ -51,7 +46,7 @@ type build_system =
| BNdk
| BPython
| BXcode
[@@deriving compare]
[@@deriving compare]
val equal_build_system : build_system -> build_system -> bool

6
infer/src/base/DB.ml
Unescape View File

@ -117,7 +117,7 @@ let update_file_with_lock dir fname update =
in
Utils.create_dir dir ;
let path = Filename.concat dir fname in
let fd = Unix.openfile path ~mode:Unix.([O_CREAT; O_SYNC; O_RDWR]) ~perm:0o640 in
let fd = Unix.openfile path ~mode:Unix.[O_CREAT; O_SYNC; O_RDWR] ~perm:0o640 in
Unix.lockf fd ~mode:Unix.F_LOCK ~len:0L ;
let buf = read_whole_file fd in
reset_file fd ;
@ -135,7 +135,7 @@ let update_file_with_lock dir fname update =
let read_file_with_lock dir fname =
let path = Filename.concat dir fname in
try
let fd = Unix.openfile path ~mode:Unix.([O_RSYNC; O_RDONLY]) ~perm:0o646 in
let fd = Unix.openfile path ~mode:Unix.[O_RSYNC; O_RDONLY] ~perm:0o646 in
try
Unix.lockf fd ~mode:Unix.F_RLOCK ~len:0L ;
let buf = read_whole_file fd in
@ -223,7 +223,7 @@ module Results_dir = struct
L.(die InternalError) "create_path"
in
let full_fname = Filename.concat (create dir_path) filename in
Unix.openfile full_fname ~mode:Unix.([O_WRONLY; O_CREAT; O_TRUNC]) ~perm:0o777
Unix.openfile full_fname ~mode:Unix.[O_WRONLY; O_CREAT; O_TRUNC] ~perm:0o777
end
let is_source_file path =

7
infer/src/base/IssueType.ml
Unescape View File

@ -11,9 +11,8 @@ open! IStd
(* Make sure we cannot create new issue types other than by calling [from_string]. This is because
we want to keep track of the list of all the issues ever declared. *)
module Unsafe : sig
type t = private
{unique_id: string; mutable enabled: bool; mutable hum: string}
[@@deriving compare]
type t = private {unique_id: string; mutable enabled: bool; mutable hum: string}
[@@deriving compare]
val equal : t -> t -> bool
@ -63,7 +62,7 @@ end = struct
value of enabled (see doc comment) *)
if Option.is_some hum0 then old.hum <- hum ;
old
with Not_found ->
with Caml.Not_found ->
all_issues := IssueSet.add issue !all_issues ;
issue

5
infer/src/base/IssueType.mli
Unescape View File

@ -10,9 +10,8 @@
open! IStd
(** type of string used for localisation *)
type t = private
{unique_id: string; mutable enabled: bool; mutable hum: string}
[@@deriving compare]
type t = private {unique_id: string; mutable enabled: bool; mutable hum: string}
[@@deriving compare]
val equal : t -> t -> bool

2
infer/src/base/Location.ml
Unescape View File

@ -15,7 +15,7 @@ type t =
{ line: int (** The line number. -1 means "do not know" *)
; col: int (** The column number. -1 means "do not know" *)
; file: SourceFile.t (** The name of the source file *) }
[@@deriving compare]
[@@deriving compare]
let equal = [%compare.equal : t]

2
infer/src/base/Location.mli
Unescape View File

@ -14,7 +14,7 @@ type t =
{ line: int (** The line number. -1 means "do not know" *)
; col: int (** The column number. -1 means "do not know" *)
; file: SourceFile.t (** The name of the source file *) }
[@@deriving compare]
[@@deriving compare]
val equal : t -> t -> bool

2
infer/src/base/Logging.mli
Unescape View File

@ -67,7 +67,7 @@ val debug_dev : ('a, Format.formatter, unit) format -> 'a
[@@deprecated
"Only use to debug during development. If you want more permanent logging, use \
[Logging.debug] instead."]
[@@warning "-32"]
[@@warning "-32"]
(** For debugging during development. *)
(** Type of location in ml source: __POS__ *)

8
infer/src/base/Multilinks.ml
Unescape View File

@ -50,7 +50,9 @@ let write multilinks ~dir =
let lookup ~dir =
try Some (String.Table.find_exn multilink_files_cache dir) with Not_found -> read ~dir
try Some (String.Table.find_exn multilink_files_cache dir) with
| Not_found_s _ | Caml.Not_found ->
read ~dir
let resolve fname =
@ -63,4 +65,6 @@ let resolve fname =
| None ->
fname
| Some links ->
try DB.filename_from_string (String.Table.find_exn links base) with Not_found -> fname
try DB.filename_from_string (String.Table.find_exn links base) with
| Not_found_s _ | Caml.Not_found ->
fname

14
infer/src/base/ResultsDir.ml
Unescape View File

@ -19,12 +19,12 @@ let is_results_dir ~check_correct_version () =
List.for_all results_dir_dir_markers ~f:(fun d ->
Sys.is_directory d = `Yes
||
(not_found := d ^ "/" ;
false) )
( not_found := d ^ "/" ;
false ) )
&& ( not check_correct_version || Sys.is_file ResultsDatabase.database_fullpath = `Yes
||
(not_found := ResultsDatabase.database_fullpath ;
false) )
( not_found := ResultsDatabase.database_fullpath ;
false ) )
in
Result.ok_if_true has_all_markers ~error:(Printf.sprintf "'%s' not found" !not_found)
@ -42,8 +42,8 @@ let remove_results_dir () =
Result.iter_error (is_results_dir ~check_correct_version:false ()) ~f:(fun err ->
L.(die UserError)
"ERROR: '%s' exists but does not seem to be an infer results directory: %s@\n\
ERROR: Please delete '%s' and try again@." Config.results_dir err Config.results_dir
) ;
ERROR: Please delete '%s' and try again@."
Config.results_dir err Config.results_dir ) ;
Utils.rmtree Config.results_dir ) ;
RunState.reset ()
@ -85,7 +85,7 @@ let assert_results_dir advice =
let delete_capture_and_analysis_data () =
ResultsDatabase.reset_capture_tables () ;
let dirs_to_delete =
List.map ~f:(Filename.concat Config.results_dir) Config.([captured_dir_name; specs_dir_name])
List.map ~f:(Filename.concat Config.results_dir) Config.[captured_dir_name; specs_dir_name]
in
List.iter ~f:Utils.rmtree dirs_to_delete ;
List.iter ~f:Unix.mkdir_p dirs_to_delete ;

13
infer/src/base/RunState.ml
Unescape View File

@ -27,7 +27,7 @@ let add_run_to_sequence () =
; date= run_time_string
; command= Config.command }
in
Runstate_t.(state := {(!state) with run_sequence= run :: !state.run_sequence})
Runstate_t.(state := {!state with run_sequence= run :: !state.run_sequence})
let state_filename = ".infer_runstate.json"
@ -47,17 +47,18 @@ let load_and_validate () =
(Printf.sprintf
"Incompatible results directory '%s':\n\
%s\n\
Was '%s' created using an older version of infer?" Config.results_dir err_msg
Config.results_dir) )
Was '%s' created using an older version of infer?"
Config.results_dir err_msg Config.results_dir) )
msg
in
if Sys.file_exists state_file_path <> `Yes then error "save state not found"
else
try
let loaded_state = Ag_util.Json.from_file Runstate_j.read_t state_file_path in
if not
(String.equal !state.Runstate_t.results_dir_format
loaded_state.Runstate_t.results_dir_format)
if
not
(String.equal !state.Runstate_t.results_dir_format
loaded_state.Runstate_t.results_dir_format)
then
error "Incompatible formats: found\n %s\n\nbut expected this format:\n %s\n\n"
loaded_state.results_dir_format !state.Runstate_t.results_dir_format

8
infer/src/base/Serialization.ml
Unescape View File

@ -35,14 +35,14 @@ let create_serializer (key: Key.t) : 'a serializer =
if key <> key' then (
L.user_error
"Wrong key in when loading data from %s -- are you running infer with results coming from \
a previous version of infer?@\n\
" source_msg ;
a previous version of infer?@\n"
source_msg ;
None )
else if version <> version' then (
L.user_error
"Wrong version in when loading data from %s -- are you running infer with results coming \
from a previous version of infer?@\n\
" source_msg ;
from a previous version of infer?@\n"
source_msg ;
None )
else Some value
in

11
infer/src/base/SourceFile.ml
Unescape View File

@ -24,7 +24,7 @@ type t =
(* relative to project root *)
| RelativeInferModel of string
(* relative to infer models *)
[@@deriving compare]
[@@deriving compare]
let equal = [%compare.equal : t]
@ -135,10 +135,11 @@ let is_under_project_root = function
let exists_cache = String.Table.create ~size:256 ()
let path_exists abs_path =
try String.Table.find_exn exists_cache abs_path with Not_found ->
let result = Sys.file_exists abs_path = `Yes in
String.Table.set exists_cache ~key:abs_path ~data:result ;
result
try String.Table.find_exn exists_cache abs_path with
| Not_found_s _ | Caml.Not_found ->
let result = Sys.file_exists abs_path = `Yes in
String.Table.set exists_cache ~key:abs_path ~data:result ;
result
let of_header ?(warn_on_error= true) header_file =

11
infer/src/base/Utils.ml
Unescape View File

@ -260,7 +260,7 @@ let realpath_cache = Hashtbl.create 1023
let realpath ?(warn_on_error= true) path =
match Hashtbl.find realpath_cache path with
| exception Not_found -> (
| exception Caml.Not_found -> (
match Filename.realpath path with
| realpath ->
Hashtbl.add realpath_cache path (Ok realpath) ;
@ -303,7 +303,7 @@ let compare_versions v1 v2 =
let write_file_with_locking ?(delete= false) ~f:do_write fname =
Unix.with_file
~mode:Unix.([O_WRONLY; O_CREAT])
~mode:Unix.[O_WRONLY; O_CREAT]
fname
~f:(fun file_descr ->
if Unix.flock file_descr Unix.Flock_command.lock_exclusive then (
@ -326,9 +326,10 @@ let rec rmtree name =
let rec rmdir dir =
match Unix.readdir_opt dir with
| Some entry ->
if not
( String.equal entry Filename.current_dir_name
|| String.equal entry Filename.parent_dir_name )
if
not
( String.equal entry Filename.current_dir_name
|| String.equal entry Filename.parent_dir_name )
then rmtree (name ^/ entry) ;
rmdir dir
| None ->

4
infer/src/base/ZipLib.ml
Unescape View File

@ -35,7 +35,7 @@ let load_from_cache serializer zip_path cache_dir zip_library =
Some data
| None ->
None
| exception Not_found ->
| exception Caml.Not_found ->
None
@ -47,7 +47,7 @@ let load_from_zip serializer zip_path zip_library =
Some data
| None ->
None
| exception Not_found ->
| exception Caml.Not_found ->
None

34
infer/src/biabduction/Abs.ml
Unescape View File

@ -22,7 +22,7 @@ type rule =
; r_root: Match.hpred_pat
; r_sigma: Match.hpred_pat list
; (* sigma should be in a specific order *)
r_new_sigma: Sil.hpred list
r_new_sigma: Sil.hpred list
; r_new_pi: Prop.normal Prop.t -> Prop.normal Prop.t -> Sil.exp_subst -> Sil.atom list
; r_condition: Prop.normal Prop.t -> Sil.exp_subst -> bool }
@ -65,7 +65,7 @@ let create_condition_ls ids_private id_base p_leftover (inst: Sil.exp_subst) =
let inst_private, inst_public = Sil.sub_domain_partition f inst in
let insts_of_public_ids = Sil.sub_range inst_public in
let inst_of_base =
try Sil.sub_find (Ident.equal id_base) inst_public with Not_found -> assert false
try Sil.sub_find (Ident.equal id_base) inst_public with Caml.Not_found -> assert false
in
let insts_of_private_ids = Sil.sub_range inst_private in
(insts_of_private_ids, insts_of_public_ids, inst_of_base)
@ -550,9 +550,9 @@ let discover_para_candidates tenv p =
let rec get_edges_sigma = function
| [] ->
()
| (Sil.Hlseg _) :: sigma_rest | (Sil.Hdllseg _) :: sigma_rest ->
| Sil.Hlseg _ :: sigma_rest | Sil.Hdllseg _ :: sigma_rest ->
get_edges_sigma sigma_rest
| (Sil.Hpointsto (root, se, te)) :: sigma_rest ->
| Sil.Hpointsto (root, se, te) :: sigma_rest ->
let rec_flds = typ_get_recursive_flds tenv te in
get_edges_strexp rec_flds root se ; get_edges_sigma sigma_rest
in
@ -600,9 +600,9 @@ let discover_para_dll_candidates tenv p =
let rec get_edges_sigma = function
| [] ->
()
| (Sil.Hlseg _) :: sigma_rest | (Sil.Hdllseg _) :: sigma_rest ->
| Sil.Hlseg _ :: sigma_rest | Sil.Hdllseg _ :: sigma_rest ->
get_edges_sigma sigma_rest
| (Sil.Hpointsto (root, se, te)) :: sigma_rest ->
| Sil.Hpointsto (root, se, te) :: sigma_rest ->
let rec_flds = typ_get_recursive_flds tenv te in
get_edges_strexp rec_flds root se ; get_edges_sigma sigma_rest
in
@ -877,15 +877,15 @@ let abstract_pure_part tenv p ~(from_abstract_footprint: bool) =
~f:(fun pi a ->
match a with
(* we only use Lt and Le because Gt and Ge are inserted in terms of Lt and Le. *)
| Sil.Aeq (Exp.Const Const.Cint i, Exp.BinOp (Binop.Lt, _, _))
| Sil.Aeq (Exp.BinOp (Binop.Lt, _, _), Exp.Const Const.Cint i)
| Sil.Aeq (Exp.Const Const.Cint i, Exp.BinOp (Binop.Le, _, _))
| Sil.Aeq (Exp.BinOp (Binop.Le, _, _), Exp.Const Const.Cint i)
| Sil.Aeq (Exp.Const (Const.Cint i), Exp.BinOp (Binop.Lt, _, _))
| Sil.Aeq (Exp.BinOp (Binop.Lt, _, _), Exp.Const (Const.Cint i))
| Sil.Aeq (Exp.Const (Const.Cint i), Exp.BinOp (Binop.Le, _, _))
| Sil.Aeq (Exp.BinOp (Binop.Le, _, _), Exp.Const (Const.Cint i))
when IntLit.isone i ->
a :: pi
| Sil.Aeq (Exp.Var name, e) when not (Ident.is_primed name) -> (
match e with Exp.Var _ | Exp.Const _ -> a :: pi | _ -> pi )
| Sil.Aneq (Var _, _) | Sil.Apred (_, (Var _) :: _) | Anpred (_, (Var _) :: _) ->
| Sil.Aneq (Var _, _) | Sil.Apred (_, Var _ :: _) | Anpred (_, Var _ :: _) ->
a :: pi
| Sil.Aeq _ | Aneq _ | Apred _ | Anpred _ ->
pi )
@ -982,14 +982,14 @@ let sigma_reachable root_fav sigma =
let check_observer_is_unsubscribed_deallocation tenv prop e =
let pvar_opt =
match Attribute.get_resource tenv prop e with
| Some Apred (Aresource {ra_vpath= Some Dpvar pvar}, _) ->
| Some (Apred (Aresource {ra_vpath= Some (Dpvar pvar)}, _)) ->
Some pvar
| _ ->
None
in
let loc = State.get_loc () in
match Attribute.get_observer tenv prop e with
| Some Apred (Aobserver, _) -> (
| Some (Apred (Aobserver, _)) -> (
match pvar_opt with
| Some pvar when Config.nsnotification_center_checker_backend ->
L.d_strln
@ -1043,19 +1043,19 @@ let check_junk pname tenv prop =
let do_entry e =
check_observer_is_unsubscribed_deallocation tenv prop e ;
match Attribute.get_wontleak tenv prop e with
| Some Apred ((Awont_leak as a), _) ->
| Some (Apred ((Awont_leak as a), _)) ->
L.d_strln "WONT_LEAK" ;
res := Some a
| _ ->
match Attribute.get_resource tenv prop e with
| Some Apred ((Aresource {ra_kind= Racquire} as a), _) ->
| Some (Apred ((Aresource {ra_kind= Racquire} as a), _)) ->
L.d_str "ATTRIBUTE: " ;
PredSymb.d_attribute a ;
L.d_ln () ;
res := Some a
| _ ->
match Attribute.get_undef tenv prop e with
| Some Apred ((Aundef _ as a), _) ->
| Some (Apred ((Aundef _ as a), _)) ->
L.d_strln "UNDEF" ;
res := Some a
| _ ->
@ -1123,7 +1123,7 @@ let check_junk pname tenv prop =
| Some _, None | None, Some _ ->
false
in
is_none alloc_attribute && !leaks_reported <> []
(is_none alloc_attribute && !leaks_reported <> [])
|| (* None attribute only reported if it's the first one *)
List.mem ~equal:attr_opt_equal !leaks_reported alloc_attribute
in

24
infer/src/biabduction/Absarray.ml
Unescape View File

@ -77,7 +77,7 @@ end = struct
match (se, t.desc, syn_offs) with
| _, _, [] ->
(se, t)
| Sil.Estruct (fsel, _), Tstruct name, (Field (fld, _)) :: syn_offs' -> (
| Sil.Estruct (fsel, _), Tstruct name, Field (fld, _) :: syn_offs' -> (
match Tenv.lookup tenv name with
| Some {fields} ->
let se' = snd (List.find_exn ~f:(fun (f', _) -> Typ.Fieldname.equal f' fld) fsel) in
@ -85,7 +85,7 @@ end = struct
get_strexp_at_syn_offsets tenv se' t' syn_offs'
| None ->
fail () )
| Sil.Earray (_, esel, _), Typ.Tarray {elt= t'}, (Index ind) :: syn_offs' ->
| Sil.Earray (_, esel, _), Typ.Tarray {elt= t'}, Index ind :: syn_offs' ->
let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' ind) esel) in
get_strexp_at_syn_offsets tenv se' t' syn_offs'
| _ ->
@ -97,7 +97,7 @@ end = struct
match (se, t.desc, syn_offs) with
| _, _, [] ->
update se
| Sil.Estruct (fsel, inst), Tstruct name, (Field (fld, _)) :: syn_offs' -> (
| Sil.Estruct (fsel, inst), Tstruct name, Field (fld, _) :: syn_offs' -> (
match Tenv.lookup tenv name with
| Some {fields} ->
let se' = snd (List.find_exn ~f:(fun (f', _) -> Typ.Fieldname.equal f' fld) fsel) in
@ -115,7 +115,7 @@ end = struct
Sil.Estruct (fsel', inst)
| None ->
assert false )
| Sil.Earray (len, esel, inst), Tarray {elt= t'}, (Index idx) :: syn_offs' ->
| Sil.Earray (len, esel, inst), Tarray {elt= t'}, Index idx :: syn_offs' ->
let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' idx) esel) in
let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in
let esel' =
@ -131,10 +131,10 @@ end = struct
let rec convert acc = function
| [] ->
acc
| (Field (f, t)) :: syn_offs' ->
| Field (f, t) :: syn_offs' ->
let acc' = List.map ~f:(fun e -> Exp.Lfield (e, f, t)) acc in
convert acc' syn_offs'
| (Index idx) :: syn_offs' ->
| Index idx :: syn_offs' ->
let acc' = List.map ~f:(fun e -> Exp.Lindex (e, idx)) acc in
convert acc' syn_offs'
in
@ -354,7 +354,7 @@ let generic_strexp_abstract tenv (abstraction_name: string) (p_in: Prop.normal P
let match_select_next (matchings_cur, matchings_fp) =
match (matchings_cur, matchings_fp) with
| [], [] ->
raise Not_found
raise Caml.Not_found
| matched :: cur', fp' ->
(matched, false, (cur', fp'))
| [], matched :: fp' ->
@ -368,7 +368,7 @@ let generic_strexp_abstract tenv (abstraction_name: string) (p_in: Prop.normal P
let strexp_data = StrexpMatch.get_data tenv matched in
let p1, changed = do_abstract footprint_part p0 strexp_data in
if changed then (p1, true) else match_abstract p0 matchings_cur_fp'
with Not_found -> (p0, false)
with Caml.Not_found -> (p0, false)
in
let rec find_then_abstract bound p0 =
if Int.equal bound 0 then p0
@ -423,7 +423,7 @@ let blur_array_index tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (inde
let sigma_fp' = StrexpMatch.replace_index tenv true matched_fp index fresh_index in
Prop.set p ~sigma_fp:sigma_fp'
else Prop.expose p
with Not_found -> Prop.expose p
with Caml.Not_found -> Prop.expose p
in
let p3 =
let matched = StrexpMatch.find_path p.Prop.sigma path in
@ -437,7 +437,7 @@ let blur_array_index tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (inde
prop_replace_path_index tenv p3 path map
in
Prop.normalize tenv p4
with Not_found -> p
with Caml.Not_found -> p
(** Given [p] containing an array at [root], blur [indices] in it *)
@ -466,7 +466,7 @@ let keep_only_indices tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (ind
(sigma', true)
| _ ->
(sigma, false)
with Not_found -> (sigma, false)
with Caml.Not_found -> (sigma, false)
in
prop_update_sigma_and_fp_sigma tenv p prune_sigma
@ -658,7 +658,7 @@ let remove_redundant_elements tenv prop =
false
in
match (e, se) with
| Exp.Const Const.Cint i, Sil.Eexp (Exp.Var id, _)
| Exp.Const (Const.Cint i), Sil.Eexp (Exp.Var id, _)
when (not fp_part || IntLit.iszero i) && not (Ident.is_normal id) && occurs_at_most_once id ->
remove () (* unknown value can be removed in re-execution mode or if the index is zero *)
| Exp.Var id, Sil.Eexp _ when not (Ident.is_normal id) && occurs_at_most_once id ->

2
infer/src/biabduction/Attribute.ml
Unescape View File

@ -391,7 +391,7 @@ let find_equal_formal_path tenv e prop =
Some vfs
| None ->
match get_objc_null tenv prop e with
| Some Apred (Aobjc_null, [_; vfs]) ->
| Some (Apred (Aobjc_null, [_; vfs])) ->
Some vfs
| _ ->
None

15
infer/src/biabduction/Buckets.ml
Unescape View File

@ -93,7 +93,7 @@ let check_access access_opt de_opt =
let has_call_or_sets_null node =
let rec exp_is_null exp =
match exp with
| Exp.Const Const.Cint n ->
| Exp.Const (Const.Cint n) ->
IntLit.iszero n
| Exp.Cast (_, e) ->
exp_is_null e
@ -117,8 +117,9 @@ let check_access access_opt de_opt =
in
let local_access_found = ref false in
let do_node node =
if Int.equal (Procdesc.Node.get_loc node).Location.line line_number
&& has_call_or_sets_null node
if
Int.equal (Procdesc.Node.get_loc node).Location.line line_number
&& has_call_or_sets_null node
then local_access_found := true
in
let path, pos_opt = State.get_path () in
@ -134,14 +135,14 @@ let check_access access_opt de_opt =
else None
in
match access_opt with
| Some Localise.Last_assigned (n, ncf) ->
| Some (Localise.Last_assigned (n, ncf)) ->
find_bucket n ncf
| Some Localise.Returned_from_call n ->
| Some (Localise.Returned_from_call n) ->
find_bucket n false
| Some Localise.Last_accessed (_, is_nullable) when is_nullable ->
| Some (Localise.Last_accessed (_, is_nullable)) when is_nullable ->
Some Localise.BucketLevel.b1
| _ ->
match de_opt with Some DecompiledExp.Dconst _ -> Some Localise.BucketLevel.b1 | _ -> None
match de_opt with Some (DecompiledExp.Dconst _) -> Some Localise.BucketLevel.b1 | _ -> None
let classify_access desc access_opt de_opt is_nullable =

4
infer/src/biabduction/Builtin.ml
Unescape View File

@ -41,7 +41,7 @@ let check_register_populated () =
(** get the symbolic execution handler associated to the builtin function name *)
let get name : t option =
try Some (Typ.Procname.Hash.find builtin_functions name) with Not_found ->
try Some (Typ.Procname.Hash.find builtin_functions name) with Caml.Not_found ->
check_register_populated () ; None
@ -55,7 +55,7 @@ let register proc_name sym_exe_fun : registered =
let pp_registered fmt () =
let builtin_names = ref [] in
Typ.Procname.Hash.iter (fun name _ -> builtin_names := name :: !builtin_names) builtin_functions ;
builtin_names := List.sort ~cmp:Typ.Procname.compare !builtin_names ;
builtin_names := List.sort ~compare:Typ.Procname.compare !builtin_names ;
let pp pname = Format.fprintf fmt "%a@\n" Typ.Procname.pp pname in
Format.fprintf fmt "Registered builtins:@\n @[" ;
List.iter ~f:pp !builtin_names ;

16
infer/src/biabduction/BuiltinDefn.ml
Unescape View File

@ -67,7 +67,7 @@ let add_array_to_prop tenv pdesc prop_ lexp typ =
prop.Prop.sigma
in
match hpred_opt with
| Some Sil.Hpointsto (_, Sil.Earray (len, _, _), _) ->
| Some (Sil.Hpointsto (_, Sil.Earray (len, _, _), _)) ->
Some (len, prop)
| Some _ ->
None (* e points to something but not an array *)
@ -131,7 +131,7 @@ let execute___set_array_length {Builtin.tenv; pdesc; prop_; path; ret_id; args}
prop.Prop.sigma
in
match hpred with
| [(Sil.Hpointsto (e, Sil.Earray (_, esel, inst), t))] ->
| [Sil.Hpointsto (e, Sil.Earray (_, esel, inst), t)] ->
let hpred' = Sil.Hpointsto (e, Sil.Earray (n_len, esel, inst), t) in
let prop' = Prop.set prop ~sigma:(hpred' :: sigma') in
[(Prop.normalize tenv prop', path)]
@ -248,7 +248,7 @@ let replace_ptsto_texp tenv prop root_e texp =
sigma
in
match sigma1 with
| [(Sil.Hpointsto (e, se, _))] ->
| [Sil.Hpointsto (e, se, _)] ->
Sil.Hpointsto (e, se, texp) :: sigma2
| _ ->
sigma
@ -351,7 +351,7 @@ let execute___cast builtin_args : Builtin.ret_typ =
let set_resource_attribute tenv prop path n_lexp loc ra_res =
let prop' =
match Attribute.get_resource tenv prop n_lexp with
| Some Apred (Aresource ra, _) ->
| Some (Apred (Aresource ra, _)) ->
Attribute.add_or_replace tenv prop (Apred (Aresource {ra with ra_res}, [n_lexp]))
| _ ->
let pname = PredSymb.mem_alloc_pname PredSymb.Mnew in
@ -573,7 +573,7 @@ let execute_alloc mk can_return_null {Builtin.pdesc; tenv; prop_; path; ret_id;
| [(size_exp, _)] ->
(* for malloc and __new *)
(size_exp, PredSymb.mem_alloc_pname mk)
| [(size_exp, _); (Exp.Const Const.Cfun pname, _)] ->
| [(size_exp, _); (Exp.Const (Const.Cfun pname), _)] ->
(size_exp, pname)
| _ ->
raise (Exceptions.Wrong_argument_number __POS__)
@ -721,7 +721,7 @@ let execute___split_get_nth {Builtin.tenv; pdesc; prop_; path; ret_id; args} : B
let n_lexp2, prop___ = check_arith_norm_exp tenv pname lexp2 prop__ in
let n_lexp3, prop = check_arith_norm_exp tenv pname lexp3 prop___ in
match (n_lexp1, n_lexp2, n_lexp3) with
| Exp.Const Const.Cstr str1, Exp.Const Const.Cstr str2, Exp.Const Const.Cint n_sil
| Exp.Const (Const.Cstr str1), Exp.Const (Const.Cstr str2), Exp.Const (Const.Cint n_sil)
-> (
let n = IntLit.to_int n_sil in
try
@ -729,7 +729,7 @@ let execute___split_get_nth {Builtin.tenv; pdesc; prop_; path; ret_id; args} : B
let n_part = List.nth_exn parts n in
let res = Exp.Const (Const.Cstr n_part) in
[(return_result tenv res prop ret_id, path)]
with Not_found -> assert false )
with Caml.Not_found -> assert false )
| _ ->
[(prop, path)] )
| _ ->
@ -754,7 +754,7 @@ let execute___infer_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env}
match args with
| [(lexp_msg, _)] -> (
match Prop.exp_normalize_prop tenv prop_ lexp_msg with
| Exp.Const Const.Cstr str ->
| Exp.Const (Const.Cstr str) ->
str
| _ ->
assert false )

53
infer/src/biabduction/Dom.ml
Unescape View File

@ -37,8 +37,8 @@ let equal_sigma sigma1 sigma2 =
if Sil.equal_hpred hpred1 hpred2 then f sigma1_rest' sigma2_rest'
else ( L.d_strln "failure reason 2" ; raise Sil.JoinFail )
in
let sigma1_sorted = List.sort ~cmp:Sil.compare_hpred sigma1 in
let sigma2_sorted = List.sort ~cmp:Sil.compare_hpred sigma2 in
let sigma1_sorted = List.sort ~compare:Sil.compare_hpred sigma1 in
let sigma2_sorted = List.sort ~compare:Sil.compare_hpred sigma2 in
f sigma1_sorted sigma2_sorted
@ -46,7 +46,7 @@ let sigma_get_start_lexps_sort sigma =
let exp_compare_neg e1 e2 = -Exp.compare e1 e2 in
let filter e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
let lexps = Sil.hpred_list_get_lexps filter sigma in
List.sort ~cmp:exp_compare_neg lexps
List.sort ~compare:exp_compare_neg lexps
(** {2 Utility functions for side} *)
@ -100,7 +100,7 @@ end = struct
let lookup' tbl e default =
match e with
| Exp.Var _ -> (
try Hashtbl.find tbl e with Not_found -> Hashtbl.replace tbl e default ; default )
try Hashtbl.find tbl e with Caml.Not_found -> Hashtbl.replace tbl e default ; default )
| _ ->
assert false
@ -378,11 +378,11 @@ module CheckMeet : InfoLossCheckerSig = struct
match (es, e) with
| [], _ ->
true
| [(Exp.Const _)], Exp.Lvar _ ->
| [Exp.Const _], Exp.Lvar _ ->
false
| [(Exp.Const _)], Exp.Var _ ->
| [Exp.Const _], Exp.Var _ ->
not (Exp.Set.mem e lexps)
| [(Exp.Const _)], _ ->
| [Exp.Const _], _ ->
assert false
| [_], Exp.Lvar _ | [_], Exp.Var _ ->
true
@ -498,10 +498,10 @@ end = struct
let minus2_to_2 = List.map ~f:IntLit.of_int [-2; -1; 0; 1; 2]
let get_induced_pi tenv () =
let t_sorted = List.sort ~cmp:entry_compare !t in
let t_sorted = List.sort ~compare:entry_compare !t in
let add_and_chk_eq e1 e1' n =
match (e1, e1') with
| Exp.Const Const.Cint n1, Exp.Const Const.Cint n1' ->
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n1') ->
IntLit.eq (n1 ++ n) n1'
| _ ->
false
@ -538,7 +538,7 @@ end = struct
let eqs, t_minimal = f_eqs [] [] t_sorted in
let f_ineqs acc (e1, e2, e) =
match (e1, e2) with
| Exp.Const Const.Cint n1, Exp.Const Const.Cint n2 ->
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) ->
let strict_lower1, upper1 =
if IntLit.leq n1 n2 then (n1 -- IntLit.one, n2) else (n2 -- IntLit.one, n1)
in
@ -640,11 +640,11 @@ end = struct
let res = ref [] in
let f v =
match (v, side) with
| (Exp.BinOp (Binop.PlusA, e1', Exp.Const Const.Cint i), e2, e'), Lhs when Exp.equal e e1' ->
| (Exp.BinOp (Binop.PlusA, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs when Exp.equal e e1' ->
let c' = Exp.int (IntLit.neg i) in
let v' = (e1', Exp.BinOp (Binop.PlusA, e2, c'), Exp.BinOp (Binop.PlusA, e', c')) in
res := v' :: !res
| (e1, Exp.BinOp (Binop.PlusA, e2', Exp.Const Const.Cint i), e'), Rhs when Exp.equal e e2' ->
| (e1, Exp.BinOp (Binop.PlusA, e2', Exp.Const (Const.Cint i)), e'), Rhs when Exp.equal e e2' ->
let c' = Exp.int (IntLit.neg i) in
let v' = (Exp.BinOp (Binop.PlusA, e1, c'), e2', Exp.BinOp (Binop.PlusA, e', c')) in
res := v' :: !res
@ -694,7 +694,7 @@ end = struct
renaming_restricted
in
let sub_list_side_sorted =
List.sort ~cmp:(fun (_, e) (_, e') -> Exp.compare e e') sub_list_side
List.sort ~compare:(fun (_, e) (_, e') -> Exp.compare e e') sub_list_side
in
let rec find_duplicates = function
| (_, e) :: ((_, e') :: _ as t) ->
@ -722,7 +722,7 @@ end = struct
in
let sub_list_sorted =
let compare (i, _) (i', _) = Ident.compare i i' in
List.sort ~cmp:compare sub_list
List.sort ~compare sub_list
in
let rec find_duplicates = function
| (i, _) :: ((i', _) :: _ as t) ->
@ -812,13 +812,13 @@ end = struct
| Sil.Aeq (e', (Exp.Var id as e))
when exp_contains_only_normal_ids e' && not (Ident.is_normal id) ->
build_other_atoms (fun e0 -> Prop.mk_eq tenv e0 e') side e
| Sil.Aeq (Exp.BinOp (Binop.Le, e, e'), Exp.Const Const.Cint i)
| Sil.Aeq (Exp.Const Const.Cint i, Exp.BinOp (Binop.Le, e, e'))
| Sil.Aeq (Exp.BinOp (Binop.Le, e, e'), Exp.Const (Const.Cint i))
| Sil.Aeq (Exp.Const (Const.Cint i), Exp.BinOp (Binop.Le, e, e'))
when IntLit.isone i && exp_contains_only_normal_ids e' ->
let construct e0 = Prop.mk_inequality tenv (Exp.BinOp (Binop.Le, e0, e')) in
build_other_atoms construct side e
| Sil.Aeq (Exp.BinOp (Binop.Lt, e', e), Exp.Const Const.Cint i)
| Sil.Aeq (Exp.Const Const.Cint i, Exp.BinOp (Binop.Lt, e', e))
| Sil.Aeq (Exp.BinOp (Binop.Lt, e', e), Exp.Const (Const.Cint i))
| Sil.Aeq (Exp.Const (Const.Cint i), Exp.BinOp (Binop.Lt, e', e))
when IntLit.isone i && exp_contains_only_normal_ids e' ->
let construct e0 = Prop.mk_inequality tenv (Exp.BinOp (Binop.Lt, e', e0)) in
build_other_atoms construct side e
@ -843,8 +843,9 @@ end = struct
|| Exp.free_vars e2 |> Sequence.exists ~f:Ident.is_primed
in
let e =
if not (Exp.free_vars e1 |> Sequence.exists ~f:can_rename)
&& not (Exp.free_vars e2 |> Sequence.exists ~f:can_rename)
if
not (Exp.free_vars e1 |> Sequence.exists ~f:can_rename)
&& not (Exp.free_vars e2 |> Sequence.exists ~f:can_rename)
then
if Exp.equal e1 e2 then e1 else ( L.d_strln "failure reason 13" ; raise Sil.JoinFail )
else
@ -927,7 +928,7 @@ let hpred_construct_fresh side =
(** {2 Join and Meet for Ids} *)
let ident_same_kind_primed_footprint id1 id2 =
Ident.is_primed id1 && Ident.is_primed id2 || Ident.is_footprint id1 && Ident.is_footprint id2
(Ident.is_primed id1 && Ident.is_primed id2) || (Ident.is_footprint id1 && Ident.is_footprint id2)
let ident_partial_join (id1: Ident.t) (id2: Ident.t) =
@ -998,12 +999,12 @@ let rec exp_partial_join (e1: Exp.t) (e2: Exp.t) : Exp.t =
| Exp.Var id1, Exp.BinOp (Binop.PlusA, Exp.Var id2, Exp.Const _)
when ident_same_kind_primed_footprint id1 id2 ->
Rename.extend e1 e2 Rename.ExtFresh
| Exp.BinOp (Binop.PlusA, Exp.Var id1, Exp.Const Const.Cint c1), Exp.Const Const.Cint c2
| Exp.BinOp (Binop.PlusA, Exp.Var id1, Exp.Const (Const.Cint c1)), Exp.Const (Const.Cint c2)
when can_rename id1 ->
let c2' = c2 -- c1 in
let e_res = Rename.extend (Exp.Var id1) (Exp.int c2') Rename.ExtFresh in
Exp.BinOp (Binop.PlusA, e_res, Exp.int c1)
| Exp.Const Const.Cint c1, Exp.BinOp (Binop.PlusA, Exp.Var id2, Exp.Const Const.Cint c2)
| Exp.Const (Const.Cint c1), Exp.BinOp (Binop.PlusA, Exp.Var id2, Exp.Const (Const.Cint c2))
when can_rename id2 ->
let c1' = c1 -- c2 in
let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in
@ -1615,7 +1616,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc: Prop.sigma) (sigma1_in: Prop.s
CheckJoin.add Rhs iF2 iB2 ;
(* add equality iF2=iB2 *)
sigma_partial_join' tenv mode sigma_acc' sigma1' sigma2
| Some Sil.Hpointsto _, Some Sil.Hpointsto _ ->
| Some (Sil.Hpointsto _), Some (Sil.Hpointsto _) ->
assert false
(* Should be handled by a guarded case *)
with Todo.Empty ->
@ -1707,7 +1708,7 @@ let pi_partial_join tenv mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop
(* find some array length in the prop, to be used as heuritic for upper bound in widening *)
let len_list = ref [] in
let do_hpred = function
| Sil.Hpointsto (_, Sil.Earray (Exp.Const Const.Cint n, _, _), _) ->
| Sil.Hpointsto (_, Sil.Earray (Exp.Const (Const.Cint n), _, _), _) ->
if IntLit.geq n IntLit.one then len_list := n :: !len_list
| _ ->
()
@ -1718,7 +1719,7 @@ let pi_partial_join tenv mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop
let bounds =
let bounds1 = get_array_len ep1 in
let bounds2 = get_array_len ep2 in
let bounds_sorted = List.sort ~cmp:IntLit.compare_value (bounds1 @ bounds2) in
let bounds_sorted = List.sort ~compare:IntLit.compare_value (bounds1 @ bounds2) in
List.rev (List.remove_consecutive_duplicates ~equal:IntLit.eq bounds_sorted)
in
let widening_atom a =

3
infer/src/biabduction/Match.ml
Unescape View File

@ -709,7 +709,8 @@ let rec generic_find_partial_iso tenv mode update corres sigma_corres todos sigm
generic_find_partial_iso tenv mode update new_corres sigma_corres todos' sigma_todo )
| None, _ | _, None ->
None
| Some Sil.Hpointsto (_, _, te1), Some Sil.Hpointsto (_, _, te2) when not (Exp.equal te1 te2) ->
| Some (Sil.Hpointsto (_, _, te1)), Some (Sil.Hpointsto (_, _, te2))
when not (Exp.equal te1 te2) ->
None
| Some (Sil.Hpointsto (_, se1, _) as hpred1), Some (Sil.Hpointsto (_, se2, _) as hpred2) -> (
match generate_todos_from_strexp mode [] se1 se2 with

16
infer/src/biabduction/Paths.ml
Unescape View File

@ -79,7 +79,7 @@ end = struct
type stats =
{ mutable max_length: int
; (* length of the longest linear sequence *)
mutable linear_num: float
mutable linear_num: float
(* number of linear sequences described by the path *) }
(* type aliases for components of t values that compare should ignore *)
@ -108,7 +108,7 @@ end = struct
and continue with [path]. *)
| Pjoin of t * t * stats_ (** join of two paths *)
| Pcall of t * procname_ * path_exec_ * stats_ (** add a sub-path originating from a call *)
[@@deriving compare]
[@@deriving compare]
let get_dummy_stats () = {max_length= -1; linear_num= -1.0}
@ -361,7 +361,7 @@ end = struct
try
let n = Procdesc.NodeMap.find node !map in
map := Procdesc.NodeMap.add node (n + 1) !map
with Not_found -> map := Procdesc.NodeMap.add node 1 !map )
with Caml.Not_found -> map := Procdesc.NodeMap.add node 1 !map )
| None ->
()
in
@ -402,7 +402,7 @@ end = struct
let delayed_num = ref 0 in
let delayed = ref PathMap.empty in
let add_path p =
try ignore (PathMap.find p !delayed) with Not_found ->
try ignore (PathMap.find p !delayed) with Caml.Not_found ->
incr delayed_num ;
delayed := PathMap.add p !delayed_num !delayed
in
@ -424,10 +424,10 @@ end = struct
in
let rec doit n fmt path =
try
if n > 0 then raise Not_found ;
if n > 0 then raise Caml.Not_found ;
let num = PathMap.find path !delayed in
F.fprintf fmt "P%d" num
with Not_found ->
with Caml.Not_found ->
match path with
| Pstart (node, _) ->
F.fprintf fmt "n%a" Procdesc.Node.pp node
@ -639,7 +639,7 @@ end = struct
try
let path_old = PropMap.find p ps in
Path.join path_old path
with Not_found -> path
with Caml.Not_found -> path
in
PropMap.add p path_new ps
@ -664,7 +664,7 @@ end = struct
let path_old = PropMap.find p !res in
if path_nodes_subset path path_old (* do not propagate new path if it has no new nodes *)
then res := PropMap.remove p !res
with Not_found -> res := PropMap.remove p !res
with Caml.Not_found -> res := PropMap.remove p !res
in
PropMap.iter rem ps2 ; !res

268
infer/src/biabduction/Prop.ml
Unescape View File

@ -47,7 +47,7 @@ module Core : sig
; pi: pi (** pure part *)
; sigma_fp: sigma (** abduced spatial part *)
; pi_fp: pi (** abduced pure part *) }
[@@deriving compare]
[@@deriving compare]
val prop_emp : normal t
(** Proposition [true /\ emp]. *)
@ -75,7 +75,7 @@ end = struct
; pi: pi (** pure part *)
; sigma_fp: sigma (** abduced spatial part *)
; pi_fp: pi (** abduced pure part *) }
[@@deriving compare]
[@@deriving compare]
(** Proposition [true /\ emp]. *)
let prop_emp : normal t = {sub= Sil.exp_sub_empty; pi= []; sigma= []; pi_fp= []; sigma_fp= []}
@ -198,7 +198,7 @@ let sigma_get_stack_nonstack only_local_vars sigma =
let pp_sigma_simple pe env fmt sigma =
let sigma_stack, sigma_nonstack = sigma_get_stack_nonstack false sigma in
let pp_stack fmt sg_ =
let sg = List.sort ~cmp:Sil.compare_hpred sg_ in
let sg = List.sort ~compare:Sil.compare_hpred sg_ in
if sg <> [] then
Format.fprintf fmt "%a" (Pp.semicolon_seq ~print_env:pe (pp_hpred_stackvar pe)) sg
in
@ -236,7 +236,7 @@ let get_pure_extended p =
let old_id = Ident.Map.find pid primed_map in
let new_atom = Sil.Aeq (Var id, Var old_id) in
(new_atom :: atoms, primed_map)
with Not_found -> (atoms, Ident.Map.add pid id primed_map)
with Caml.Not_found -> (atoms, Ident.Map.add pid id primed_map)
in
match base_atom with
| Sil.Aeq (Exp.Var id0, Exp.Var id1) when Ident.is_primed id0 && not (Ident.is_primed id1) ->
@ -423,7 +423,7 @@ let sigma_sub subst sigma =
(** Return [true] if the atom is an inequality *)
let atom_is_inequality (atom: Sil.atom) =
match atom with
| Aeq (BinOp ((Le | Lt), _, _), Const Cint i) when IntLit.isone i ->
| Aeq (BinOp ((Le | Lt), _, _), Const (Cint i)) when IntLit.isone i ->
true
| _ ->
false
@ -432,7 +432,7 @@ let atom_is_inequality (atom: Sil.atom) =
(** If the atom is [e<=n] return [e,n] *)
let atom_exp_le_const (atom: Sil.atom) =
match atom with
| Aeq (BinOp (Le, e1, Const Cint n), Const Cint i) when IntLit.isone i ->
| Aeq (BinOp (Le, e1, Const (Cint n)), Const (Cint i)) when IntLit.isone i ->
Some (e1, n)
| _ ->
None
@ -441,7 +441,7 @@ let atom_exp_le_const (atom: Sil.atom) =
(** If the atom is [n<e] return [n,e] *)
let atom_const_lt_exp (atom: Sil.atom) =
match atom with
| Aeq (BinOp (Lt, Const Cint n, e1), Const Cint i) when IntLit.isone i ->
| Aeq (BinOp (Lt, Const (Cint n), e1), Const (Cint i)) when IntLit.isone i ->
Some (n, e1)
| _ ->
None
@ -478,8 +478,8 @@ let rec create_strexp_of_type ~path tenv struct_init_mode (typ: Typ.t) len inst
if List.exists ~f:(fun (n, _) -> Typ.Name.equal n name) path then
L.die InternalError
"Ill-founded recursion in [create_strexp_of_type]: a sub-element of struct %a is also \
of type struct %a: %a:%a" Typ.Name.pp name Typ.Name.pp name pp_path (List.rev path)
Typ.Name.pp name ;
of type struct %a: %a:%a"
Typ.Name.pp name Typ.Name.pp name pp_path (List.rev path) Typ.Name.pp name ;
match (struct_init_mode, Tenv.lookup tenv name) with
| Fld_init, Some {fields} ->
(* pass len as an accumulator, so that it is passed to create_strexp_of_type for the last
@ -521,13 +521,13 @@ let replace_array_contents (hpred: Sil.hpred) esel : Sil.hpred =
(** remove duplicate atoms and redundant inequalities from a sorted pi *)
let rec pi_sorted_remove_redundant (pi: pi) =
match pi with
| (Aeq (BinOp (Le, e1, Const Cint n1), Const Cint i1) as a1)
:: (Aeq (BinOp (Le, e2, Const Cint n2), Const Cint i2)) :: rest
| (Aeq (BinOp (Le, e1, Const (Cint n1)), Const (Cint i1)) as a1)
:: Aeq (BinOp (Le, e2, Const (Cint n2)), Const (Cint i2)) :: rest
when IntLit.isone i1 && IntLit.isone i2 && Exp.equal e1 e2 && IntLit.lt n1 n2 ->
(* second inequality redundant *)
pi_sorted_remove_redundant (a1 :: rest)
| (Aeq (BinOp (Lt, Const Cint n1, e1), Const Cint i1))
:: (Aeq (BinOp (Lt, Const Cint n2, e2), Const Cint i2) as a2) :: rest
| Aeq (BinOp (Lt, Const (Cint n1), e1), Const (Cint i1))
:: (Aeq (BinOp (Lt, Const (Cint n2), e2), Const (Cint i2)) as a2) :: rest
when IntLit.isone i1 && IntLit.isone i2 && Exp.equal e1 e2 && IntLit.lt n1 n2 ->
(* first inequality redundant *)
pi_sorted_remove_redundant (a2 :: rest)
@ -615,9 +615,9 @@ module Normalize = struct
match sigma1 with
| [] ->
set
| (Hpointsto (e, _, _)) :: sigma' | (Hlseg (Sil.Lseg_NE, _, e, _, _)) :: sigma' ->
| Hpointsto (e, _, _) :: sigma' | Hlseg (Sil.Lseg_NE, _, e, _, _) :: sigma' ->
f_alloc (Exp.Set.add e set) sigma'
| (Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _)) :: sigma' ->
| Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _) :: sigma' ->
f_alloc (Exp.Set.add iF (Exp.Set.add iB set)) sigma'
| _ :: sigma' ->
f_alloc set sigma'
@ -630,12 +630,12 @@ module Normalize = struct
(List.rev eqs_zero, List.rev sigma_passed)
| (Hpointsto _ as hpred) :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma'
| (Hlseg (Lseg_PE, _, e1, e2, _)) :: sigma'
| Hlseg (Lseg_PE, _, e1, e2, _) :: sigma'
when Exp.equal e1 Exp.zero || Exp.Set.mem e1 alloc_set ->
f (Sil.Aeq (e1, e2) :: eqs_zero) sigma_passed sigma'
| (Hlseg _ as hpred) :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma'
| (Hdllseg (Lseg_PE, _, iF, oB, oF, iB, _)) :: sigma'
| Hdllseg (Lseg_PE, _, iF, oB, oF, iB, _) :: sigma'
when Exp.equal iF Exp.zero || Exp.Set.mem iF alloc_set || Exp.equal iB Exp.zero
|| Exp.Set.mem iB alloc_set ->
f (Sil.Aeq (iF, oF) :: Sil.Aeq (iB, oB) :: eqs_zero) sigma_passed sigma'
@ -652,14 +652,14 @@ module Normalize = struct
List.rev sigma_passed
| (Hpointsto _ as hpred) :: sigma' ->
f (hpred :: sigma_passed) sigma'
| (Hlseg (Lseg_PE, para, f1, f2, shared)) :: sigma'
when Exp.equal e1 f1 && Exp.equal e2 f2 || Exp.equal e2 f1 && Exp.equal e1 f2 ->
| Hlseg (Lseg_PE, para, f1, f2, shared) :: sigma'
when (Exp.equal e1 f1 && Exp.equal e2 f2) || (Exp.equal e2 f1 && Exp.equal e1 f2) ->
f (Sil.Hlseg (Lseg_NE, para, f1, f2, shared) :: sigma_passed) sigma'
| (Hlseg _ as hpred) :: sigma' ->
f (hpred :: sigma_passed) sigma'
| (Hdllseg (Lseg_PE, para, iF, oB, oF, iB, shared)) :: sigma'
when Exp.equal e1 iF && Exp.equal e2 oF || Exp.equal e2 iF && Exp.equal e1 oF
|| Exp.equal e1 iB && Exp.equal e2 oB || Exp.equal e2 iB && Exp.equal e1 oB ->
| Hdllseg (Lseg_PE, para, iF, oB, oF, iB, shared) :: sigma'
when (Exp.equal e1 iF && Exp.equal e2 oF) || (Exp.equal e2 iF && Exp.equal e1 oF)
|| (Exp.equal e1 iB && Exp.equal e2 oB) || (Exp.equal e2 iB && Exp.equal e1 oB) ->
f (Sil.Hdllseg (Lseg_NE, para, iF, oB, oF, iB, shared) :: sigma_passed) sigma'
| (Hdllseg _ as hpred) :: sigma' ->
f (hpred :: sigma_passed) sigma'
@ -699,9 +699,9 @@ module Normalize = struct
eval e1
| UnOp (Unop.LNot, e1, topt) -> (
match eval e1 with
| Const Cint i when IntLit.iszero i ->
| Const (Cint i) when IntLit.iszero i ->
Exp.one
| Const Cint _ ->
| Const (Cint _) ->
Exp.zero
| UnOp (LNot, e1', _) ->
e1'
@ -711,9 +711,9 @@ module Normalize = struct
match eval e1 with
| UnOp (Neg, e2', _) ->
e2'
| Const Cint i ->
| Const (Cint i) ->
Exp.int (IntLit.neg i)
| Const Cfloat v ->
| Const (Cfloat v) ->
Exp.float ~-.v
| Var id ->
UnOp (Neg, Var id, topt)
@ -723,31 +723,31 @@ module Normalize = struct
match eval e1 with
| UnOp (BNot, e2', _) ->
e2'
| Const Cint i ->
| Const (Cint i) ->
Exp.int (IntLit.lognot i)
| e1' ->
if abs then Exp.get_undefined false else UnOp (BNot, e1', topt) )
| BinOp (Le, e1, e2) -> (
match (eval e1, eval e2) with
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.bool (IntLit.leq n m)
| Const Cfloat v, Const Cfloat w ->
| Const (Cfloat v), Const (Cfloat w) ->
Exp.bool (v <= w)
| BinOp (PlusA, e3, Const Cint n), Const Cint m ->
| BinOp (PlusA, e3, Const (Cint n)), Const (Cint m) ->
BinOp (Le, e3, Exp.int (m -- n))
| e1', e2' ->
Exp.le e1' e2' )
| BinOp (Lt, e1, e2) -> (
match (eval e1, eval e2) with
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.bool (IntLit.lt n m)
| Const Cfloat v, Const Cfloat w ->
| Const (Cfloat v), Const (Cfloat w) ->
Exp.bool (v < w)
| Const Cint n, BinOp (MinusA, f1, f2) ->
| Const (Cint n), BinOp (MinusA, f1, f2) ->
BinOp (Le, BinOp (MinusA, f2, f1), Exp.int (IntLit.minus_one -- n))
| BinOp (MinusA, f1, f2), Const Cint n ->
| BinOp (MinusA, f1, f2), Const (Cint n) ->
Exp.le (BinOp (MinusA, f1, f2)) (Exp.int (n -- IntLit.one))
| BinOp (PlusA, e3, Const Cint n), Const Cint m ->
| BinOp (PlusA, e3, Const (Cint n)), Const (Cint m) ->
BinOp (Lt, e3, Exp.int (m -- n))
| e1', e2' ->
Exp.lt e1' e2' )
@ -757,11 +757,11 @@ module Normalize = struct
eval (Exp.lt e2 e1)
| BinOp (Eq, e1, e2) -> (
match (eval e1, eval e2) with
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.bool (IntLit.eq n m)
| Const Cfloat v, Const Cfloat w ->
| Const (Cfloat v), Const (Cfloat w) ->
Exp.bool (Float.equal v w)
| Const Cint _, Exp.Lvar _ | Exp.Lvar _, Const Cint _ ->
| Const (Cint _), Exp.Lvar _ | Exp.Lvar _, Const (Cint _) ->
(* Comparing pointer with nonzero integer is undefined behavior in ISO C++ *)
(* Assume they are not equal *)
Exp.zero
@ -769,11 +769,11 @@ module Normalize = struct
Exp.eq e1' e2' )
| BinOp (Ne, e1, e2) -> (
match (eval e1, eval e2) with
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.bool (IntLit.neq n m)
| Const Cfloat v, Const Cfloat w ->
| Const (Cfloat v), Const (Cfloat w) ->
Exp.bool (v <> w)
| Const Cint _, Exp.Lvar _ | Exp.Lvar _, Const Cint _ ->
| Const (Cint _), Exp.Lvar _ | Exp.Lvar _, Const (Cint _) ->
(* Comparing pointer with nonzero integer is undefined behavior in ISO C++ *)
(* Assume they are not equal *)
Exp.one
@ -784,13 +784,13 @@ module Normalize = struct
let e1' = eval e1 in
let e2' = eval e2 in
match (e1', e2') with
| Const Cint i, _ when IntLit.iszero i ->
| Const (Cint i), _ when IntLit.iszero i ->
e1'
| Const Cint _, _ ->
| Const (Cint _), _ ->
e2'
| _, Const Cint i when IntLit.iszero i ->
| _, Const (Cint i) when IntLit.iszero i ->
e2'
| _, Const Cint _ ->
| _, Const (Cint _) ->
e1'
| _ ->
BinOp (LAnd, e1', e2') )
@ -799,13 +799,13 @@ module Normalize = struct
let e1' = eval e1 in
let e2' = eval e2 in
match (e1', e2') with
| Const Cint i, _ when IntLit.iszero i ->
| Const (Cint i), _ when IntLit.iszero i ->
e2'
| Const Cint _, _ ->
| Const (Cint _), _ ->
e1'
| _, Const Cint i when IntLit.iszero i ->
| _, Const (Cint i) when IntLit.iszero i ->
e1'
| _, Const Cint _ ->
| _, Const (Cint _) ->
e2'
| _ ->
BinOp (LOr, e1', e2') )
@ -826,18 +826,18 @@ module Normalize = struct
let ominus = if isPlusA then Binop.MinusA else Binop.MinusPI in
let ( +++ ) (x: Exp.t) (y: Exp.t) : Exp.t =
match (x, y) with
| _, Const Cint i when IntLit.iszero i ->
| _, Const (Cint i) when IntLit.iszero i ->
x
| Const Cint i, Const Cint j ->
| Const (Cint i), Const (Cint j) ->
Const (Cint (IntLit.add i j))
| _ ->
BinOp (oplus, x, y)
in
let ( --- ) (x: Exp.t) (y: Exp.t) : Exp.t =
match (x, y) with
| _, Const Cint i when IntLit.iszero i ->
| _, Const (Cint i) when IntLit.iszero i ->
x
| Const Cint i, Const Cint j ->
| Const (Cint i), Const (Cint j) ->
Const (Cint (IntLit.sub i j))
| _ ->
BinOp (ominus, x, y)
@ -859,19 +859,19 @@ module Normalize = struct
e2'
| _, Const c when Const.iszero_int_float c ->
e1'
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.int (n ++ m)
| Const Cfloat v, Const Cfloat w ->
| Const (Cfloat v), Const (Cfloat w) ->
Exp.float (v +. w)
| UnOp (Neg, f1, _), f2 | f2, UnOp (Neg, f1, _) ->
BinOp (ominus, f2, f1)
| BinOp (PlusA, e, Const Cint n1), Const Cint n2
| BinOp (PlusPI, e, Const Cint n1), Const Cint n2
| Const Cint n2, BinOp (PlusA, e, Const Cint n1)
| Const Cint n2, BinOp (PlusPI, e, Const Cint n1) ->
| BinOp (PlusA, e, Const (Cint n1)), Const (Cint n2)
| BinOp (PlusPI, e, Const (Cint n1)), Const (Cint n2)
| Const (Cint n2), BinOp (PlusA, e, Const (Cint n1))
| Const (Cint n2), BinOp (PlusPI, e, Const (Cint n1)) ->
e +++ Exp.int (n1 ++ n2)
| BinOp (MinusA, Const Cint n1, e), Const Cint n2
| Const Cint n2, BinOp (MinusA, Const Cint n1, e) ->
| BinOp (MinusA, Const (Cint n1), e), Const (Cint n2)
| Const (Cint n2), BinOp (MinusA, Const (Cint n1), e) ->
Exp.int (n1 ++ n2) --- e
| BinOp (MinusA, e1, e2), e3 ->
(* (e1-e2)+e3 --> e1 + (e3-e2) *)
@ -902,13 +902,13 @@ module Normalize = struct
eval (Exp.UnOp (Neg, e2', None))
| _, Const c when Const.iszero_int_float c ->
e1'
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.int (n -- m)
| Const Cfloat v, Const Cfloat w ->
| Const (Cfloat v), Const (Cfloat w) ->
Exp.float (v -. w)
| _, UnOp (Neg, f2, _) ->
eval (e1 +++ f2)
| _, Const Cint n ->
| _, Const (Cint n) ->
eval (e1' +++ Exp.int (IntLit.neg n))
| Const _, _ ->
e1' --- e2'
@ -935,9 +935,9 @@ module Normalize = struct
e1'
| _, Const c when Const.isminusone_int_float c ->
eval (Exp.UnOp (Neg, e1', None))
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.int (IntLit.mul n m)
| Const Cfloat v, Const Cfloat w ->
| Const (Cfloat v), Const (Cfloat w) ->
Exp.float (v *. w)
| Var _, Var _ ->
BinOp (Mult, e1', e2')
@ -956,9 +956,9 @@ module Normalize = struct
e1'
| _, Const c when Const.isone_int_float c ->
e1'
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.int (IntLit.div n m)
| Const Cfloat v, Const Cfloat w ->
| Const (Cfloat v), Const (Cfloat w) ->
Exp.float (v /. w)
| ( Sizeof {typ= {desc= Tarray {elt}}; dynamic_length= Some len}
, Sizeof {typ= elt2; dynamic_length= None} )
@ -977,13 +977,13 @@ module Normalize = struct
let e1' = eval e1 in
let e2' = eval e2 in
match (e1', e2') with
| _, Const Cint i when IntLit.iszero i ->
| _, Const (Cint i) when IntLit.iszero i ->
Exp.get_undefined false
| Const Cint i, _ when IntLit.iszero i ->
| Const (Cint i), _ when IntLit.iszero i ->
e1'
| _, Const Cint i when IntLit.isone i ->
| _, Const (Cint i) when IntLit.isone i ->
Exp.zero
| Const Cint n, Const Cint m ->
| Const (Cint n), Const (Cint m) ->
Exp.int (IntLit.rem n m)
| _ ->
if abs then Exp.get_undefined false else BinOp (Mod, e1', e2') )
@ -992,14 +992,14 @@ module Normalize = struct
if abs then Exp.get_undefined false
else
match (e1, e2) with
| Const Cint n, Const Cint m -> (
| Const (Cint n), Const (Cint m) -> (
try Exp.int (IntLit.shift_left n m) with IntLit.OversizedShift ->
BinOp (Shiftlt, eval e1, eval e2) )
| _, Const Cint m when IntLit.iszero m ->
| _, Const (Cint m) when IntLit.iszero m ->
eval e1
| _, Const Cint m when IntLit.isone m ->
| _, Const (Cint m) when IntLit.isone m ->
eval (Exp.BinOp (PlusA, e1, e1))
| Const Cint m, _ when IntLit.iszero m ->
| Const (Cint m), _ when IntLit.iszero m ->
e1
| _ ->
BinOp (Shiftlt, eval e1, eval e2) )
@ -1008,12 +1008,12 @@ module Normalize = struct
if abs then Exp.get_undefined false
else
match (e1, e2) with
| Const Cint n, Const Cint m -> (
| Const (Cint n), Const (Cint m) -> (
try Exp.int (IntLit.shift_right n m) with IntLit.OversizedShift ->
BinOp (Shiftrt, eval e1, eval e2) )
| _, Const Cint m when IntLit.iszero m ->
| _, Const (Cint m) when IntLit.iszero m ->
eval e1
| Const Cint m, _ when IntLit.iszero m ->
| Const (Cint m), _ when IntLit.iszero m ->
e1
| _ ->
BinOp (Shiftrt, eval e1, eval e2) )
@ -1022,11 +1022,11 @@ module Normalize = struct
let e1' = eval e1 in
let e2' = eval e2 in
match (e1', e2') with
| Const Cint i, _ when IntLit.iszero i ->
| Const (Cint i), _ when IntLit.iszero i ->
e1'
| _, Const Cint i when IntLit.iszero i ->
| _, Const (Cint i) when IntLit.iszero i ->
e2'
| Const Cint i1, Const Cint i2 ->
| Const (Cint i1), Const (Cint i2) ->
Exp.int (IntLit.logand i1 i2)
| _ ->
if abs then Exp.get_undefined false else BinOp (BAnd, e1', e2') )
@ -1035,11 +1035,11 @@ module Normalize = struct
let e1' = eval e1 in
let e2' = eval e2 in
match (e1', e2') with
| Const Cint i, _ when IntLit.iszero i ->
| Const (Cint i), _ when IntLit.iszero i ->
e2'
| _, Const Cint i when IntLit.iszero i ->
| _, Const (Cint i) when IntLit.iszero i ->
e1'
| Const Cint i1, Const Cint i2 ->
| Const (Cint i1), Const (Cint i2) ->
Exp.int (IntLit.logor i1 i2)
| _ ->
if abs then Exp.get_undefined false else BinOp (BOr, e1', e2') )
@ -1048,11 +1048,11 @@ module Normalize = struct
let e1' = eval e1 in
let e2' = eval e2 in
match (e1', e2') with
| Const Cint i, _ when IntLit.iszero i ->
| Const (Cint i), _ when IntLit.iszero i ->
e2'
| _, Const Cint i when IntLit.iszero i ->
| _, Const (Cint i) when IntLit.iszero i ->
e1'
| Const Cint i1, Const Cint i2 ->
| Const (Cint i1), Const (Cint i2) ->
Exp.int (IntLit.logxor i1 i2)
| _ ->
if abs then Exp.get_undefined false else BinOp (BXor, e1', e2') )
@ -1106,24 +1106,24 @@ module Normalize = struct
(** Turn an inequality expression into an atom *)
let mk_inequality tenv (e: Exp.t) : Sil.atom =
match e with
| BinOp (Le, base, Const Cint n)
| BinOp (Le, base, Const (Cint n))
-> (
(* base <= n case *)
let nbase = exp_normalize_noabs tenv Sil.sub_empty base in
match nbase with
| BinOp (PlusA, base', Const Cint n') ->
| BinOp (PlusA, base', Const (Cint n')) ->
let new_offset = Exp.int (n -- n') in
let new_e : Exp.t = BinOp (Le, base', new_offset) in
Aeq (new_e, Exp.one)
| BinOp (PlusA, Const Cint n', base') ->
| BinOp (PlusA, Const (Cint n'), base') ->
let new_offset = Exp.int (n -- n') in
let new_e : Exp.t = BinOp (Le, base', new_offset) in
Aeq (new_e, Exp.one)
| BinOp (MinusA, base', Const Cint n') ->
| BinOp (MinusA, base', Const (Cint n')) ->
let new_offset = Exp.int (n ++ n') in
let new_e : Exp.t = BinOp (Le, base', new_offset) in
Aeq (new_e, Exp.one)
| BinOp (MinusA, Const Cint n', base') ->
| BinOp (MinusA, Const (Cint n'), base') ->
let new_offset = Exp.int (n' -- n -- IntLit.one) in
let new_e : Exp.t = BinOp (Lt, new_offset, base') in
Aeq (new_e, Exp.one)
@ -1134,24 +1134,24 @@ module Normalize = struct
Aeq (new_e, Exp.one)
| _ ->
Aeq (e, Exp.one) )
| BinOp (Lt, Const Cint n, base)
| BinOp (Lt, Const (Cint n), base)
-> (
(* n < base case *)
let nbase = exp_normalize_noabs tenv Sil.sub_empty base in
match nbase with
| BinOp (PlusA, base', Const Cint n') ->
| BinOp (PlusA, base', Const (Cint n')) ->
let new_offset = Exp.int (n -- n') in
let new_e : Exp.t = BinOp (Lt, new_offset, base') in
Aeq (new_e, Exp.one)
| BinOp (PlusA, Const Const.Cint n', base') ->
| BinOp (PlusA, Const (Const.Cint n'), base') ->
let new_offset = Exp.int (n -- n') in
let new_e : Exp.t = BinOp (Lt, new_offset, base') in
Aeq (new_e, Exp.one)
| BinOp (MinusA, base', Const Cint n') ->
| BinOp (MinusA, base', Const (Cint n')) ->
let new_offset = Exp.int (n ++ n') in
let new_e : Exp.t = BinOp (Lt, new_offset, base') in
Aeq (new_e, Exp.one)
| BinOp (MinusA, Const Cint n', base') ->
| BinOp (MinusA, Const (Cint n'), base') ->
let new_offset = Exp.int (n' -- n -- IntLit.one) in
let new_e : Exp.t = BinOp (Le, base', new_offset) in
Aeq (new_e, Exp.one)
@ -1172,7 +1172,7 @@ module Normalize = struct
integer offset representing inequality [sum(pos) - sum(neg) + off <= 0] *)
let rec exp_to_posnegoff (e: Exp.t) =
match e with
| Const Cint n ->
| Const (Cint n) ->
([], [], n)
| BinOp (PlusA, e1, e2) | BinOp (PlusPI, e1, e2) ->
let pos1, neg1, n1 = exp_to_posnegoff e1 in
@ -1190,8 +1190,8 @@ module Normalize = struct
in
(* sort and filter out expressions appearing in both the positive and negative part *)
let normalize_posnegoff (pos, neg, off) =
let pos' = List.sort ~cmp:Exp.compare pos in
let neg' = List.sort ~cmp:Exp.compare neg in
let pos' = List.sort ~compare:Exp.compare pos in
let neg' = List.sort ~compare:Exp.compare neg in
let rec combine pacc nacc = function
| x :: ps, y :: ng -> (
match Exp.compare x y with
@ -1229,7 +1229,7 @@ module Normalize = struct
BinOp (Le, lhs_e, Exp.int (IntLit.zero -- n))
in
let ineq =
match a with Aeq (ineq, Const Cint i) when IntLit.isone i -> ineq | _ -> assert false
match a with Aeq (ineq, Const (Cint i)) when IntLit.isone i -> ineq | _ -> assert false
in
match ineq with
| BinOp (Le, e1, e2) ->
@ -1249,15 +1249,15 @@ module Normalize = struct
let a = Sil.atom_sub sub a0 in
let rec normalize_eq (eq: Exp.t * Exp.t) =
match eq with
| BinOp (PlusA, e1, Const Cint n1), Const Cint n2
| BinOp (PlusA, e1, Const (Cint n1)), Const (Cint n2)
(* e1+n1==n2 ---> e1==n2-n1 *)
| BinOp (PlusPI, e1, Const Cint n1), Const Cint n2 ->
| BinOp (PlusPI, e1, Const (Cint n1)), Const (Cint n2) ->
(e1, Exp.int (n2 -- n1))
| BinOp (MinusA, e1, Const Cint n1), Const Cint n2
| BinOp (MinusA, e1, Const (Cint n1)), Const (Cint n2)
(* e1-n1==n2 ---> e1==n1+n2 *)
| BinOp (MinusPI, e1, Const Cint n1), Const Cint n2 ->
| BinOp (MinusPI, e1, Const (Cint n1)), Const (Cint n2) ->
(e1, Exp.int (n1 ++ n2))
| BinOp (MinusA, Const Cint n1, e1), Const Cint n2 ->
| BinOp (MinusA, Const (Cint n1), e1), Const (Cint n2) ->
(* n1-e1 == n2 -> e1==n1-n2 *)
(e1, Exp.int (n1 -- n2))
| Lfield (e1', fld1, _), Lfield (e2', fld2, _) ->
@ -1279,7 +1279,7 @@ module Normalize = struct
in
let handle_unary_negation (e1: Exp.t) (e2: Exp.t) =
match (e1, e2) with
| (UnOp (LNot, e1', _), Const Cint i | Const Cint i, UnOp (LNot, e1', _))
| (UnOp (LNot, e1', _), Const (Cint i) | Const (Cint i), UnOp (LNot, e1', _))
when IntLit.iszero i ->
(e1', Exp.zero, true)
| _ ->
@ -1316,15 +1316,15 @@ module Normalize = struct
let normalize_and_strengthen_atom tenv (p: normal t) (a: Sil.atom) : Sil.atom =
let a' = atom_normalize tenv (`Exp p.sub) a in
match a' with
| Aeq (BinOp (Le, Var id, Const Cint n), Const Cint i) when IntLit.isone i ->
| Aeq (BinOp (Le, Var id, Const (Cint n)), Const (Cint i)) when IntLit.isone i ->
let lower = Exp.int (n -- IntLit.one) in
let a_lower : Sil.atom = Aeq (BinOp (Lt, lower, Var id), Exp.one) in
if not (List.mem ~equal:Sil.equal_atom p.pi a_lower) then a' else Aeq (Var id, Exp.int n)
| Aeq (BinOp (Lt, Const Cint n, Var id), Const Cint i) when IntLit.isone i ->
| Aeq (BinOp (Lt, Const (Cint n), Var id), Const (Cint i)) when IntLit.isone i ->
let upper = Exp.int (n ++ IntLit.one) in
let a_upper : Sil.atom = Aeq (BinOp (Le, Var id, upper), Exp.one) in
if not (List.mem ~equal:Sil.equal_atom p.pi a_upper) then a' else Aeq (Var id, upper)
| Aeq (BinOp (Ne, e1, e2), Const Cint i) when IntLit.isone i ->
| Aeq (BinOp (Ne, e1, e2), Const (Cint i)) when IntLit.isone i ->
Aneq (e1, e2)
| _ ->
a'
@ -1347,11 +1347,14 @@ module Normalize = struct
let cnt' = strexp_normalize tenv sub cnt in
if phys_equal cnt cnt' then x else (fld, cnt') )
in
if phys_equal fld_cnts fld_cnts'
&& List.is_sorted ~compare:[%compare : Typ.Fieldname.t * Sil.strexp] fld_cnts
if
phys_equal fld_cnts fld_cnts'
&& List.is_sorted ~compare:[%compare : Typ.Fieldname.t * Sil.strexp] fld_cnts
then se
else
let fld_cnts'' = List.sort ~cmp:[%compare : Typ.Fieldname.t * Sil.strexp] fld_cnts' in
let fld_cnts'' =
List.sort ~compare:[%compare : Typ.Fieldname.t * Sil.strexp] fld_cnts'
in
Estruct (fld_cnts'', inst) )
| Earray (len, idx_cnts, inst) ->
let len' = exp_normalize_noabs tenv sub len in
@ -1367,11 +1370,12 @@ module Normalize = struct
let cnt' = strexp_normalize tenv sub cnt in
if phys_equal idx idx' && phys_equal cnt cnt' then x else (idx', cnt') )
in
if phys_equal idx_cnts idx_cnts'
&& List.is_sorted ~compare:[%compare : Exp.t * Sil.strexp] idx_cnts
if
phys_equal idx_cnts idx_cnts'
&& List.is_sorted ~compare:[%compare : Exp.t * Sil.strexp] idx_cnts
then se
else
let idx_cnts'' = List.sort ~cmp:[%compare : Exp.t * Sil.strexp] idx_cnts' in
let idx_cnts'' = List.sort ~compare:[%compare : Exp.t * Sil.strexp] idx_cnts' in
Earray (len', idx_cnts'', inst)
@ -1533,20 +1537,20 @@ module Normalize = struct
and hpara_normalize tenv (para: Sil.hpara) =
let normalized_body = List.map ~f:(hpred_normalize tenv Sil.sub_empty) para.body in
let sorted_body = List.sort ~cmp:Sil.compare_hpred normalized_body in
let sorted_body = List.sort ~compare:Sil.compare_hpred normalized_body in
{para with body= sorted_body}
and hpara_dll_normalize tenv (para: Sil.hpara_dll) =
let normalized_body = List.map ~f:(hpred_normalize tenv Sil.sub_empty) para.body_dll in
let sorted_body = List.sort ~cmp:Sil.compare_hpred normalized_body in
let sorted_body = List.sort ~compare:Sil.compare_hpred normalized_body in
{para with body_dll= sorted_body}
let sigma_normalize tenv sub sigma =
let sigma' =
List.map ~f:(hpred_normalize tenv sub) sigma |> make_captured_in_closures_consistent
|> List.stable_sort ~cmp:Sil.compare_hpred
|> List.stable_sort ~compare:Sil.compare_hpred
in
if equal_sigma sigma sigma' then sigma else sigma'
@ -1555,7 +1559,11 @@ module Normalize = struct
let ineq_list, nonineq_list = List.partition_tf ~f:atom_is_inequality pi in
let diseq_list =
let get_disequality_info acc (a: Sil.atom) =
match a with Aneq (Const Cint n, e) | Aneq (e, Const Cint n) -> (e, n) :: acc | _ -> acc
match a with
| Aneq (Const (Cint n), e) | Aneq (e, Const (Cint n)) ->
(e, n) :: acc
| _ ->
acc
in
List.fold ~f:get_disequality_info ~init:[] nonineq_list
in
@ -1607,7 +1615,7 @@ module Normalize = struct
List.filter
~f:(fun (a: Sil.atom) ->
match a with
| Aneq (Const Cint n, e) | Aneq (e, Const Cint n) ->
| Aneq (Const (Cint n), e) | Aneq (e, Const (Cint n)) ->
not
(List.exists
~f:(fun (e', n') -> Exp.equal e e' && IntLit.lt n' n)
@ -1641,7 +1649,7 @@ module Normalize = struct
let filter_useful_atom : Sil.atom -> bool =
let unsigned_exps = lazy (sigma_get_unsigned_exps sigma) in
function
| Aneq ((Var _ as e), Const Cint n) when IntLit.isnegative n ->
| Aneq ((Var _ as e), Const (Cint n)) when IntLit.isnegative n ->
not (List.exists ~f:(Exp.equal e) (Lazy.force unsigned_exps))
| Aneq (e1, e2) ->
not (syntactically_different (e1, e2))
@ -1651,7 +1659,7 @@ module Normalize = struct
true
in
let pi' =
List.stable_sort ~cmp:Sil.compare_atom
List.stable_sort ~compare:Sil.compare_atom
(List.filter ~f:filter_useful_atom nonineq_list @ ineq_list)
in
let pi'' = pi_sorted_remove_redundant pi' in
@ -1891,7 +1899,7 @@ let sigma_get_start_lexps_sort sigma =
let exp_compare_neg e1 e2 = -Exp.compare e1 e2 in
let filter e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
let lexps = Sil.hpred_list_get_lexps filter sigma in
List.sort ~cmp:exp_compare_neg lexps
List.sort ~compare:exp_compare_neg lexps
let sigma_dfs_sort tenv sigma =
@ -1982,7 +1990,7 @@ let sigma_get_array_indices sigma =
let compute_reindexing_from_indices list =
let get_id_offset (e: Exp.t) =
match e with
| BinOp (PlusA, Var id, Const Cint offset) ->
| BinOp (PlusA, Var id, Const (Cint offset)) ->
if Ident.is_primed id then Some (id, offset) else None
| _ ->
None
@ -2042,7 +2050,7 @@ let prop_rename_array_indices tenv prop =
let indices = sigma_get_array_indices prop.sigma in
let not_same_base_lt_offsets (e1: Exp.t) (e2: Exp.t) =
match (e1, e2) with
| BinOp (PlusA, e1', Const Cint n1'), BinOp (PlusA, e2', Const Cint n2') ->
| BinOp (PlusA, e1', Const (Cint n1')), BinOp (PlusA, e2', Const (Cint n2')) ->
not (Exp.equal e1' e2' && IntLit.lt n1' n2')
| _ ->
true
@ -2081,12 +2089,12 @@ let compute_renaming free_vars =
let rec idlist_assoc id = function
| [] ->
raise Not_found
raise Caml.Not_found
| (i, x) :: l ->
if Ident.equal i id then x else idlist_assoc id l
let ident_captured_ren ren id = try idlist_assoc id ren with Not_found -> id
let ident_captured_ren ren id = try idlist_assoc id ren with Caml.Not_found -> id
(* If not defined in ren, id should be mapped to itself *)
@ -2322,7 +2330,7 @@ type 'a prop_iter =
; pit_pi: pi (** pure part *)
; pit_newpi: (bool * Sil.atom) list (** newly added atoms. *)
; (* The first records !Config.footprint. *)
pit_old: sigma (** sigma already visited *)
pit_old: sigma (** sigma already visited *)
; pit_curr: Sil.hpred (** current element *)
; pit_state: 'a (** state of current element *)
; pit_new: sigma (** sigma not yet visited *)

2
infer/src/biabduction/Prop.mli
Unescape View File

@ -36,7 +36,7 @@ type 'a t = private
; pi: pi (** pure part *)
; sigma_fp: sigma (** abduced spatial part *)
; pi_fp: pi (** abduced pure part *) }
[@@deriving compare]
[@@deriving compare]
(** type to describe different strategies for initializing fields of a structure. [No_init] does not
initialize any fields of the struct. [Fld_init] initializes the fields of the struct with fresh

20
infer/src/biabduction/Propgraph.ml
Unescape View File

@ -28,15 +28,15 @@ let edge_is_hpred = function Ehpred _ -> true | Eatom _ -> false | Esub_entry _
(** Return the source of the edge *)
let edge_get_source = function
| Ehpred Sil.Hpointsto (e, _, _) ->
| Ehpred (Sil.Hpointsto (e, _, _)) ->
Some e
| Ehpred Sil.Hlseg (_, _, e, _, _) ->
| Ehpred (Sil.Hlseg (_, _, e, _, _)) ->
Some e
| Ehpred Sil.Hdllseg (_, _, e1, _, _, _, _) ->
| Ehpred (Sil.Hdllseg (_, _, e1, _, _, _, _)) ->
Some e1 (* only one direction supported for now *)
| Eatom Sil.Aeq (e1, _) ->
| Eatom (Sil.Aeq (e1, _)) ->
Some e1
| Eatom Sil.Aneq (e1, _) ->
| Eatom (Sil.Aneq (e1, _)) ->
Some e1
| Eatom (Sil.Apred (_, e :: _) | Anpred (_, e :: _)) ->
Some e
@ -155,14 +155,14 @@ and compute_esel_diff esel1 esel2 : Obj.t list =
(** Compute the subobjects in [newedge] which are different from those in [oldedge] *)
let compute_edge_diff (oldedge: edge) (newedge: edge) : Obj.t list =
match (oldedge, newedge) with
| Ehpred Sil.Hpointsto (_, se1, e1), Ehpred Sil.Hpointsto (_, se2, e2) ->
| Ehpred (Sil.Hpointsto (_, se1, e1)), Ehpred (Sil.Hpointsto (_, se2, e2)) ->
compute_sexp_diff se1 se2 @ compute_exp_diff e1 e2
| Eatom Sil.Aeq (_, e1), Eatom Sil.Aeq (_, e2) ->
| Eatom (Sil.Aeq (_, e1)), Eatom (Sil.Aeq (_, e2)) ->
compute_exp_diff e1 e2
| Eatom Sil.Aneq (_, e1), Eatom Sil.Aneq (_, e2) ->
| Eatom (Sil.Aneq (_, e1)), Eatom (Sil.Aneq (_, e2)) ->
compute_exp_diff e1 e2
| Eatom Sil.Apred (_, es1), Eatom Sil.Apred (_, es2)
| Eatom Sil.Anpred (_, es1), Eatom Sil.Anpred (_, es2) ->
| Eatom (Sil.Apred (_, es1)), Eatom (Sil.Apred (_, es2))
| Eatom (Sil.Anpred (_, es1)), Eatom (Sil.Anpred (_, es2)) ->
List.concat (try List.map2_exn ~f:compute_exp_diff es1 es2 with Invalid_argument _ -> [])
| Esub_entry (_, e1), Esub_entry (_, e2) ->
compute_exp_diff e1 e2

168
infer/src/biabduction/Prover.ml
Unescape View File

@ -20,9 +20,9 @@ let decrease_indent_when_exception thunk =
IExn.reraise_after exn ~f:(fun () -> L.d_decrease_indent 1)
let compute_max_from_nonempty_int_list l = uw (List.max_elt ~cmp:IntLit.compare_value l)
let compute_max_from_nonempty_int_list l = uw (List.max_elt ~compare:IntLit.compare_value l)
let compute_min_from_nonempty_int_list l = uw (List.min_elt ~cmp:IntLit.compare_value l)
let compute_min_from_nonempty_int_list l = uw (List.min_elt ~compare:IntLit.compare_value l)
let rec list_rev_acc acc = function [] -> acc | x :: l -> list_rev_acc (x :: acc) l
@ -48,9 +48,9 @@ let rec is_java_class tenv (typ: Typ.t) =
(** Negate an atom *)
let atom_negate tenv = function
| Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const Const.Cint i) when IntLit.isone i ->
| Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
Prop.mk_inequality tenv (Exp.lt e2 e1)
| Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const Const.Cint i) when IntLit.isone i ->
| Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
Prop.mk_inequality tenv (Exp.le e2 e1)
| Sil.Aeq (e1, e2) ->
Sil.Aneq (e1, e2)
@ -100,7 +100,7 @@ end = struct
let from_leq acc (e1, e2) =
match (e1, e2) with
| ( Exp.BinOp (Binop.MinusA, (Exp.Var id11 as e11), (Exp.Var id12 as e12))
, Exp.Const Const.Cint n )
, Exp.Const (Const.Cint n) )
when not (Ident.equal id11 id12) -> (
match IntLit.to_signed n with
| None ->
@ -113,7 +113,8 @@ end = struct
let from_lt acc (e1, e2) =
match (e1, e2) with
| Exp.Const Const.Cint n, Exp.BinOp (Binop.MinusA, (Exp.Var id21 as e21), (Exp.Var id22 as e22))
| ( Exp.Const (Const.Cint n)
, Exp.BinOp (Binop.MinusA, (Exp.Var id21 as e21), (Exp.Var id22 as e22)) )
when not (Ident.equal id21 id22) -> (
match IntLit.to_signed n with
| None ->
@ -144,7 +145,7 @@ end = struct
let sort_then_remove_redundancy constraints =
let constraints_sorted = List.sort ~cmp:compare constraints in
let constraints_sorted = List.sort ~compare constraints in
let have_same_key (e1, e2, _) (f1, f2, _) =
[%compare.equal : Exp.t * Exp.t] (e1, e2) (f1, f2)
in
@ -303,10 +304,10 @@ end = struct
let leqs_sort_then_remove_redundancy leqs =
let leqs_sorted = List.sort ~cmp:leq_compare leqs in
let leqs_sorted = List.sort ~compare:leq_compare leqs in
let have_same_key leq1 leq2 =
match (leq1, leq2) with
| (e1, Exp.Const Const.Cint n1), (e2, Exp.Const Const.Cint n2) ->
| (e1, Exp.Const (Const.Cint n1)), (e2, Exp.Const (Const.Cint n2)) ->
Exp.equal e1 e2 && IntLit.leq n1 n2
| _, _ ->
false
@ -315,10 +316,10 @@ end = struct
let lts_sort_then_remove_redundancy lts =
let lts_sorted = List.sort ~cmp:lt_compare lts in
let lts_sorted = List.sort ~compare:lt_compare lts in
let have_same_key lt1 lt2 =
match (lt1, lt2) with
| (Exp.Const Const.Cint n1, e1), (Exp.Const Const.Cint n2, e2) ->
| (Exp.Const (Const.Cint n1), e1), (Exp.Const (Const.Cint n2), e2) ->
Exp.equal e1 e2 && IntLit.geq n1 n2
| _, _ ->
false
@ -337,18 +338,18 @@ end = struct
try
let old_upper = Exp.Map.find e umap in
if IntLit.leq old_upper new_upper then umap else Exp.Map.add e new_upper umap
with Not_found -> Exp.Map.add e new_upper umap
with Caml.Not_found -> Exp.Map.add e new_upper umap
in
let lmap_add lmap e new_lower =
try
let old_lower = Exp.Map.find e lmap in
if IntLit.geq old_lower new_lower then lmap else Exp.Map.add e new_lower lmap
with Not_found -> Exp.Map.add e new_lower lmap
with Caml.Not_found -> Exp.Map.add e new_lower lmap
in
let rec umap_create_from_leqs umap = function
| [] ->
umap
| (e1, Exp.Const Const.Cint upper1) :: leqs_rest ->
| (e1, Exp.Const (Const.Cint upper1)) :: leqs_rest ->
let umap' = umap_add umap e1 upper1 in
umap_create_from_leqs umap' leqs_rest
| _ :: leqs_rest ->
@ -357,7 +358,7 @@ end = struct
let rec lmap_create_from_lts lmap = function
| [] ->
lmap
| (Exp.Const Const.Cint lower1, e1) :: lts_rest ->
| (Exp.Const (Const.Cint lower1), e1) :: lts_rest ->
let lmap' = lmap_add lmap e1 lower1 in
lmap_create_from_lts lmap' lts_rest
| _ :: lts_rest ->
@ -373,7 +374,7 @@ end = struct
let new_upper1 = upper2 ++ n in
let new_umap = umap_add umap e1 new_upper1 in
umap_improve_by_difference_constraints new_umap constrs_rest
with Not_found -> umap_improve_by_difference_constraints umap constrs_rest
with Caml.Not_found -> umap_improve_by_difference_constraints umap constrs_rest
in
let rec lmap_improve_by_difference_constraints lmap = function
| [] ->
@ -386,7 +387,7 @@ end = struct
let new_lower2 = lower1 -- n -- IntLit.one in
let new_lmap = lmap_add lmap e2 new_lower2 in
lmap_improve_by_difference_constraints new_lmap constrs_rest
with Not_found -> lmap_improve_by_difference_constraints lmap constrs_rest
with Caml.Not_found -> lmap_improve_by_difference_constraints lmap constrs_rest
in
let leqs_res =
let umap = umap_create_from_leqs Exp.Map.empty leqs in
@ -419,9 +420,9 @@ end = struct
| Sil.Aneq (e1, e2) ->
(* != *)
neqs := (e1, e2) :: !neqs
| Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const Const.Cint i) when IntLit.isone i ->
| Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
leqs := (e1, e2) :: !leqs (* <= *)
| Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const Const.Cint i) when IntLit.isone i ->
| Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
lts := (e1, e2) :: !lts (* < *)
| Sil.Aeq _ | Sil.Apred _ | Anpred _ ->
()
@ -495,27 +496,28 @@ end = struct
let check_le {leqs; lts; neqs= _} e1 e2 =
(* L.d_str "check_le "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
match (e1, e2) with
| Exp.Const Const.Cint n1, Exp.Const Const.Cint n2 ->
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) ->
IntLit.leq n1 n2
| ( Exp.BinOp (Binop.MinusA, Exp.Sizeof {nbytes= Some nb1}, Exp.Sizeof {nbytes= Some nb2})
, Exp.Const Const.Cint n2 ) ->
, Exp.Const (Const.Cint n2) ) ->
(* [ sizeof(t1) - sizeof(t2) <= n2 ] *)
IntLit.(leq (sub (of_int nb1) (of_int nb2)) n2)
| Exp.BinOp (Binop.MinusA, Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2}), Exp.Const Const.Cint n2
| ( Exp.BinOp (Binop.MinusA, Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2})
, Exp.Const (Const.Cint n2) )
when IntLit.isminusone n2 && type_size_comparable t1 t2 ->
(* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
check_type_size_lt t1 t2
| e, Exp.Const Const.Cint n ->
| e, Exp.Const (Const.Cint n) ->
(* [e <= n' <= n |- e <= n] *)
List.exists
~f:(function
| e', Exp.Const Const.Cint n' -> Exp.equal e e' && IntLit.leq n' n | _, _ -> false)
| e', Exp.Const (Const.Cint n') -> Exp.equal e e' && IntLit.leq n' n | _, _ -> false)
leqs
| Exp.Const Const.Cint n, e ->
| Exp.Const (Const.Cint n), e ->
(* [ n-1 <= n' < e |- n <= e] *)
List.exists
~f:(function
| Exp.Const Const.Cint n', e' ->
| Exp.Const (Const.Cint n'), e' ->
Exp.equal e e' && IntLit.leq (n -- IntLit.one) n'
| _, _ ->
false)
@ -528,19 +530,19 @@ end = struct
let check_lt {leqs; lts; neqs= _} e1 e2 =
(* L.d_str "check_lt "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
match (e1, e2) with
| Exp.Const Const.Cint n1, Exp.Const Const.Cint n2 ->
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) ->
IntLit.lt n1 n2
| Exp.Const Const.Cint n, e ->
| Exp.Const (Const.Cint n), e ->
(* [n <= n' < e |- n < e] *)
List.exists
~f:(function
| Exp.Const Const.Cint n', e' -> Exp.equal e e' && IntLit.leq n n' | _, _ -> false)
| Exp.Const (Const.Cint n'), e' -> Exp.equal e e' && IntLit.leq n n' | _, _ -> false)
lts
| e, Exp.Const Const.Cint n ->
| e, Exp.Const (Const.Cint n) ->
(* [e <= n' <= n-1 |- e < n] *)
List.exists
~f:(function
| e', Exp.Const Const.Cint n' ->
| e', Exp.Const (Const.Cint n') ->
Exp.equal e e' && IntLit.leq n' (n -- IntLit.one)
| _, _ ->
false)
@ -558,16 +560,18 @@ end = struct
(** Find a IntLit.t n such that [t |- e<=n] if possible. *)
let compute_upper_bound {leqs; lts= _; neqs= _} e1 =
match e1 with
| Exp.Const Const.Cint n1 ->
| Exp.Const (Const.Cint n1) ->
Some n1
| _ ->
let e_upper_list =
List.filter
~f:(function e', Exp.Const Const.Cint _ -> Exp.equal e1 e' | _, _ -> false)
~f:(function e', Exp.Const (Const.Cint _) -> Exp.equal e1 e' | _, _ -> false)
leqs
in
let upper_list =
List.map ~f:(function _, Exp.Const Const.Cint n -> n | _ -> assert false) e_upper_list
List.map
~f:(function _, Exp.Const (Const.Cint n) -> n | _ -> assert false)
e_upper_list
in
if List.is_empty upper_list then None
else Some (compute_min_from_nonempty_int_list upper_list)
@ -576,7 +580,7 @@ end = struct
(** Find a IntLit.t n such that [t |- n < e] if possible. *)
let compute_lower_bound {leqs= _; lts; neqs= _} e1 =
match e1 with
| Exp.Const Const.Cint n1 ->
| Exp.Const (Const.Cint n1) ->
Some (n1 -- IntLit.one)
| Exp.Sizeof {nbytes= Some n1} ->
Some (IntLit.of_int n1 -- IntLit.one)
@ -585,11 +589,13 @@ end = struct
| _ ->
let e_lower_list =
List.filter
~f:(function Exp.Const Const.Cint _, e' -> Exp.equal e1 e' | _, _ -> false)
~f:(function Exp.Const (Const.Cint _), e' -> Exp.equal e1 e' | _, _ -> false)
lts
in
let lower_list =
List.map ~f:(function Exp.Const Const.Cint n, _ -> n | _ -> assert false) e_lower_list
List.map
~f:(function Exp.Const (Const.Cint n), _ -> n | _ -> assert false)
e_lower_list
in
if List.is_empty lower_list then None
else Some (compute_max_from_nonempty_int_list lower_list)
@ -634,12 +640,12 @@ let check_equal tenv prop e1_0 e2_0 =
let check_equal () = Exp.equal n_e1 n_e2 in
let check_equal_const () =
match (n_e1, n_e2) with
| Exp.BinOp (Binop.PlusA, e1, Exp.Const Const.Cint d), e2
| e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const Const.Cint d) ->
| Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2
| e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) ->
if Exp.equal e1 e2 then IntLit.iszero d else false
| Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const Const.Cint i) when IntLit.iszero i ->
| Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
Const.equal c1 c2
| Exp.Lindex (Exp.Const c1, Exp.Const Const.Cint i), Exp.Const c2 when IntLit.iszero i ->
| Exp.Lindex (Exp.Const c1, Exp.Const (Const.Cint i)), Exp.Const c2 when IntLit.iszero i ->
Const.equal c1 c2
| _, _ ->
false
@ -688,9 +694,9 @@ let get_bounds tenv prop e0 =
let e_norm = Prop.exp_normalize_prop ~destructive:true tenv prop e0 in
let e_root, off =
match e_norm with
| Exp.BinOp (Binop.PlusA, e, Exp.Const Const.Cint n1) ->
| Exp.BinOp (Binop.PlusA, e, Exp.Const (Const.Cint n1)) ->
(e, IntLit.neg n1)
| Exp.BinOp (Binop.MinusA, e, Exp.Const Const.Cint n1) ->
| Exp.BinOp (Binop.MinusA, e, Exp.Const (Const.Cint n1)) ->
(e, n1)
| _ ->
(e_norm, IntLit.zero)
@ -711,24 +717,24 @@ let check_disequal tenv prop e1 e2 =
match (ce1, ce2) with
| Exp.Const c1, Exp.Const c2 ->
Const.kind_equal c1 c2 && not (Const.equal c1 c2)
| Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const Const.Cint d) ->
| Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const (Const.Cint d)) ->
if IntLit.iszero d then not (Const.equal c1 c2) (* offset=0 is no offset *)
else Const.equal c1 c2
(* same base, different offsets *)
| ( Exp.BinOp (Binop.PlusA, e1, Exp.Const Const.Cint d1)
, Exp.BinOp (Binop.PlusA, e2, Exp.Const Const.Cint d2) ) ->
| ( Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d1))
, Exp.BinOp (Binop.PlusA, e2, Exp.Const (Const.Cint d2)) ) ->
if Exp.equal e1 e2 then IntLit.neq d1 d2 else false
| Exp.BinOp (Binop.PlusA, e1, Exp.Const Const.Cint d), e2
| e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const Const.Cint d) ->
| Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2
| e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) ->
if Exp.equal e1 e2 then not (IntLit.iszero d) else false
| Exp.Lindex (Exp.Const c1, Exp.Const Const.Cint d), Exp.Const c2 ->
| Exp.Lindex (Exp.Const c1, Exp.Const (Const.Cint d)), Exp.Const c2 ->
if IntLit.iszero d then not (Const.equal c1 c2) else Const.equal c1 c2
| Exp.Lindex (Exp.Const c1, Exp.Const d1), Exp.Lindex (Exp.Const c2, Exp.Const d2) ->
Const.equal c1 c2 && not (Const.equal d1 d2)
| Exp.Const Const.Cint n, Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21)
| Exp.Const Const.Cint n, Exp.BinOp (Binop.Mult, e21, Sizeof _)
| Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21), Exp.Const Const.Cint n
| Exp.BinOp (Binop.Mult, e21, Exp.Sizeof _), Exp.Const Const.Cint n ->
| Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21)
| Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult, e21, Sizeof _)
| Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21), Exp.Const (Const.Cint n)
| Exp.BinOp (Binop.Mult, e21, Exp.Sizeof _), Exp.Const (Const.Cint n) ->
IntLit.iszero n && not (Exp.is_zero e21)
| Exp.Lvar pv0, Exp.Lvar pv1 ->
(* Addresses of any two local vars must be different *)
@ -736,7 +742,7 @@ let check_disequal tenv prop e1 e2 =
| Exp.Lvar pv, Exp.Var id | Exp.Var id, Exp.Lvar pv ->
(* Address of any non-global var must be different from the value of any footprint var *)
not (Pvar.is_global pv) && Ident.is_footprint id
| Exp.Lvar _, Exp.Const Const.Cint _ | Exp.Const Const.Cint _, Exp.Lvar _ ->
| Exp.Lvar _, Exp.Const (Const.Cint _) | Exp.Const (Const.Cint _), Exp.Lvar _ ->
(* Comparing pointer with nonzero integer is undefined behavior in ISO C++ *)
(* Assume they are not equal *)
true
@ -778,7 +784,7 @@ let check_disequal tenv prop e1 e2 =
else
let sigma_rest' = List.rev_append sigma_irrelevant sigma_rest in
f [] e2 sigma_rest' )
| (Sil.Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _)) :: sigma_rest ->
| Sil.Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _) :: sigma_rest ->
if is_root tenv prop iF e <> None || is_root tenv prop iB e <> None then
let sigma_irrelevant' = List.rev_append sigma_irrelevant sigma_rest in
Some (true, sigma_irrelevant')
@ -827,7 +833,7 @@ let check_le_normalized tenv prop e1 e2 =
(* L.d_str "check_le_normalized "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
let eL, eR, off =
match (e1, e2) with
| Exp.BinOp (Binop.MinusA, f1, f2), Exp.Const Const.Cint n ->
| Exp.BinOp (Binop.MinusA, f1, f2), Exp.Const (Const.Cint n) ->
if Exp.equal f1 f2 then (Exp.zero, Exp.zero, n) else (f1, f2, n)
| _ ->
(e1, e2, IntLit.zero)
@ -898,9 +904,9 @@ let check_atom tenv prop a0 =
(Prop.pp_prop Pp.text) prop_no_fp ;
Out_channel.close outc ) ;
match a with
| Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const Const.Cint i) when IntLit.isone i ->
| Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
check_le_normalized tenv prop e1 e2
| Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const Const.Cint i) when IntLit.isone i ->
| Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
check_lt_normalized tenv prop e1 e2
| Sil.Aeq (e1, e2) ->
check_equal tenv prop e1 e2
@ -922,8 +928,9 @@ let check_allocatedness tenv prop e =
is_root tenv prop e1 n_e <> None
else false
| Sil.Hdllseg (k, _, iF, oB, oF, iB, _) ->
if Sil.equal_lseg_kind k Sil.Lseg_NE || check_disequal tenv prop iF oF
|| check_disequal tenv prop iB oB
if
Sil.equal_lseg_kind k Sil.Lseg_NE || check_disequal tenv prop iF oF
|| check_disequal tenv prop iB oB
then is_root tenv prop iF n_e <> None || is_root tenv prop iB n_e <> None
else false
in
@ -941,7 +948,7 @@ let check_inconsistency_two_hpreds tenv prop =
if Exp.equal e1 e then true else f e (hpred :: sigma_seen) sigma_rest
| (Sil.Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _) as hpred) :: sigma_rest ->
if Exp.equal iF e || Exp.equal iB e then true else f e (hpred :: sigma_seen) sigma_rest
| (Sil.Hlseg (Sil.Lseg_PE, _, e1, Exp.Const Const.Cint i, _) as hpred) :: sigma_rest
| (Sil.Hlseg (Sil.Lseg_PE, _, e1, Exp.Const (Const.Cint i), _) as hpred) :: sigma_rest
when IntLit.iszero i ->
if Exp.equal e1 e then true else f e (hpred :: sigma_seen) sigma_rest
| (Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) as hpred) :: sigma_rest ->
@ -952,7 +959,7 @@ let check_inconsistency_two_hpreds tenv prop =
let e_new = Prop.exp_normalize_prop ~destructive:true tenv prop_new e in
f e_new [] sigma_new
else f e (hpred :: sigma_seen) sigma_rest
| (Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Exp.Const Const.Cint i, _, _) as hpred) :: sigma_rest
| (Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Exp.Const (Const.Cint i), _, _) as hpred) :: sigma_rest
when IntLit.iszero i ->
if Exp.equal e1 e then true else f e (hpred :: sigma_seen) sigma_rest
| (Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, e3, _, _) as hpred) :: sigma_rest ->
@ -1240,8 +1247,9 @@ end = struct
let d_missing sub =
(* optional print of missing: if print something, prepend with newline *)
if !missing_pi <> [] || !missing_sigma <> [] || !missing_fld <> [] || !missing_typ <> []
|| not (Sil.is_sub_empty sub)
if
!missing_pi <> [] || !missing_sigma <> [] || !missing_fld <> [] || !missing_typ <> []
|| not (Sil.is_sub_empty sub)
then ( L.d_ln () ; L.d_str "[" ; d_missing_ sub ; L.d_str "]" )
@ -1366,8 +1374,9 @@ let exp_imply tenv calc_missing (subs: subst2) e1_in e2_in : subst2 =
| e1, Exp.Var v2 ->
let occurs_check v e =
(* check whether [v] occurs in normalized [e] *)
if Exp.ident_mem e v
&& Exp.ident_mem (Prop.exp_normalize_prop ~destructive:true tenv Prop.prop_emp e) v
if
Exp.ident_mem e v
&& Exp.ident_mem (Prop.exp_normalize_prop ~destructive:true tenv Prop.prop_emp e) v
then raise (IMPL_EXC ("occurs check", subs, EXC_FALSE_EXPS (e1, e2)))
in
if Ident.is_primed v2 then
@ -1405,10 +1414,10 @@ let exp_imply tenv calc_missing (subs: subst2) e1_in e2_in : subst2 =
| Exp.Const c1, Exp.Const c2 ->
if Const.equal c1 c2 then subs
else raise (IMPL_EXC ("constants not equal", subs, EXC_FALSE_EXPS (e1, e2)))
| Exp.Const Const.Cint _, Exp.BinOp (Binop.PlusPI, _, _) ->
| Exp.Const (Const.Cint _), Exp.BinOp (Binop.PlusPI, _, _) ->
raise
(IMPL_EXC ("pointer+index cannot evaluate to a constant", subs, EXC_FALSE_EXPS (e1, e2)))
| Exp.Const Const.Cint n1, Exp.BinOp (Binop.PlusA, f1, Exp.Const Const.Cint n2) ->
| Exp.Const (Const.Cint n1), Exp.BinOp (Binop.PlusA, f1, Exp.Const (Const.Cint n2)) ->
do_imply subs (Exp.int (n1 -- n2)) f1
| Exp.BinOp (op1, e1, f1), Exp.BinOp (op2, e2, f2) when Binop.equal op1 op2 ->
do_imply (do_imply subs e1 e2) f1 f2
@ -1424,10 +1433,10 @@ let exp_imply tenv calc_missing (subs: subst2) e1_in e2_in : subst2 =
, Exp.Sizeof {typ= t2; dynamic_length= Some d2; subtype= st2} )
when Typ.equal t1 t2 && Exp.equal d1 d2 && Subtype.equal_modulo_flag st1 st2 ->
subs
| e', Exp.Const Const.Cint n
| e', Exp.Const (Const.Cint n)
when IntLit.iszero n && check_disequal tenv Prop.prop_emp e' Exp.zero ->
raise (IMPL_EXC ("expressions not equal", subs, EXC_FALSE_EXPS (e1, e2)))
| Exp.Const Const.Cint n, e'
| Exp.Const (Const.Cint n), e'
when IntLit.iszero n && check_disequal tenv Prop.prop_emp e' Exp.zero ->
raise (IMPL_EXC ("expressions not equal", subs, EXC_FALSE_EXPS (e1, e2)))
| e1, Exp.Const _ ->
@ -1460,9 +1469,9 @@ let path_to_id path =
match f e with None -> None | Some s -> Some (s ^ "_" ^ Exp.to_string ind) )
| Exp.Lvar _ ->
Some (Exp.to_string path)
| Exp.Const Const.Cstr s ->
| Exp.Const (Const.Cstr s) ->
Some ("_const_str_" ^ s)
| Exp.Const Const.Cclass c ->
| Exp.Const (Const.Cclass c) ->
Some ("_const_class_" ^ Ident.name_to_string c)
| Exp.Const _ ->
None
@ -1928,8 +1937,9 @@ let cast_exception tenv texp1 texp2 e1 subs =
let _ =
match (texp1, texp2) with
| Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2; subtype= st2} ->
if Config.developer_mode
|| Subtype.is_cast st2 && not (Subtyping_check.check_subtype tenv t1 t2)
if
Config.developer_mode
|| (Subtype.is_cast st2 && not (Subtyping_check.check_subtype tenv t1 t2))
then ProverState.checks := Class_cast_check (texp1, texp2, e1) :: !ProverState.checks
| _ ->
()
@ -1957,8 +1967,8 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
| Exp.Sizeof {typ= typ1}, Exp.Sizeof {typ= typ2} -> (
match (typ1.desc, typ2.desc) with
| (Tstruct _ | Tarray _), (Tstruct _ | Tarray _) ->
is_java_class tenv typ1 || Typ.is_cpp_class typ1 && Typ.is_cpp_class typ2
|| Typ.is_objc_class typ1 && Typ.is_objc_class typ2
is_java_class tenv typ1 || (Typ.is_cpp_class typ1 && Typ.is_cpp_class typ2)
|| (Typ.is_objc_class typ1 && Typ.is_objc_class typ2)
| _ ->
false )
| _ ->
@ -2312,9 +2322,9 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
-> (
let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in
match e2 with
| Exp.Const Const.Cstr s ->
| Exp.Const (Const.Cstr s) ->
Some (s, true)
| Exp.Const Const.Cclass c ->
| Exp.Const (Const.Cclass c) ->
Some (Ident.name_to_string c, false)
| _ ->
None )
@ -2709,7 +2719,7 @@ exception NO_COVER
let find_minimum_pure_cover tenv cases =
let cases =
let compare (pi1, _) (pi2, _) = Int.compare (List.length pi1) (List.length pi2) in
List.sort ~cmp:compare cases
List.sort ~compare cases
in
let rec grow seen todo =
match todo with

Some files were not shown because too many files have changed in this diff Show More

Write Preview
Loading…
Cancel
Save