You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
55 lines
1.5 KiB
55 lines
1.5 KiB
7 years ago
|
(*
|
||
|
|
* Copyright (c) 2018-present, Facebook, Inc.
|
||
|
|
*
|
||
|
|
* This source code is licensed under the MIT license found in the
|
||
|
|
* LICENSE file in the root directory of this source tree.
|
||
|
|
*)
|
||
|
|
|
||
|
|
open! IStd
|
||
|
|
open! AbstractDomain.Types
|
||
|
|
module ItvPure = Itv.ItvPure
|
||
|
|
module Relation = BufferOverrunDomainRelation
|
||
|
|
module ValTraceSet = BufferOverrunTrace.Set
|
||
|
|
|
||
|
|
module Condition : sig
|
||
|
|
type t
|
||
|
|
end
|
||
|
|
|
||
|
|
module ConditionTrace : sig
|
||
|
|
type t
|
||
|
|
|
||
|
|
val get_report_location : t -> Location.t
|
||
|
|
|
||
|
|
val get_val_traces : t -> ValTraceSet.t
|
||
|
|
end
|
||
|
|
|
||
|
|
module ConditionSet : sig
|
||
|
|
type t
|
||
|
|
|
||
|
|
val empty : t
|
||
|
|
|
||
|
|
val pp : Format.formatter -> t -> unit
|
||
|
|
|
||
|
|
val pp_summary : Format.formatter -> t -> unit
|
||
|
|
|
||
|
|
val add_array_access :
|
||
|
|
Location.t -> idx:ItvPure.astate -> size:ItvPure.astate -> is_collection_add:bool
|
||
|
|
-> idx_sym_exp:Relation.SymExp.t option -> size_sym_exp:Relation.SymExp.t option
|
||
|
|
-> relation:Relation.astate -> ValTraceSet.t -> t -> t
|
||
|
|
|
||
|
|
val add_alloc_size : Location.t -> length:ItvPure.astate -> ValTraceSet.t -> t -> t
|
||
|
|
|
||
|
|
val join : t -> t -> t
|
||
|
|
|
||
|
|
val subst :
|
||
|
|
t -> Bounds.Bound.t bottom_lifted Symb.SymbolMap.t * ValTraceSet.t Symb.SymbolMap.t
|
||
|
|
-> Relation.SubstMap.t -> Relation.astate -> Typ.Procname.t -> Location.t -> t
|
||
|
|
|
||
|
|
val check_all : report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> t -> t
|
||
|
|
(** Check the conditions, call [report] on those that trigger an issue, returns those that needs to be propagated to callers. *)
|
||
|
|
|
||
|
|
val forget_locs : AbsLoc.PowLoc.t -> t -> t
|
||
|
|
end
|
||
|
|
|
||
|
|
val description : Condition.t -> ConditionTrace.t -> string
|