Summary: Other checkers are going to start using these, so they shouldn't live in the Quandary directory anymore Reviewed By: jvillard Differential Revision: D4124654 fbshipit-source-id: b1d5bddmaster
parent
8c481d2d9f
commit
ae5f8eff0d
@ -0,0 +1,28 @@
|
|||||||
|
(*
|
||||||
|
* Copyright (c) 2016 - present Facebook, Inc.
|
||||||
|
* All rights reserved.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the BSD style license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree. An additional grant
|
||||||
|
* of patent rights can be found in the PATENTS file in the same directory.
|
||||||
|
*)
|
||||||
|
|
||||||
|
type 'a parameter =
|
||||||
|
{ sink : 'a;
|
||||||
|
(** sink type of the parameter *)
|
||||||
|
index : int;
|
||||||
|
(** index of the parameter *)
|
||||||
|
report_reachable : bool;
|
||||||
|
(** if true, report if *any* value heap-reachable from the sink parameter is a source.
|
||||||
|
if false, report only if the value passed to the sink is itself a source *)
|
||||||
|
}
|
||||||
|
|
||||||
|
val make_sink_param : 'a -> int -> report_reachable:bool -> 'a parameter
|
||||||
|
|
||||||
|
|
||||||
|
module type S = sig
|
||||||
|
include TraceElem.S
|
||||||
|
|
||||||
|
(** return the parameter index and sink kind for the given call site with the given actuals *)
|
||||||
|
val get : CallSite.t -> (Exp.t * Typ.t) list -> t parameter list
|
||||||
|
end
|
Loading…
Reference in new issue