infer_clone/infer/src/pulse/PulseInvalidation.mli

(*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

open! IStd
module F = Format

type std_vector_function =
  | Assign
  | Clear
  | Emplace
  | EmplaceBack
  | Insert
  | PushBack
  | Reserve
  | ShrinkToFit
[@@deriving compare]

val pp_std_vector_function : F.formatter -> std_vector_function -> unit

type java_iterator_function = Remove [@@deriving compare]

type t =
  | CFree
  | ConstantDereference of IntLit.t
  | CppDelete
  | EndIterator
  | GoneOutOfScope of Pvar.t * Typ.t
  | StdVector of std_vector_function
  | JavaIterator of java_iterator_function
[@@deriving compare]

val pp : F.formatter -> t -> unit

val issue_type_of_cause : t -> IssueType.t

val describe : F.formatter -> t -> unit
[pulse][2/9] add PulseInvalidation to PulseBasicInterface Summary: See explanations in D17955104 Reviewed By: ezgicicek Differential Revision: D17955286 fbshipit-source-id: 831491e47 5 years ago			`(*`
			`* Copyright (c) Facebook, Inc. and its affiliates.`
			`*`
			`* This source code is licensed under the MIT license found in the`
			`* LICENSE file in the root directory of this source tree.`
			`*)`

			`open! IStd`
			`module F = Format`

			`type std_vector_function =`
			`\| Assign`
			`\| Clear`
			`\| Emplace`
			`\| EmplaceBack`
			`\| Insert`
			`\| PushBack`
			`\| Reserve`
			`\| ShrinkToFit`
			`[@@deriving compare]`

			`val pp_std_vector_function : F.formatter -> std_vector_function -> unit`

[pulse] Brush up Java iterator models Summary: Java's iterator models were wrong. This causes `VECTOR_INVALIDATION` errors in fbandroid projects. This diff aims to fix it by modeling Java iterators with a current pointer and an underlying collection array. Reviewed By: skcho Differential Revision: D21448322 fbshipit-source-id: 7d44354b5 5 years ago			`type java_iterator_function = Remove [@@deriving compare]`

[pulse][2/9] add PulseInvalidation to PulseBasicInterface Summary: See explanations in D17955104 Reviewed By: ezgicicek Differential Revision: D17955286 fbshipit-source-id: 831491e47 5 years ago			`type t =`
			`\| CFree`
[pulse] report dereference of NULL and constants Summary: Note: Disabled by default. Having some support for values, we can report when a null or constant value is being dereferenced. The particularity here is that we don't report when 0 is a possible value for the address, or even if we know that the value of the address can only be 0 in that branch! Instead, we allow ourselves to report only when we the address has been set to NULL (or any constant). This is in line with how pulse deals with other issues: only report when 1. we see an address become invalid, and 2. we see the same address be used later on Reviewed By: skcho Differential Revision: D17665468 fbshipit-source-id: f1ccf94cf 5 years ago			`\| ConstantDereference of IntLit.t`
[pulse][2/9] add PulseInvalidation to PulseBasicInterface Summary: See explanations in D17955104 Reviewed By: ezgicicek Differential Revision: D17955286 fbshipit-source-id: 831491e47 5 years ago			`\| CppDelete`
[pulse] Modeling std::vector::end() Summary: It is undefined behavior to dereference end iterator. To catch end iterator dereferencing issues we change iterator model: instead of having `internal pointer` storing the current index, we model it as a pointer to a current index. This allows us to model `end()` iterator as having an invalid pointer and there is no need to create an invalidated element in the vector itself. Reviewed By: ezgicicek Differential Revision: D21178441 fbshipit-source-id: fd6a94b0b 5 years ago			`\| EndIterator`
[pulse][2/9] add PulseInvalidation to PulseBasicInterface Summary: See explanations in D17955104 Reviewed By: ezgicicek Differential Revision: D17955286 fbshipit-source-id: 831491e47 5 years ago			`\| GoneOutOfScope of Pvar.t * Typ.t`
			`\| StdVector of std_vector_function`
[pulse] Brush up Java iterator models Summary: Java's iterator models were wrong. This causes `VECTOR_INVALIDATION` errors in fbandroid projects. This diff aims to fix it by modeling Java iterators with a current pointer and an underlying collection array. Reviewed By: skcho Differential Revision: D21448322 fbshipit-source-id: 7d44354b5 5 years ago			`\| JavaIterator of java_iterator_function`
[pulse][2/9] add PulseInvalidation to PulseBasicInterface Summary: See explanations in D17955104 Reviewed By: ezgicicek Differential Revision: D17955286 fbshipit-source-id: 831491e47 5 years ago			`[@@deriving compare]`

			`val pp : F.formatter -> t -> unit`

			`val issue_type_of_cause : t -> IssueType.t`

			`val describe : F.formatter -> t -> unit`