From 94d7a0047e85ab59eb9e43869d7956a9d6af431f Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 15 Jul 2024 09:30:33 -0700 Subject: [PATCH] add category for SIOF Summary: Set the category for SIOF issues, namely Memory Error, which is the same as reads of uninitialised values. Reviewed By: ngorogiannis Differential Revision: D59757393 fbshipit-source-id: 64e51a8446f0677882ec575f2eaaa32f44f3ef65 --- infer/src/base/IssueType.ml | 2 +- website/docs/all-categories.md | 1 + website/docs/all-issue-types.md | 2 +- .../static/odoc/next/infer/BO/BiabductionProp/index.html | 2 ++ .../next/infer/Checkers/Lineage/Unified/Dot/index.html | 2 ++ .../infer/Checkers/Lineage/Unified/UVertex/index.html | 5 +++++ .../odoc/next/infer/Checkers/Lineage/Unified/index.html | 6 ++++++ .../odoc/next/infer/IBase/EarlyScubaLogging/index.html | 2 ++ .../PulseAbductiveDomain/AddressAttributes/index.html | 3 +++ .../PulseAbductiveDomain/CanonValue/Attributes/index.html | 5 ++++- .../infer/Pulselib/PulseAttribute/Attributes/index.html | 2 +- .../next/infer/Pulselib/PulseAttribute/Builder/index.html | 2 ++ .../odoc/next/infer/Pulselib/PulseAttribute/index.html | 2 +- .../infer/Pulselib/PulseBaseAddressAttributes/index.html | 8 +++++++- .../PulseBaseAddressAttributes/module-type-S/index.html | 5 ++++- .../Pulselib/PulseCanonValue/Make/Attributes/index.html | 5 ++++- .../PulseCanonValue/module-type-S/Attributes/index.html | 5 ++++- .../odoc/next/infer/Pulselib/PulseInterproc/index.html | 2 +- .../next/infer/Pulselib/PulseModelsDSL/Syntax/index.html | 2 +- 19 files changed, 52 insertions(+), 11 deletions(-) create mode 100644 website/static/odoc/next/infer/BO/BiabductionProp/index.html create mode 100644 website/static/odoc/next/infer/Checkers/Lineage/Unified/Dot/index.html create mode 100644 website/static/odoc/next/infer/Checkers/Lineage/Unified/UVertex/index.html create mode 100644 website/static/odoc/next/infer/Checkers/Lineage/Unified/index.html create mode 100644 website/static/odoc/next/infer/IBase/EarlyScubaLogging/index.html create mode 100644 website/static/odoc/next/infer/Pulselib/PulseAttribute/Builder/index.html diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index c52cf21e9fd..bc1812e8355 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -941,7 +941,7 @@ let starvation = let static_initialization_order_fiasco = - register ~category:NoCategory ~id:"STATIC_INITIALIZATION_ORDER_FIASCO" Error SIOF + register ~category:MemoryError ~id:"STATIC_INITIALIZATION_ORDER_FIASCO" Error SIOF ~user_documentation:[%blob "./documentation/issues/STATIC_INITIALIZATION_ORDER_FIASCO.md"] diff --git a/website/docs/all-categories.md b/website/docs/all-categories.md index dd302b6b043..97a0ace6d63 100644 --- a/website/docs/all-categories.md +++ b/website/docs/all-categories.md @@ -34,6 +34,7 @@ Issue types in this category: - [PULSE_REFERENCE_STABILITY](/docs/next/all-issue-types#pulse_reference_stability) - [PULSE_UNINITIALIZED_VALUE](/docs/next/all-issue-types#pulse_uninitialized_value) - [STACK_VARIABLE_ADDRESS_ESCAPE](/docs/next/all-issue-types#stack_variable_address_escape) +- [STATIC_INITIALIZATION_ORDER_FIASCO](/docs/next/all-issue-types#static_initialization_order_fiasco) - [STRONG_SELF_NOT_CHECKED](/docs/next/all-issue-types#strong_self_not_checked) - [USE_AFTER_DELETE](/docs/next/all-issue-types#use_after_delete) - [USE_AFTER_DELETE_LATENT](/docs/next/all-issue-types#use_after_delete_latent) diff --git a/website/docs/all-issue-types.md b/website/docs/all-issue-types.md index 558edb88fd1..b4732dca431 100644 --- a/website/docs/all-issue-types.md +++ b/website/docs/all-issue-types.md @@ -2756,7 +2756,7 @@ include the JAR files in `infer/annotations` for this annotation to work. ## STATIC_INITIALIZATION_ORDER_FIASCO -*Reported as "Static Initialization Order Fiasco" by [siof](/docs/next/checker-siof).* +*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Static Initialization Order Fiasco" by [siof](/docs/next/checker-siof).* This error is reported in C++. It fires when the initialization of a static variable `A`, accesses a static variable `B` from another translation unit diff --git a/website/static/odoc/next/infer/BO/BiabductionProp/index.html b/website/static/odoc/next/infer/BO/BiabductionProp/index.html new file mode 100644 index 00000000000..ce95992a35d --- /dev/null +++ b/website/static/odoc/next/infer/BO/BiabductionProp/index.html @@ -0,0 +1,2 @@ + +BiabductionProp (infer.BO.BiabductionProp)

Module BO.BiabductionProp

val exp_normalize_noabs : IR.Tenv.t -> IR.Exp.t -> IR.Exp.t

Normalize the expression without abstracting complex subexpressions

diff --git a/website/static/odoc/next/infer/Checkers/Lineage/Unified/Dot/index.html b/website/static/odoc/next/infer/Checkers/Lineage/Unified/Dot/index.html new file mode 100644 index 00000000000..69af3557c98 --- /dev/null +++ b/website/static/odoc/next/infer/Checkers/Lineage/Unified/Dot/index.html @@ -0,0 +1,2 @@ + +Dot (infer.Checkers.Lineage.Unified.Dot)

Module Unified.Dot

val output_graph : Stdlib.out_channel -> G.t -> unit
diff --git a/website/static/odoc/next/infer/Checkers/Lineage/Unified/UVertex/index.html b/website/static/odoc/next/infer/Checkers/Lineage/Unified/UVertex/index.html new file mode 100644 index 00000000000..20437c784d5 --- /dev/null +++ b/website/static/odoc/next/infer/Checkers/Lineage/Unified/UVertex/index.html @@ -0,0 +1,5 @@ + +UVertex (infer.Checkers.Lineage.Unified.UVertex)

Module Unified.UVertex

type v =
  1. | Local of Local.t * PPNode.t
  2. | Argument of int * Checkers.LineageShape.StdModules.FieldPath.t
  3. | Return of Checkers.LineageShape.StdModules.FieldPath.t
  4. | Captured of int
  5. | Function
val sexp_of_v : v -> Sexplib0.Sexp.t
val v_of_sexp : Sexplib0.Sexp.t -> v
val compare_v : v -> v -> int
val equal_v : v -> v -> bool
val hash_fold_v : + Ppx_hash_lib.Std.Hash.state -> + v -> + Ppx_hash_lib.Std.Hash.state
val hash_v : v -> Ppx_hash_lib.Std.Hash.hash_value
type t = {
  1. procname : IR.Procname.t;
  2. vertex : v;
}
include Sexplib0.Sexpable.S with type t := t
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
include Ppx_compare_lib.Equal.S with type t := t
val equal : t Base__Ppx_compare_lib.equal
include Ppx_hash_lib.Hashable.S with type t := t
val hash_fold_t : t Base__Ppx_hash_lib.hash_fold
val hash : t -> Base__Ppx_hash_lib.Std.Hash.hash_value
diff --git a/website/static/odoc/next/infer/Checkers/Lineage/Unified/index.html b/website/static/odoc/next/infer/Checkers/Lineage/Unified/index.html new file mode 100644 index 00000000000..b9b8f263792 --- /dev/null +++ b/website/static/odoc/next/infer/Checkers/Lineage/Unified/index.html @@ -0,0 +1,6 @@ + +Unified (infer.Checkers.Lineage.Unified)

Module Lineage.Unified

module UVertex : sig ... end
module LocalG := G
module G : Graph.Sig.P with type V.t = UVertex.t and type E.label = Edge.t
val transform_e : + (IR.Procname.t -> LineageShape.Summary.t option) -> + IR.Procname.t -> + LocalG.edge -> + G.edge list
module Dot : sig ... end
diff --git a/website/static/odoc/next/infer/IBase/EarlyScubaLogging/index.html b/website/static/odoc/next/infer/IBase/EarlyScubaLogging/index.html new file mode 100644 index 00000000000..a011199c657 --- /dev/null +++ b/website/static/odoc/next/infer/IBase/EarlyScubaLogging/index.html @@ -0,0 +1,2 @@ + +EarlyScubaLogging (infer.IBase.EarlyScubaLogging)

Module IBase.EarlyScubaLogging

val log_message : label:string -> message:string -> unit
val finish : unit -> LogEntry.t list
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html index f6e3d2df77e..db123ffa5e3 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html @@ -183,4 +183,7 @@ option
val has_unknown_effect : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> + bool
val is_hack_sinit_called : + Pulselib.PulseBasicInterface.AbstractValue.t -> + t -> bool
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/CanonValue/Attributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/CanonValue/Attributes/index.html index 56b952621d4..686cf03ef0d 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/CanonValue/Attributes/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/CanonValue/Attributes/index.html @@ -107,4 +107,7 @@ t -> t -> (IR.Var.t * IBase.Location.t * Pulselib.PulseBasicInterface.ValueHistory.t) - option
val has_unknown_effect : t -> t -> bool
+ option
val has_unknown_effect : t -> t -> bool
val is_hack_sinit_called : t -> t -> bool
val get_hack_sinit_must_not_be_called : + t -> + t -> + Pulselib.PulseBasicInterface.Timestamp.t option
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html index 7c43b1312af..56aca82c9df 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html @@ -9,7 +9,7 @@ t -> (IR.Procname.t * IBase.Location.t * Trace.t) option
val get_copied_into : t -> CopiedInto.t option
val get_copied_return : t -> - (AbstractValue.t * bool * CopyOrigin.t * IBase.Location.t) option
val remove_copied_return : t -> t
val get_source_origin_of_copy : t -> (PulseAbstractValue.t * bool) option
val get_allocation : t -> (allocator * Trace.t) option
val remove_allocation : t -> t
val get_unknown_effect : t -> (CallEvent.t * ValueHistory.t) option
val remove_dict_contain_const_keys : t -> t
val is_dict_contain_const_keys : t -> bool
val get_dict_read_const_keys : t -> ConstKeys.t option
val get_static_type : t -> IR.Typ.Name.t option
val is_java_resource_released : t -> bool
val get_hack_builder : t -> Builder.t option
val remove_hack_builder : t -> t
val is_hack_builder_discardable : t -> bool
val is_csharp_resource_released : t -> bool
val is_end_of_collection : t -> bool
val get_invalid : t -> (Invalidation.t * Trace.t) option
val get_tainted : t -> TaintedSet.t
val remove_tainted : t -> t
val remove_must_not_be_tainted : ?kinds:TaintConfig.Kind.Set.t -> t -> t
val get_propagate_taint_from : + (AbstractValue.t * bool * CopyOrigin.t * IBase.Location.t) option
val remove_copied_return : t -> t
val get_source_origin_of_copy : t -> (PulseAbstractValue.t * bool) option
val get_allocation : t -> (allocator * Trace.t) option
val remove_allocation : t -> t
val get_unknown_effect : t -> (CallEvent.t * ValueHistory.t) option
val remove_dict_contain_const_keys : t -> t
val is_dict_contain_const_keys : t -> bool
val get_dict_read_const_keys : t -> ConstKeys.t option
val get_static_type : t -> IR.Typ.Name.t option
val is_java_resource_released : t -> bool
val get_hack_builder : t -> Builder.t option
val remove_hack_builder : t -> t
val is_hack_builder_discardable : t -> bool
val is_hack_sinit_called : t -> bool
val get_hack_sinit_must_not_be_called : t -> Timestamp.t option
val is_csharp_resource_released : t -> bool
val is_end_of_collection : t -> bool
val get_invalid : t -> (Invalidation.t * Trace.t) option
val get_tainted : t -> TaintedSet.t
val remove_tainted : t -> t
val remove_must_not_be_tainted : ?kinds:TaintConfig.Kind.Set.t -> t -> t
val get_propagate_taint_from : t -> (taint_propagation_reason * taint_in list) option
val remove_propagate_taint_from : t -> t
val get_returned_from_unknown : t -> AbstractValue.t list option
val get_taint_sanitized : t -> TaintSanitizedSet.t
val remove_taint_sanitized : t -> t
val get_must_be_valid : t -> diff --git a/website/static/odoc/next/infer/Pulselib/PulseAttribute/Builder/index.html b/website/static/odoc/next/infer/Pulselib/PulseAttribute/Builder/index.html new file mode 100644 index 00000000000..7bdd498c519 --- /dev/null +++ b/website/static/odoc/next/infer/Pulselib/PulseAttribute/Builder/index.html @@ -0,0 +1,2 @@ + +Builder (infer.Pulselib.PulseAttribute.Builder)

Module PulseAttribute.Builder

type t =
  1. | Discardable
  2. | NonDiscardable
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
include Ppx_compare_lib.Equal.S with type t := t
val equal : t Base__Ppx_compare_lib.equal
val pp : F.formatter -> t -> unit
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html b/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html index 44d3d117b9c..b745ca4c82b 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html @@ -4,7 +4,7 @@ IStdlib.PrettyPrintable.PPSet with type elt = TaintSanitized.t
type taint_propagation_reason =
  1. | InternalModel
  2. | UnknownCall
  3. | UserConfig
val pp_taint_propagation_reason : F.formatter -> taint_propagation_reason -> - unit
module CopyOrigin : sig ... end
module CopiedInto : sig ... end
module ConfigUsage : sig ... end
module Builder : sig ... end
module UninitializedTyp : sig ... end
module ConstKeys : sig ... end
type t =
  1. | AddressOfCppTemporary of IR.Var.t * ValueHistory.t
  2. | AddressOfStackVariable of IR.Var.t * IBase.Location.t * ValueHistory.t
  3. | Allocated of allocator * Trace.t
  4. | AlwaysReachable
  5. | Closure of IR.Procname.t
  6. | ConfigUsage of ConfigUsage.t
  7. | CopiedInto of CopiedInto.t
    (*

    records the copied var/field for each source address

    *)
  8. | CopiedReturn of {
    1. source : AbstractValue.t;
    2. is_const_ref : bool;
    3. from : CopyOrigin.t;
    4. copied_location : IBase.Location.t;
    }
    (*

    records the copied value for the return address

    *)
  9. | DictContainConstKeys
    (*

    the dictionary contains only constant keys (note: only string constant is supported for now)

    *)
  10. | DictReadConstKeys of ConstKeys.t
    (*

    constant string keys that are read from the dictionary

    *)
  11. | EndOfCollection
  12. | HackBuilder of Builder.t
  13. | InReportedRetainCycle
  14. | Initialized
  15. | Invalid of Invalidation.t * Trace.t
  16. | LastLookup of AbstractValue.t
  17. | MustBeInitialized of Timestamp.t * Trace.t
  18. | MustBeValid of Timestamp.t * Trace.t * Invalidation.must_be_valid_reason option
  19. | MustNotBeTainted of TaintSink.t TaintSinkMap.t
  20. | JavaResourceReleased
  21. | CSharpResourceReleased
  22. | HackAsyncAwaited
  23. | PropagateTaintFrom of taint_propagation_reason * taint_in list
  24. | ReturnedFromUnknown of AbstractValue.t list
  25. | SourceOriginOfCopy of {
    1. source : PulseAbstractValue.t;
    2. is_const_ref : bool;
    }
    (*

    records the source value for a given copy to lookup the appropriate heap in non-disj domain

    *)
  26. | StaticType of IR.Typ.Name.t
    (*

    type gotten or inferred from types in SIL instructions (only for Hack frontend)

    *)
  27. | StdMoved
  28. | StdVectorReserve
  29. | Tainted of TaintedSet.t
  30. | TaintSanitized of TaintSanitizedSet.t
  31. | Uninitialized of UninitializedTyp.t
  32. | UnknownEffect of CallEvent.t * ValueHistory.t
    (*

    generated by calls to unknown functions to remember that a pointer has been passed to an unknown function and so everything reachable from it has potentially been affected in unknown ways

    *)
  33. | UnreachableAt of IBase.Location.t
    (*

    temporary marker to remember where a variable became unreachable; helps with accurately reporting leaks

    *)
  34. | UsedAsBranchCond of IR.Procname.t * IBase.Location.t * Trace.t
  35. | WrittenTo of Timestamp.t * Trace.t
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
val pp : F.formatter -> t -> unit
val filter_unreachable : + unit
module CopyOrigin : sig ... end
module CopiedInto : sig ... end
module ConfigUsage : sig ... end
module Builder : sig ... end
module UninitializedTyp : sig ... end
module ConstKeys : sig ... end
type t =
  1. | AddressOfCppTemporary of IR.Var.t * ValueHistory.t
  2. | AddressOfStackVariable of IR.Var.t * IBase.Location.t * ValueHistory.t
  3. | Allocated of allocator * Trace.t
  4. | AlwaysReachable
  5. | Closure of IR.Procname.t
  6. | ConfigUsage of ConfigUsage.t
  7. | CopiedInto of CopiedInto.t
    (*

    records the copied var/field for each source address

    *)
  8. | CopiedReturn of {
    1. source : AbstractValue.t;
    2. is_const_ref : bool;
    3. from : CopyOrigin.t;
    4. copied_location : IBase.Location.t;
    }
    (*

    records the copied value for the return address

    *)
  9. | DictContainConstKeys
    (*

    the dictionary contains only constant keys (note: only string constant is supported for now)

    *)
  10. | DictReadConstKeys of ConstKeys.t
    (*

    constant string keys that are read from the dictionary

    *)
  11. | EndOfCollection
  12. | HackBuilder of Builder.t
  13. | HackSinitCalled
  14. | HackSinitMustNotBeCalled of Timestamp.t
  15. | InReportedRetainCycle
  16. | Initialized
  17. | Invalid of Invalidation.t * Trace.t
  18. | LastLookup of AbstractValue.t
  19. | MustBeInitialized of Timestamp.t * Trace.t
  20. | MustBeValid of Timestamp.t * Trace.t * Invalidation.must_be_valid_reason option
  21. | MustNotBeTainted of TaintSink.t TaintSinkMap.t
  22. | JavaResourceReleased
  23. | CSharpResourceReleased
  24. | HackAsyncAwaited
  25. | PropagateTaintFrom of taint_propagation_reason * taint_in list
  26. | ReturnedFromUnknown of AbstractValue.t list
  27. | SourceOriginOfCopy of {
    1. source : PulseAbstractValue.t;
    2. is_const_ref : bool;
    }
    (*

    records the source value for a given copy to lookup the appropriate heap in non-disj domain

    *)
  28. | StaticType of IR.Typ.Name.t
    (*

    type gotten or inferred from types in SIL instructions (only for Hack frontend)

    *)
  29. | StdMoved
  30. | StdVectorReserve
  31. | Tainted of TaintedSet.t
  32. | TaintSanitized of TaintSanitizedSet.t
  33. | Uninitialized of UninitializedTyp.t
  34. | UnknownEffect of CallEvent.t * ValueHistory.t
    (*

    generated by calls to unknown functions to remember that a pointer has been passed to an unknown function and so everything reachable from it has potentially been affected in unknown ways

    *)
  35. | UnreachableAt of IBase.Location.t
    (*

    temporary marker to remember where a variable became unreachable; helps with accurately reporting leaks

    *)
  36. | UsedAsBranchCond of IR.Procname.t * IBase.Location.t * Trace.t
  37. | WrittenTo of Timestamp.t * Trace.t
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
val pp : F.formatter -> t -> unit
val filter_unreachable : AbstractValue.Set.t AbstractValue.Map.t -> (AbstractValue.t -> bool) -> t -> diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html index 50b58ac008c..84a9802db75 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html @@ -195,7 +195,13 @@ option
val has_unknown_effect : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> - bool
val make_suitable_for_pre_summary : t -> t
val canonicalize_post : + bool
val is_hack_sinit_called : + Pulselib.PulseBasicInterface.AbstractValue.t -> + t -> + bool
val get_hack_sinit_must_not_be_called : + Pulselib.PulseBasicInterface.AbstractValue.t -> + t -> + Pulselib.PulseBasicInterface.Timestamp.t option
val make_suitable_for_pre_summary : t -> t
val canonicalize_post : get_var_repr: (Pulselib.PulseBasicInterface.AbstractValue.t -> Pulselib.PulseBasicInterface.AbstractValue.t) -> diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/module-type-S/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/module-type-S/index.html index 929e32fcbdc..1c01f3f5db9 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/module-type-S/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/module-type-S/index.html @@ -110,4 +110,7 @@ key -> t -> (IR.Var.t * IBase.Location.t * Pulselib.PulseBasicInterface.ValueHistory.t) - option
val has_unknown_effect : key -> t -> bool
+ option
val has_unknown_effect : key -> t -> bool
val is_hack_sinit_called : key -> t -> bool
val get_hack_sinit_must_not_be_called : + key -> + t -> + Pulselib.PulseBasicInterface.Timestamp.t option
diff --git a/website/static/odoc/next/infer/Pulselib/PulseCanonValue/Make/Attributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseCanonValue/Make/Attributes/index.html index d2feb531e4b..3a1839d0eb5 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseCanonValue/Make/Attributes/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseCanonValue/Make/Attributes/index.html @@ -107,4 +107,7 @@ t -> t -> (IR.Var.t * IBase.Location.t * Pulselib.PulseBasicInterface.ValueHistory.t) - option
val has_unknown_effect : t -> t -> bool
+ option
val has_unknown_effect : t -> t -> bool
val is_hack_sinit_called : t -> t -> bool
val get_hack_sinit_must_not_be_called : + t -> + t -> + Pulselib.PulseBasicInterface.Timestamp.t option
diff --git a/website/static/odoc/next/infer/Pulselib/PulseCanonValue/module-type-S/Attributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseCanonValue/module-type-S/Attributes/index.html index cb406593a89..ff37c613e18 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseCanonValue/module-type-S/Attributes/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseCanonValue/module-type-S/Attributes/index.html @@ -107,4 +107,7 @@ t -> t -> (IR.Var.t * IBase.Location.t * Pulselib.PulseBasicInterface.ValueHistory.t) - option
val has_unknown_effect : t -> t -> bool
+ option
val has_unknown_effect : t -> t -> bool
val is_hack_sinit_called : t -> t -> bool
val get_hack_sinit_must_not_be_called : + t -> + t -> + Pulselib.PulseBasicInterface.Timestamp.t option
diff --git a/website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html b/website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html index 8ce9deccb6a..7c6eeaa53dc 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html @@ -6,7 +6,7 @@ list;}
  • | FormalActualLength of {
    1. formals : (IR.Pvar.t * IR.Typ.t) list;
    2. actuals : ((Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) * IR.Typ.t) - list;
    }
  • | PathCondition
    • val is_dynamic_type_needed_contradiction : + list;}
  • | HackSinitMustNotBeCalled of Pulselib.PulseBasicInterface.AbstractValue.t
  • | PathCondition
    • val merge_contradictions : diff --git a/website/static/odoc/next/infer/Pulselib/PulseModelsDSL/Syntax/index.html b/website/static/odoc/next/infer/Pulselib/PulseModelsDSL/Syntax/index.html index b1cfc39e089..827153a04bd 100644 --- a/website/static/odoc/next/infer/Pulselib/PulseModelsDSL/Syntax/index.html +++ b/website/static/odoc/next/infer/Pulselib/PulseModelsDSL/Syntax/index.html @@ -30,7 +30,7 @@ unit model_monad

    Disjunctive reasoning

    val disjuncts : 'a model_monad list -> 'a model_monad
    val start_model : unit model_monad -> PulseModelsImport.model

    get a model from a disjunctive model_monad

    val lift_to_monad : PulseModelsImport.model -> unit model_monad

    beware that the model may modify the PulseModelsImport.model_data.ret field

    val lift_to_monad_and_get_result : PulseModelsImport.model -> aval model_monad

    apply the model and return its result. fails if the model did not assign the reserved model_data.ret variable.

    Operations

    PulseOperations functions you need should be copied here

    val add_dict_contain_const_keys : aval -> unit model_monad
    val add_dict_read_const_key : aval -> IR.Fieldname.t -> unit model_monad
    val remove_dict_contain_const_keys : aval -> unit model_monad
    val add_static_type : IR.Typ.name -> aval -> unit model_monad
    val deep_copy : ?depth_max:int -> aval -> aval model_monad
    val eval_binop : IR.Binop.t -> aval -> aval -> aval model_monad
    val eval_binop_int : IR.Binop.t -> aval -> IR.IntLit.t -> aval model_monad
    val eval_read : IR.Exp.t -> aval model_monad
    val eval_const_int : int -> aval model_monad
    val eval_const_string : string -> aval model_monad
    val eval_string_concat : aval -> aval -> aval model_monad
    val eval_to_value_origin : + unit model_monad
    val add_dict_contain_const_keys : aval -> unit model_monad
    val add_dict_read_const_key : aval -> IR.Fieldname.t -> unit model_monad
    val remove_dict_contain_const_keys : aval -> unit model_monad
    val is_hack_sinit_called : aval -> bool model_monad
    val set_hack_sinit_called : aval -> unit model_monad
    val set_hack_sinit_must_not_be_called : aval -> unit model_monad
    val add_static_type : IR.Typ.name -> aval -> unit model_monad
    val deep_copy : ?depth_max:int -> aval -> aval model_monad
    val eval_binop : IR.Binop.t -> aval -> aval -> aval model_monad
    val eval_binop_int : IR.Binop.t -> aval -> IR.IntLit.t -> aval model_monad
    val eval_read : IR.Exp.t -> aval model_monad
    val eval_const_int : int -> aval model_monad
    val eval_const_string : string -> aval model_monad
    val eval_string_concat : aval -> aval -> aval model_monad
    val eval_access : ?desc:string ->