diff --git a/website/static/man/next/infer-analyze.1.html b/website/static/man/next/infer-analyze.1.html
index a4da3c55d..db2b7f5f7 100644
--- a/website/static/man/next/infer-analyze.1.html
+++ b/website/static/man/next/infer-analyze.1.html
@@ -520,14 +520,32 @@ modelled as allocs in Pulse
string
Regex of methods that should be
-modelled as free in Pulse
+modelled as wrappers to free(3) in Pulse. The pointer
+to be freed should be the first argument of the function.
+This should only be needed if the code of the wrapper is not
+visible to infer or if Pulse somehow doesn't understand it
+(e.g. the call is dispatched to global function
+pointers).
--pulse-model-malloc-patternstring
Regex of methods that should be
-modelled as mallocs in Pulse
+modelled as wrappers to malloc(3) in Pulse. The size
+to allocate should be the first argument of the function.
+See --pulse-model-free-pattern for more
+information.
+
+
+
--pulse-model-realloc-pattern
+string
+
+
Regex of methods that should be
+modelled as wrappers to realloc(3) in Pulse. The
+pointer to be reallocated should be the first argument of
+the function and the new size the second argument. See
+--pulse-model-free-pattern for more information.
--pulse-model-release-pattern
diff --git a/website/static/man/next/infer.1.html b/website/static/man/next/infer.1.html
index cfaf584b3..45c339d67 100644
--- a/website/static/man/next/infer.1.html
+++ b/website/static/man/next/infer.1.html
@@ -1706,14 +1706,32 @@ modelled as allocs in Pulse
--pulse-model-free-pattern string
Regex of methods that should be
-modelled as free in Pulse
+modelled as wrappers to free(3) in Pulse. The pointer
+to be freed should be the first argument of the function.
+This should only be needed if the code of the wrapper is not
+visible to infer or if Pulse somehow doesn't understand it
+(e.g. the call is dispatched to global function
+pointers).
See also
infer-analyze(1).
--pulse-model-malloc-patternstring
Regex of methods that should be
-modelled as mallocs in Pulse
+modelled as wrappers to malloc(3) in Pulse. The size
+to allocate should be the first argument of the function.
+See --pulse-model-free-pattern for more
+information.
+
+
See also
+infer-analyze(1).
+--pulse-model-realloc-patternstring
+
+
Regex of methods that should be
+modelled as wrappers to realloc(3) in Pulse. The
+pointer to be reallocated should be the first argument of
+the function and the new size the second argument. See
+--pulse-model-free-pattern for more information.
See also
infer-analyze(1).
diff --git a/website/static/odoc/next/infer/Absint/AbstractDomain/InvertedMap/index.html b/website/static/odoc/next/infer/Absint/AbstractDomain/InvertedMap/index.html
index a367f475c..8b63cd78b 100644
--- a/website/static/odoc/next/infer/Absint/AbstractDomain/InvertedMap/index.html
+++ b/website/static/odoc/next/infer/Absint/AbstractDomain/InvertedMap/index.html
@@ -1,2 +1,2 @@
-InvertedMap (infer.Absint.AbstractDomain.InvertedMap)
Module AbstractDomain.InvertedMap
Map domain ordered by intersection over the set of bindings, so the top element is the empty map. Every element implictly maps to top unless it is explicitly bound to something else
\ No newline at end of file
+InvertedMap (infer.Absint.AbstractDomain.InvertedMap)
Module AbstractDomain.InvertedMap
Map domain ordered by intersection over the set of bindings, so the top element is the empty map. Every element implictly maps to top unless it is explicitly bound to something else
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint/AbstractDomain/Map/index.html b/website/static/odoc/next/infer/Absint/AbstractDomain/Map/index.html
index 571b63509..509351348 100644
--- a/website/static/odoc/next/infer/Absint/AbstractDomain/Map/index.html
+++ b/website/static/odoc/next/infer/Absint/AbstractDomain/Map/index.html
@@ -1,2 +1,2 @@
-Map (infer.Absint.AbstractDomain.Map)
Module AbstractDomain.Map
Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else
\ No newline at end of file
+Map (infer.Absint.AbstractDomain.Map)
Module AbstractDomain.Map
Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint/AbstractDomain/MapOfPPMap/index.html b/website/static/odoc/next/infer/Absint/AbstractDomain/MapOfPPMap/index.html
index d528870aa..93323bd3d 100644
--- a/website/static/odoc/next/infer/Absint/AbstractDomain/MapOfPPMap/index.html
+++ b/website/static/odoc/next/infer/Absint/AbstractDomain/MapOfPPMap/index.html
@@ -1,2 +1,2 @@
-MapOfPPMap (infer.Absint.AbstractDomain.MapOfPPMap)
Module AbstractDomain.MapOfPPMap
Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else. Uses PPMap as the underlying map
\ No newline at end of file
+MapOfPPMap (infer.Absint.AbstractDomain.MapOfPPMap)
Module AbstractDomain.MapOfPPMap
Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else. Uses PPMap as the underlying map
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint/AbstractDomain/SafeInvertedMap/index.html b/website/static/odoc/next/infer/Absint/AbstractDomain/SafeInvertedMap/index.html
index f7c17ee2c..89228a2b5 100644
--- a/website/static/odoc/next/infer/Absint/AbstractDomain/SafeInvertedMap/index.html
+++ b/website/static/odoc/next/infer/Absint/AbstractDomain/SafeInvertedMap/index.html
@@ -1,2 +1,2 @@
-SafeInvertedMap (infer.Absint.AbstractDomain.SafeInvertedMap)
Module AbstractDomain.SafeInvertedMap
Similar to InvertedMap but it guarantees that it has a canonical form. For example, both {a -> top_v} and empty represent the same abstract value top in InvertedMap, but in this implementation, top is always implemented as empty by not adding the top_v explicitly.
\ No newline at end of file
+SafeInvertedMap (infer.Absint.AbstractDomain.SafeInvertedMap)
Module AbstractDomain.SafeInvertedMap
Similar to InvertedMap but it guarantees that it has a canonical form. For example, both {a -> top_v} and empty represent the same abstract value top in InvertedMap, but in this implementation, top is always implemented as empty by not adding the top_v explicitly.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint/AbstractDomain/module-type-InvertedMapS/index.html b/website/static/odoc/next/infer/Absint/AbstractDomain/module-type-InvertedMapS/index.html
index 1906178ec..44cbb95d9 100644
--- a/website/static/odoc/next/infer/Absint/AbstractDomain/module-type-InvertedMapS/index.html
+++ b/website/static/odoc/next/infer/Absint/AbstractDomain/module-type-InvertedMapS/index.html
@@ -1,2 +1,2 @@
-InvertedMapS (infer.Absint.AbstractDomain.InvertedMapS)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint/AbstractDomain/module-type-MapS/index.html b/website/static/odoc/next/infer/Absint/AbstractDomain/module-type-MapS/index.html
index a93136c0d..e0cfd4636 100644
--- a/website/static/odoc/next/infer/Absint/AbstractDomain/module-type-MapS/index.html
+++ b/website/static/odoc/next/infer/Absint/AbstractDomain/module-type-MapS/index.html
@@ -1,2 +1,2 @@
-MapS (infer.Absint.AbstractDomain.MapS)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint/IdAccessPathMapDomain/index.html b/website/static/odoc/next/infer/Absint/IdAccessPathMapDomain/index.html
index 4ee323801..705d30814 100644
--- a/website/static/odoc/next/infer/Absint/IdAccessPathMapDomain/index.html
+++ b/website/static/odoc/next/infer/Absint/IdAccessPathMapDomain/index.html
@@ -1,2 +1,2 @@
-IdAccessPathMapDomain (infer.Absint.IdAccessPathMapDomain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint/PatternMatch/ObjectiveC/index.html b/website/static/odoc/next/infer/Absint/PatternMatch/ObjectiveC/index.html
index ccd6895a4..2dec424d5 100644
--- a/website/static/odoc/next/infer/Absint/PatternMatch/ObjectiveC/index.html
+++ b/website/static/odoc/next/infer/Absint/PatternMatch/ObjectiveC/index.html
@@ -1,2 +1,2 @@
-ObjectiveC (infer.Absint.PatternMatch.ObjectiveC)
Module PatternMatch.ObjectiveC
val implements : string ->IR.Tenv.t-> string -> bool
Check whether class implements a given ObjC class
val implements_ns_string_variants : IR.Tenv.t-> string -> bool
Check whether class implements NSString or NSAttributedString
val conforms_to : protocol:string->IR.Tenv.t-> string -> bool
Check whether class conforms to a given ObjC protocol
val implements_collection : IR.Tenv.t-> string -> bool
val is_core_graphics_create_or_copy : IR.Tenv.t-> string -> bool
val is_core_foundation_create_or_copy : IR.Tenv.t-> string -> bool
val is_core_graphics_release : IR.Tenv.t-> string -> bool
val is_modelled_as_alloc : IR.Tenv.t-> string -> bool
val is_modelled_as_release : IR.Tenv.t-> string -> bool
\ No newline at end of file
+ObjectiveC (infer.Absint.PatternMatch.ObjectiveC)
Module PatternMatch.ObjectiveC
val implements : string ->IR.Tenv.t-> string -> bool
Check whether class implements a given ObjC class
val implements_ns_string_variants : IR.Tenv.t-> string -> bool
Check whether class implements NSString or NSAttributedString
val conforms_to : protocol:string->IR.Tenv.t-> string -> bool
Check whether class conforms to a given ObjC protocol
val implements_collection : IR.Tenv.t-> string -> bool
val is_core_graphics_create_or_copy : IR.Tenv.t-> string -> bool
val is_core_foundation_create_or_copy : IR.Tenv.t-> string -> bool
val is_core_graphics_release : IR.Tenv.t-> string -> bool
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__AbstractDomain/InvertedMap/index.html b/website/static/odoc/next/infer/Absint__AbstractDomain/InvertedMap/index.html
index 61407c29c..1bd512eb8 100644
--- a/website/static/odoc/next/infer/Absint__AbstractDomain/InvertedMap/index.html
+++ b/website/static/odoc/next/infer/Absint__AbstractDomain/InvertedMap/index.html
@@ -1,2 +1,2 @@
-InvertedMap (infer.Absint__AbstractDomain.InvertedMap)
Module Absint__AbstractDomain.InvertedMap
Map domain ordered by intersection over the set of bindings, so the top element is the empty map. Every element implictly maps to top unless it is explicitly bound to something else
\ No newline at end of file
+InvertedMap (infer.Absint__AbstractDomain.InvertedMap)
Module Absint__AbstractDomain.InvertedMap
Map domain ordered by intersection over the set of bindings, so the top element is the empty map. Every element implictly maps to top unless it is explicitly bound to something else
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__AbstractDomain/Map/index.html b/website/static/odoc/next/infer/Absint__AbstractDomain/Map/index.html
index 5abbe1347..eaa2dbd75 100644
--- a/website/static/odoc/next/infer/Absint__AbstractDomain/Map/index.html
+++ b/website/static/odoc/next/infer/Absint__AbstractDomain/Map/index.html
@@ -1,2 +1,2 @@
-Map (infer.Absint__AbstractDomain.Map)
Module Absint__AbstractDomain.Map
Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else
\ No newline at end of file
+Map (infer.Absint__AbstractDomain.Map)
Module Absint__AbstractDomain.Map
Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__AbstractDomain/MapOfPPMap/index.html b/website/static/odoc/next/infer/Absint__AbstractDomain/MapOfPPMap/index.html
index 001139c72..984375693 100644
--- a/website/static/odoc/next/infer/Absint__AbstractDomain/MapOfPPMap/index.html
+++ b/website/static/odoc/next/infer/Absint__AbstractDomain/MapOfPPMap/index.html
@@ -1,2 +1,2 @@
-MapOfPPMap (infer.Absint__AbstractDomain.MapOfPPMap)
Module Absint__AbstractDomain.MapOfPPMap
Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else. Uses PPMap as the underlying map
\ No newline at end of file
+MapOfPPMap (infer.Absint__AbstractDomain.MapOfPPMap)
Module Absint__AbstractDomain.MapOfPPMap
Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else. Uses PPMap as the underlying map
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__AbstractDomain/SafeInvertedMap/index.html b/website/static/odoc/next/infer/Absint__AbstractDomain/SafeInvertedMap/index.html
index 37c4c3a84..594e21136 100644
--- a/website/static/odoc/next/infer/Absint__AbstractDomain/SafeInvertedMap/index.html
+++ b/website/static/odoc/next/infer/Absint__AbstractDomain/SafeInvertedMap/index.html
@@ -1,2 +1,2 @@
-SafeInvertedMap (infer.Absint__AbstractDomain.SafeInvertedMap)
Module Absint__AbstractDomain.SafeInvertedMap
Similar to InvertedMap but it guarantees that it has a canonical form. For example, both {a -> top_v} and empty represent the same abstract value top in InvertedMap, but in this implementation, top is always implemented as empty by not adding the top_v explicitly.
\ No newline at end of file
+SafeInvertedMap (infer.Absint__AbstractDomain.SafeInvertedMap)
Module Absint__AbstractDomain.SafeInvertedMap
Similar to InvertedMap but it guarantees that it has a canonical form. For example, both {a -> top_v} and empty represent the same abstract value top in InvertedMap, but in this implementation, top is always implemented as empty by not adding the top_v explicitly.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__AbstractDomain/module-type-InvertedMapS/index.html b/website/static/odoc/next/infer/Absint__AbstractDomain/module-type-InvertedMapS/index.html
index e864994b8..7464566d2 100644
--- a/website/static/odoc/next/infer/Absint__AbstractDomain/module-type-InvertedMapS/index.html
+++ b/website/static/odoc/next/infer/Absint__AbstractDomain/module-type-InvertedMapS/index.html
@@ -1,2 +1,2 @@
-InvertedMapS (infer.Absint__AbstractDomain.InvertedMapS)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__AbstractDomain/module-type-MapS/index.html b/website/static/odoc/next/infer/Absint__AbstractDomain/module-type-MapS/index.html
index a5dd4428d..9111c1274 100644
--- a/website/static/odoc/next/infer/Absint__AbstractDomain/module-type-MapS/index.html
+++ b/website/static/odoc/next/infer/Absint__AbstractDomain/module-type-MapS/index.html
@@ -1,2 +1,2 @@
-MapS (infer.Absint__AbstractDomain.MapS)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__IdAccessPathMapDomain/index.html b/website/static/odoc/next/infer/Absint__IdAccessPathMapDomain/index.html
index c63303d6a..05b6504e7 100644
--- a/website/static/odoc/next/infer/Absint__IdAccessPathMapDomain/index.html
+++ b/website/static/odoc/next/infer/Absint__IdAccessPathMapDomain/index.html
@@ -1,2 +1,2 @@
-Absint__IdAccessPathMapDomain (infer.Absint__IdAccessPathMapDomain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__PatternMatch/ObjectiveC/index.html b/website/static/odoc/next/infer/Absint__PatternMatch/ObjectiveC/index.html
index ba497e03d..c41f960da 100644
--- a/website/static/odoc/next/infer/Absint__PatternMatch/ObjectiveC/index.html
+++ b/website/static/odoc/next/infer/Absint__PatternMatch/ObjectiveC/index.html
@@ -1,2 +1,2 @@
-ObjectiveC (infer.Absint__PatternMatch.ObjectiveC)
Module Absint__PatternMatch.ObjectiveC
val implements : string ->IR.Tenv.t-> string -> bool
Check whether class implements a given ObjC class
val implements_ns_string_variants : IR.Tenv.t-> string -> bool
Check whether class implements NSString or NSAttributedString
val conforms_to : protocol:string->IR.Tenv.t-> string -> bool
Check whether class conforms to a given ObjC protocol
val implements_collection : IR.Tenv.t-> string -> bool
val is_core_graphics_create_or_copy : IR.Tenv.t-> string -> bool
val is_core_foundation_create_or_copy : IR.Tenv.t-> string -> bool
val is_core_graphics_release : IR.Tenv.t-> string -> bool
val is_modelled_as_alloc : IR.Tenv.t-> string -> bool
val is_modelled_as_release : IR.Tenv.t-> string -> bool
\ No newline at end of file
+ObjectiveC (infer.Absint__PatternMatch.ObjectiveC)
Module Absint__PatternMatch.ObjectiveC
val implements : string ->IR.Tenv.t-> string -> bool
Check whether class implements a given ObjC class
val implements_ns_string_variants : IR.Tenv.t-> string -> bool
Check whether class implements NSString or NSAttributedString
val conforms_to : protocol:string->IR.Tenv.t-> string -> bool
Check whether class conforms to a given ObjC protocol
val implements_collection : IR.Tenv.t-> string -> bool
val is_core_graphics_create_or_copy : IR.Tenv.t-> string -> bool
val is_core_foundation_create_or_copy : IR.Tenv.t-> string -> bool
val is_core_graphics_release : IR.Tenv.t-> string -> bool
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/BO/ArrayBlk/index.html b/website/static/odoc/next/infer/BO/ArrayBlk/index.html
index 7370f850b..91b418081 100644
--- a/website/static/odoc/next/infer/BO/ArrayBlk/index.html
+++ b/website/static/odoc/next/infer/BO/ArrayBlk/index.html
@@ -1,2 +1,2 @@
-ArrayBlk (infer.BO.ArrayBlk)
Lift a comparison of Itv.t and Loc.t to that of t. The comparison for Itv.t is used for integer values such as offset and size, and the comparison for Loc.t is used for allocsites.
Substitute symbolic abstract locations and symbolic interval value in the array block. eval_sym is to get substituted interval values and eval_locpath is to get substituted abstract locaion values. It also returns a set of abstract locations containing non-allocsite locations from the substitution results. Since the key of ArrayBlk.t is AbsLoc.Allocsite.t, they cannot be written in this domain.
Lift a comparison of Itv.t and Loc.t to that of t. The comparison for Itv.t is used for integer values such as offset and size, and the comparison for Loc.t is used for allocsites.
Substitute symbolic abstract locations and symbolic interval value in the array block. eval_sym is to get substituted interval values and eval_locpath is to get substituted abstract locaion values. It also returns a set of abstract locations containing non-allocsite locations from the substitution results. Since the key of ArrayBlk.t is AbsLoc.Allocsite.t, they cannot be written in this domain.
Return size of the array block. If cost_mode is true, it returns a conservative (bigger than correct one), but not correct size results.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/BO/BufferOverrunDomain/AliasTargets/index.html b/website/static/odoc/next/infer/BO/BufferOverrunDomain/AliasTargets/index.html
index 36476b816..da491fe89 100644
--- a/website/static/odoc/next/infer/BO/BufferOverrunDomain/AliasTargets/index.html
+++ b/website/static/odoc/next/infer/BO/BufferOverrunDomain/AliasTargets/index.html
@@ -1,2 +1,2 @@
-AliasTargets (infer.BO.BufferOverrunDomain.AliasTargets)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/BO/BufferOverrunDomain/PrunePairs/index.html b/website/static/odoc/next/infer/BO/BufferOverrunDomain/PrunePairs/index.html
index 93846ebc5..455564c7e 100644
--- a/website/static/odoc/next/infer/BO/BufferOverrunDomain/PrunePairs/index.html
+++ b/website/static/odoc/next/infer/BO/BufferOverrunDomain/PrunePairs/index.html
@@ -1,2 +1,2 @@
-PrunePairs (infer.BO.BufferOverrunDomain.PrunePairs)
Module BufferOverrunDomain.PrunePairs
PrunePairs is a map from abstract locations to abstract values that represents pruned results in the latest pruning. It uses InvertedMap because more pruning means smaller abstract states.
Check if a path is reachable, by using its pruned values
\ No newline at end of file
+PrunePairs (infer.BO.BufferOverrunDomain.PrunePairs)
Module BufferOverrunDomain.PrunePairs
PrunePairs is a map from abstract locations to abstract values that represents pruned results in the latest pruning. It uses InvertedMap because more pruning means smaller abstract states.
Check if a path is reachable, by using its pruned values
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/BO__ArrayBlk/index.html b/website/static/odoc/next/infer/BO__ArrayBlk/index.html
index de445bff6..3493bf36d 100644
--- a/website/static/odoc/next/infer/BO__ArrayBlk/index.html
+++ b/website/static/odoc/next/infer/BO__ArrayBlk/index.html
@@ -1,2 +1,2 @@
-BO__ArrayBlk (infer.BO__ArrayBlk)
Lift a comparison of Itv.t and Loc.t to that of t. The comparison for Itv.t is used for integer values such as offset and size, and the comparison for Loc.t is used for allocsites.
Substitute symbolic abstract locations and symbolic interval value in the array block. eval_sym is to get substituted interval values and eval_locpath is to get substituted abstract locaion values. It also returns a set of abstract locations containing non-allocsite locations from the substitution results. Since the key of ArrayBlk.t is AbsLoc.Allocsite.t, they cannot be written in this domain.
Lift a comparison of Itv.t and Loc.t to that of t. The comparison for Itv.t is used for integer values such as offset and size, and the comparison for Loc.t is used for allocsites.
Substitute symbolic abstract locations and symbolic interval value in the array block. eval_sym is to get substituted interval values and eval_locpath is to get substituted abstract locaion values. It also returns a set of abstract locations containing non-allocsite locations from the substitution results. Since the key of ArrayBlk.t is AbsLoc.Allocsite.t, they cannot be written in this domain.
Return size of the array block. If cost_mode is true, it returns a conservative (bigger than correct one), but not correct size results.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/BO__BufferOverrunDomain/AliasTargets/index.html b/website/static/odoc/next/infer/BO__BufferOverrunDomain/AliasTargets/index.html
index 41cae7f23..61eda27a2 100644
--- a/website/static/odoc/next/infer/BO__BufferOverrunDomain/AliasTargets/index.html
+++ b/website/static/odoc/next/infer/BO__BufferOverrunDomain/AliasTargets/index.html
@@ -1,2 +1,2 @@
-AliasTargets (infer.BO__BufferOverrunDomain.AliasTargets)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/BO__BufferOverrunDomain/PrunePairs/index.html b/website/static/odoc/next/infer/BO__BufferOverrunDomain/PrunePairs/index.html
index 2187bb4d6..1c3ec04be 100644
--- a/website/static/odoc/next/infer/BO__BufferOverrunDomain/PrunePairs/index.html
+++ b/website/static/odoc/next/infer/BO__BufferOverrunDomain/PrunePairs/index.html
@@ -1,2 +1,2 @@
-PrunePairs (infer.BO__BufferOverrunDomain.PrunePairs)
Module BO__BufferOverrunDomain.PrunePairs
PrunePairs is a map from abstract locations to abstract values that represents pruned results in the latest pruning. It uses InvertedMap because more pruning means smaller abstract states.
Check if a path is reachable, by using its pruned values
\ No newline at end of file
+PrunePairs (infer.BO__BufferOverrunDomain.PrunePairs)
Module BO__BufferOverrunDomain.PrunePairs
PrunePairs is a map from abstract locations to abstract values that represents pruned results in the latest pruning. It uses InvertedMap because more pruning means smaller abstract states.
Check if a path is reachable, by using its pruned values
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Backend/ClosuresSubstitution/Domain/index.html b/website/static/odoc/next/infer/Backend/ClosuresSubstitution/Domain/index.html
index b390a8fbb..5909a6f22 100644
--- a/website/static/odoc/next/infer/Backend/ClosuresSubstitution/Domain/index.html
+++ b/website/static/odoc/next/infer/Backend/ClosuresSubstitution/Domain/index.html
@@ -1,2 +1,2 @@
-Domain (infer.Backend.ClosuresSubstitution.Domain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Backend__ClosuresSubstitution/Domain/index.html b/website/static/odoc/next/infer/Backend__ClosuresSubstitution/Domain/index.html
index 1c57c33bf..e0aa3d124 100644
--- a/website/static/odoc/next/infer/Backend__ClosuresSubstitution/Domain/index.html
+++ b/website/static/odoc/next/infer/Backend__ClosuresSubstitution/Domain/index.html
@@ -1,2 +1,2 @@
-Domain (infer.Backend__ClosuresSubstitution.Domain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers/AnnotationReachabilityDomain/SinkMap/index.html b/website/static/odoc/next/infer/Checkers/AnnotationReachabilityDomain/SinkMap/index.html
index ea51bd795..4ab05d7d4 100644
--- a/website/static/odoc/next/infer/Checkers/AnnotationReachabilityDomain/SinkMap/index.html
+++ b/website/static/odoc/next/infer/Checkers/AnnotationReachabilityDomain/SinkMap/index.html
@@ -1,2 +1,2 @@
-SinkMap (infer.Checkers.AnnotationReachabilityDomain.SinkMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers/AnnotationReachabilityDomain/index.html b/website/static/odoc/next/infer/Checkers/AnnotationReachabilityDomain/index.html
index 6c71d8c52..4ce1ff1ee 100644
--- a/website/static/odoc/next/infer/Checkers/AnnotationReachabilityDomain/index.html
+++ b/website/static/odoc/next/infer/Checkers/AnnotationReachabilityDomain/index.html
@@ -1,2 +1,2 @@
-AnnotationReachabilityDomain (infer.Checkers.AnnotationReachabilityDomain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers/ReachingDefs/ReachingDefsMap/index.html b/website/static/odoc/next/infer/Checkers/ReachingDefs/ReachingDefsMap/index.html
index 6c9faa28f..427636020 100644
--- a/website/static/odoc/next/infer/Checkers/ReachingDefs/ReachingDefsMap/index.html
+++ b/website/static/odoc/next/infer/Checkers/ReachingDefs/ReachingDefsMap/index.html
@@ -1,2 +1,2 @@
-ReachingDefsMap (infer.Checkers.ReachingDefs.ReachingDefsMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers__AnnotationReachabilityDomain/SinkMap/index.html b/website/static/odoc/next/infer/Checkers__AnnotationReachabilityDomain/SinkMap/index.html
index 707ccb1d5..d1afa5e8f 100644
--- a/website/static/odoc/next/infer/Checkers__AnnotationReachabilityDomain/SinkMap/index.html
+++ b/website/static/odoc/next/infer/Checkers__AnnotationReachabilityDomain/SinkMap/index.html
@@ -1,2 +1,2 @@
-SinkMap (infer.Checkers__AnnotationReachabilityDomain.SinkMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers__AnnotationReachabilityDomain/index.html b/website/static/odoc/next/infer/Checkers__AnnotationReachabilityDomain/index.html
index ccc1c0548..ff40bb139 100644
--- a/website/static/odoc/next/infer/Checkers__AnnotationReachabilityDomain/index.html
+++ b/website/static/odoc/next/infer/Checkers__AnnotationReachabilityDomain/index.html
@@ -1,2 +1,2 @@
-Checkers__AnnotationReachabilityDomain (infer.Checkers__AnnotationReachabilityDomain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers__ReachingDefs/ReachingDefsMap/index.html b/website/static/odoc/next/infer/Checkers__ReachingDefs/ReachingDefsMap/index.html
index 044954f0a..fe7fac83c 100644
--- a/website/static/odoc/next/infer/Checkers__ReachingDefs/ReachingDefsMap/index.html
+++ b/website/static/odoc/next/infer/Checkers__ReachingDefs/ReachingDefsMap/index.html
@@ -1,2 +1,2 @@
-ReachingDefsMap (infer.Checkers__ReachingDefs.ReachingDefsMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency/RacerDDomain/AttributeMapDomain/index.html b/website/static/odoc/next/infer/Concurrency/RacerDDomain/AttributeMapDomain/index.html
index 9a6b538ce..545bc9408 100644
--- a/website/static/odoc/next/infer/Concurrency/RacerDDomain/AttributeMapDomain/index.html
+++ b/website/static/odoc/next/infer/Concurrency/RacerDDomain/AttributeMapDomain/index.html
@@ -1,2 +1,2 @@
-AttributeMapDomain (infer.Concurrency.RacerDDomain.AttributeMapDomain)
propagate attributes from the leaves to the root of an RHS Hil expression
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency/StarvationDomain/AttributeDomain/index.html b/website/static/odoc/next/infer/Concurrency/StarvationDomain/AttributeDomain/index.html
index a3219cd8c..1902d0f5d 100644
--- a/website/static/odoc/next/infer/Concurrency/StarvationDomain/AttributeDomain/index.html
+++ b/website/static/odoc/next/infer/Concurrency/StarvationDomain/AttributeDomain/index.html
@@ -1,2 +1,2 @@
-AttributeDomain (infer.Concurrency.StarvationDomain.AttributeDomain)
Module StarvationDomain.AttributeDomain
Tracks all expressions assigned values of Attribute
does the given expr has attribute FutureDone x return Some x else None
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency__RacerDDomain/AttributeMapDomain/index.html b/website/static/odoc/next/infer/Concurrency__RacerDDomain/AttributeMapDomain/index.html
index a766cfe4d..5ca3108bf 100644
--- a/website/static/odoc/next/infer/Concurrency__RacerDDomain/AttributeMapDomain/index.html
+++ b/website/static/odoc/next/infer/Concurrency__RacerDDomain/AttributeMapDomain/index.html
@@ -1,2 +1,2 @@
-AttributeMapDomain (infer.Concurrency__RacerDDomain.AttributeMapDomain)
propagate attributes from the leaves to the root of an RHS Hil expression
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency__StarvationDomain/AttributeDomain/index.html b/website/static/odoc/next/infer/Concurrency__StarvationDomain/AttributeDomain/index.html
index c871799dc..ba57b988e 100644
--- a/website/static/odoc/next/infer/Concurrency__StarvationDomain/AttributeDomain/index.html
+++ b/website/static/odoc/next/infer/Concurrency__StarvationDomain/AttributeDomain/index.html
@@ -1,2 +1,2 @@
-AttributeDomain (infer.Concurrency__StarvationDomain.AttributeDomain)
does the given expr has attribute FutureDone x return Some x else None
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Costlib/CostModels/NSAttributedString/index.html b/website/static/odoc/next/infer/Costlib/CostModels/NSAttributedString/index.html
new file mode 100644
index 000000000..39d4fdd3d
--- /dev/null
+++ b/website/static/odoc/next/infer/Costlib/CostModels/NSAttributedString/index.html
@@ -0,0 +1,2 @@
+
+NSAttributedString (infer.Costlib.CostModels.NSAttributedString)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Costlib__CostModels/NSAttributedString/index.html b/website/static/odoc/next/infer/Costlib__CostModels/NSAttributedString/index.html
new file mode 100644
index 000000000..d4dbbaf07
--- /dev/null
+++ b/website/static/odoc/next/infer/Costlib__CostModels/NSAttributedString/index.html
@@ -0,0 +1,2 @@
+
+NSAttributedString (infer.Costlib__CostModels.NSAttributedString)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ErlangFrontend/.dune-keep b/website/static/odoc/next/infer/ErlangFrontend/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/ErlangFrontend/ErlangAst/index.html b/website/static/odoc/next/infer/ErlangFrontend/ErlangAst/index.html
new file mode 100644
index 000000000..3349d294f
--- /dev/null
+++ b/website/static/odoc/next/infer/ErlangFrontend/ErlangAst/index.html
@@ -0,0 +1,2 @@
+
+ErlangAst (infer.ErlangFrontend.ErlangAst)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ErlangFrontend/ErlangJsonParser/index.html b/website/static/odoc/next/infer/ErlangFrontend/ErlangJsonParser/index.html
new file mode 100644
index 000000000..2f6cf39c5
--- /dev/null
+++ b/website/static/odoc/next/infer/ErlangFrontend/ErlangJsonParser/index.html
@@ -0,0 +1,2 @@
+
+ErlangJsonParser (infer.ErlangFrontend.ErlangJsonParser)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ErlangFrontend/ErlangTranslator/index.html b/website/static/odoc/next/infer/ErlangFrontend/ErlangTranslator/index.html
new file mode 100644
index 000000000..246beb4ca
--- /dev/null
+++ b/website/static/odoc/next/infer/ErlangFrontend/ErlangTranslator/index.html
@@ -0,0 +1,2 @@
+
+ErlangTranslator (infer.ErlangFrontend.ErlangTranslator)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ErlangFrontend/index.html b/website/static/odoc/next/infer/ErlangFrontend/index.html
new file mode 100644
index 000000000..5f3b5ced8
--- /dev/null
+++ b/website/static/odoc/next/infer/ErlangFrontend/index.html
@@ -0,0 +1,2 @@
+
+ErlangFrontend (infer.ErlangFrontend)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ErlangFrontend__ErlangAst/.dune-keep b/website/static/odoc/next/infer/ErlangFrontend__ErlangAst/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/ErlangFrontend__ErlangAst/index.html b/website/static/odoc/next/infer/ErlangFrontend__ErlangAst/index.html
new file mode 100644
index 000000000..03ab8ca78
--- /dev/null
+++ b/website/static/odoc/next/infer/ErlangFrontend__ErlangAst/index.html
@@ -0,0 +1,2 @@
+
+ErlangFrontend__ErlangAst (infer.ErlangFrontend__ErlangAst)
Module ErlangFrontend__ErlangAst
Erlang abstract forms, following https://erlang.org/doc/apps/erts/absform.html
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ErlangFrontend__ErlangJsonParser/.dune-keep b/website/static/odoc/next/infer/ErlangFrontend__ErlangJsonParser/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/ErlangFrontend__ErlangJsonParser/index.html b/website/static/odoc/next/infer/ErlangFrontend__ErlangJsonParser/index.html
new file mode 100644
index 000000000..4539d6a05
--- /dev/null
+++ b/website/static/odoc/next/infer/ErlangFrontend__ErlangJsonParser/index.html
@@ -0,0 +1,2 @@
+
+ErlangFrontend__ErlangJsonParser (infer.ErlangFrontend__ErlangJsonParser)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ErlangFrontend__ErlangTranslator/.dune-keep b/website/static/odoc/next/infer/ErlangFrontend__ErlangTranslator/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/ErlangFrontend__ErlangTranslator/index.html b/website/static/odoc/next/infer/ErlangFrontend__ErlangTranslator/index.html
new file mode 100644
index 000000000..7b66be463
--- /dev/null
+++ b/website/static/odoc/next/infer/ErlangFrontend__ErlangTranslator/index.html
@@ -0,0 +1,2 @@
+
+ErlangFrontend__ErlangTranslator (infer.ErlangFrontend__ErlangTranslator)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase/Config/index.html b/website/static/odoc/next/infer/IBase/Config/index.html
index 313457dab..c560ab421 100644
--- a/website/static/odoc/next/infer/IBase/Config/index.html
+++ b/website/static/odoc/next/infer/IBase/Config/index.html
@@ -1,2 +1,2 @@
-Config (infer.IBase.Config)
val scuba_normals : string IStdlib.IStd.String.Map.t
val scuba_tags : string listIStdlib.IStd.String.Map.t
val select : [ `All | `Select of int ] option
val show_buckets : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
val skip_analysis_in_path : string list
val skip_analysis_in_path_skips_compilation : bool
val skip_duplicated_types : bool
val skip_non_capture_clang_commands : bool
val skip_translation_headers : string list
val source_files : bool
val source_files_cfg : bool
val source_files_filter : string option
val source_files_freshly_captured : bool
val source_files_procedure_names : bool
val source_files_type_environment : bool
val source_preview : bool
val sourcepath : string option
val sources : string list
val sqlite_cache_size : int
val sqlite_page_size : int
val sqlite_lock_timeout : int
val sqlite_vfs : string option
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
val starvation_whole_program : bool
val subtype_multirange : bool
val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val tenv_json : string option
val test_determinator : bool
val export_changed_functions : bool
val test_filtering : bool
val testing_mode : bool
val threadsafe_aliases : Yojson.Basic.t
val topl_max_conjuncts : int
val topl_max_disjuncts : int
val topl_properties : string list
val trace_absarray : bool
val trace_error : bool
val trace_events : bool
val trace_ondemand : bool
val trace_topl : bool
val tv_commit : string option
val tv_limit : int
val tv_limit_filtered : int
val uninit_interproc : bool
val workspace : string option
val write_html : bool
val write_html_whitelist_regex : string list
val write_website : string option
val xcode_developer_dir : string option
val xcode_isysroot_suffix : string option
val xcpretty : bool
Configuration values derived from command-line options
val dynamic_dispatch : bool
val toplevel_results_dir : string
In some integrations, eg Buck, infer subprocesses started by the build system (started by the toplevel infer process) will have their own results directory; this points to the results directory of the toplevel infer process, which can be useful for, eg, storing debug info. In other cases this is equal to results_dir.
val is_in_custom_symbols : string -> string -> bool
Does named symbol match any prefix in the named custom symbol list?
val java_package_is_external : string -> bool
Check if a Java package is external to the repository
val scuba_execution_id : IStdlib.IStd.Int64.t option
a random number to (hopefully) uniquely identify this run
Global variables with initial values specified by command-line options
val clang_compilation_dbs : [ `Escaped of string| `Raw of string ] list
\ No newline at end of file
+Config (infer.IBase.Config)
val scuba_normals : string IStdlib.IStd.String.Map.t
val scuba_tags : string listIStdlib.IStd.String.Map.t
val select : [ `All | `Select of int ] option
val show_buckets : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
val skip_analysis_in_path : string list
val skip_analysis_in_path_skips_compilation : bool
val skip_duplicated_types : bool
val skip_non_capture_clang_commands : bool
val skip_translation_headers : string list
val source_files : bool
val source_files_cfg : bool
val source_files_filter : string option
val source_files_freshly_captured : bool
val source_files_procedure_names : bool
val source_files_type_environment : bool
val source_preview : bool
val sourcepath : string option
val sources : string list
val sqlite_cache_size : int
val sqlite_page_size : int
val sqlite_lock_timeout : int
val sqlite_vfs : string option
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
val starvation_whole_program : bool
val subtype_multirange : bool
val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val tenv_json : string option
val test_determinator : bool
val export_changed_functions : bool
val test_filtering : bool
val testing_mode : bool
val threadsafe_aliases : Yojson.Basic.t
val topl_max_conjuncts : int
val topl_max_disjuncts : int
val topl_properties : string list
val trace_absarray : bool
val trace_error : bool
val trace_events : bool
val trace_ondemand : bool
val trace_topl : bool
val tv_commit : string option
val tv_limit : int
val tv_limit_filtered : int
val uninit_interproc : bool
val workspace : string option
val write_html : bool
val write_html_whitelist_regex : string list
val write_website : string option
val xcode_developer_dir : string option
val xcode_isysroot_suffix : string option
val xcpretty : bool
Configuration values derived from command-line options
val dynamic_dispatch : bool
val toplevel_results_dir : string
In some integrations, eg Buck, infer subprocesses started by the build system (started by the toplevel infer process) will have their own results directory; this points to the results directory of the toplevel infer process, which can be useful for, eg, storing debug info. In other cases this is equal to results_dir.
val is_in_custom_symbols : string -> string -> bool
Does named symbol match any prefix in the named custom symbol list?
val java_package_is_external : string -> bool
Check if a Java package is external to the repository
val scuba_execution_id : IStdlib.IStd.Int64.t option
a random number to (hopefully) uniquely identify this run
Global variables with initial values specified by command-line options
val clang_compilation_dbs : [ `Escaped of string| `Raw of string ] list
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase__Config/index.html b/website/static/odoc/next/infer/IBase__Config/index.html
index 7f54c3b98..679fe885b 100644
--- a/website/static/odoc/next/infer/IBase__Config/index.html
+++ b/website/static/odoc/next/infer/IBase__Config/index.html
@@ -1,2 +1,2 @@
-IBase__Config (infer.IBase__Config)
val scuba_normals : string IStdlib.IStd.String.Map.t
val scuba_tags : string listIStdlib.IStd.String.Map.t
val select : [ `All | `Select of int ] option
val show_buckets : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
val skip_analysis_in_path : string list
val skip_analysis_in_path_skips_compilation : bool
val skip_duplicated_types : bool
val skip_non_capture_clang_commands : bool
val skip_translation_headers : string list
val source_files : bool
val source_files_cfg : bool
val source_files_filter : string option
val source_files_freshly_captured : bool
val source_files_procedure_names : bool
val source_files_type_environment : bool
val source_preview : bool
val sourcepath : string option
val sources : string list
val sqlite_cache_size : int
val sqlite_page_size : int
val sqlite_lock_timeout : int
val sqlite_vfs : string option
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
val starvation_whole_program : bool
val subtype_multirange : bool
val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val tenv_json : string option
val test_determinator : bool
val export_changed_functions : bool
val test_filtering : bool
val testing_mode : bool
val threadsafe_aliases : Yojson.Basic.t
val topl_max_conjuncts : int
val topl_max_disjuncts : int
val topl_properties : string list
val trace_absarray : bool
val trace_error : bool
val trace_events : bool
val trace_ondemand : bool
val trace_topl : bool
val tv_commit : string option
val tv_limit : int
val tv_limit_filtered : int
val uninit_interproc : bool
val workspace : string option
val write_html : bool
val write_html_whitelist_regex : string list
val write_website : string option
val xcode_developer_dir : string option
val xcode_isysroot_suffix : string option
val xcpretty : bool
Configuration values derived from command-line options
val dynamic_dispatch : bool
val toplevel_results_dir : string
In some integrations, eg Buck, infer subprocesses started by the build system (started by the toplevel infer process) will have their own results directory; this points to the results directory of the toplevel infer process, which can be useful for, eg, storing debug info. In other cases this is equal to results_dir.
val is_in_custom_symbols : string -> string -> bool
Does named symbol match any prefix in the named custom symbol list?
val java_package_is_external : string -> bool
Check if a Java package is external to the repository
val scuba_execution_id : IStdlib.IStd.Int64.t option
a random number to (hopefully) uniquely identify this run
Global variables with initial values specified by command-line options
val clang_compilation_dbs : [ `Escaped of string| `Raw of string ] list
\ No newline at end of file
+IBase__Config (infer.IBase__Config)
val scuba_normals : string IStdlib.IStd.String.Map.t
val scuba_tags : string listIStdlib.IStd.String.Map.t
val select : [ `All | `Select of int ] option
val show_buckets : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
val skip_analysis_in_path : string list
val skip_analysis_in_path_skips_compilation : bool
val skip_duplicated_types : bool
val skip_non_capture_clang_commands : bool
val skip_translation_headers : string list
val source_files : bool
val source_files_cfg : bool
val source_files_filter : string option
val source_files_freshly_captured : bool
val source_files_procedure_names : bool
val source_files_type_environment : bool
val source_preview : bool
val sourcepath : string option
val sources : string list
val sqlite_cache_size : int
val sqlite_page_size : int
val sqlite_lock_timeout : int
val sqlite_vfs : string option
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
val starvation_whole_program : bool
val subtype_multirange : bool
val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val tenv_json : string option
val test_determinator : bool
val export_changed_functions : bool
val test_filtering : bool
val testing_mode : bool
val threadsafe_aliases : Yojson.Basic.t
val topl_max_conjuncts : int
val topl_max_disjuncts : int
val topl_properties : string list
val trace_absarray : bool
val trace_error : bool
val trace_events : bool
val trace_ondemand : bool
val trace_topl : bool
val tv_commit : string option
val tv_limit : int
val tv_limit_filtered : int
val uninit_interproc : bool
val workspace : string option
val write_html : bool
val write_html_whitelist_regex : string list
val write_website : string option
val xcode_developer_dir : string option
val xcode_isysroot_suffix : string option
val xcpretty : bool
Configuration values derived from command-line options
val dynamic_dispatch : bool
val toplevel_results_dir : string
In some integrations, eg Buck, infer subprocesses started by the build system (started by the toplevel infer process) will have their own results directory; this points to the results directory of the toplevel infer process, which can be useful for, eg, storing debug info. In other cases this is equal to results_dir.
val is_in_custom_symbols : string -> string -> bool
Does named symbol match any prefix in the named custom symbol list?
val java_package_is_external : string -> bool
Check if a Java package is external to the repository
val scuba_execution_id : IStdlib.IStd.Int64.t option
a random number to (hopefully) uniquely identify this run
Global variables with initial values specified by command-line options
val clang_compilation_dbs : [ `Escaped of string| `Raw of string ] list
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR/ObjCDispatchModels/index.html b/website/static/odoc/next/infer/IR/ObjCDispatchModels/index.html
new file mode 100644
index 000000000..2db3c99a6
--- /dev/null
+++ b/website/static/odoc/next/infer/IR/ObjCDispatchModels/index.html
@@ -0,0 +1,2 @@
+
+ObjCDispatchModels (infer.IR.ObjCDispatchModels)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR/Procname/Erlang/index.html b/website/static/odoc/next/infer/IR/Procname/Erlang/index.html
new file mode 100644
index 000000000..798704c3d
--- /dev/null
+++ b/website/static/odoc/next/infer/IR/Procname/Erlang/index.html
@@ -0,0 +1,2 @@
+
+Erlang (infer.IR.Procname.Erlang)
Module Procname.Erlang
type t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR__ObjCDispatchModels/.dune-keep b/website/static/odoc/next/infer/IR__ObjCDispatchModels/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/IR__ObjCDispatchModels/index.html b/website/static/odoc/next/infer/IR__ObjCDispatchModels/index.html
new file mode 100644
index 000000000..924049f5d
--- /dev/null
+++ b/website/static/odoc/next/infer/IR__ObjCDispatchModels/index.html
@@ -0,0 +1,2 @@
+
+IR__ObjCDispatchModels (infer.IR__ObjCDispatchModels)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR__Procname/Erlang/index.html b/website/static/odoc/next/infer/IR__Procname/Erlang/index.html
new file mode 100644
index 000000000..146cb7280
--- /dev/null
+++ b/website/static/odoc/next/infer/IR__Procname/Erlang/index.html
@@ -0,0 +1,2 @@
+
+Erlang (infer.IR__Procname.Erlang)
Module IR__Procname.Erlang
type t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib/ISys/index.html b/website/static/odoc/next/infer/IStdlib/ISys/index.html
new file mode 100644
index 000000000..9d29b2acc
--- /dev/null
+++ b/website/static/odoc/next/infer/IStdlib/ISys/index.html
@@ -0,0 +1,2 @@
+
+ISys (infer.IStdlib.ISys)
Module IStdlib.ISys
val file_exists : ?follow_symlinks:bool-> string -> bool
Similar to Sys.file_exists_exn, but it returns false when the result is unknown, instead of raising an exception. follow_symlinks is true by default.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib/PrettyPrintable/MakePPMonoMap/index.html b/website/static/odoc/next/infer/IStdlib/PrettyPrintable/MakePPMonoMap/index.html
index 25a8f5b46..f795d6f61 100644
--- a/website/static/odoc/next/infer/IStdlib/PrettyPrintable/MakePPMonoMap/index.html
+++ b/website/static/odoc/next/infer/IStdlib/PrettyPrintable/MakePPMonoMap/index.html
@@ -1,2 +1,2 @@
-MakePPMonoMap (infer.IStdlib.PrettyPrintable.MakePPMonoMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib/PrettyPrintable/PPMonoMapOfPPMap/index.html b/website/static/odoc/next/infer/IStdlib/PrettyPrintable/PPMonoMapOfPPMap/index.html
index fcac501af..8ee043982 100644
--- a/website/static/odoc/next/infer/IStdlib/PrettyPrintable/PPMonoMapOfPPMap/index.html
+++ b/website/static/odoc/next/infer/IStdlib/PrettyPrintable/PPMonoMapOfPPMap/index.html
@@ -1,2 +1,2 @@
-PPMonoMapOfPPMap (infer.IStdlib.PrettyPrintable.PPMonoMapOfPPMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib/PrettyPrintable/module-type-MonoMap/index.html b/website/static/odoc/next/infer/IStdlib/PrettyPrintable/module-type-MonoMap/index.html
index a7ce67aab..feabf45a2 100644
--- a/website/static/odoc/next/infer/IStdlib/PrettyPrintable/module-type-MonoMap/index.html
+++ b/website/static/odoc/next/infer/IStdlib/PrettyPrintable/module-type-MonoMap/index.html
@@ -1,2 +1,2 @@
-MonoMap (infer.IStdlib.PrettyPrintable.MonoMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib/PrettyPrintable/module-type-PPMonoMap/index.html b/website/static/odoc/next/infer/IStdlib/PrettyPrintable/module-type-PPMonoMap/index.html
index 459ca699c..e809d1919 100644
--- a/website/static/odoc/next/infer/IStdlib/PrettyPrintable/module-type-PPMonoMap/index.html
+++ b/website/static/odoc/next/infer/IStdlib/PrettyPrintable/module-type-PPMonoMap/index.html
@@ -1,2 +1,2 @@
-PPMonoMap (infer.IStdlib.PrettyPrintable.PPMonoMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib/RecencyMap/Make/index.html b/website/static/odoc/next/infer/IStdlib/RecencyMap/Make/index.html
index a343b778c..c5191ad75 100644
--- a/website/static/odoc/next/infer/IStdlib/RecencyMap/Make/index.html
+++ b/website/static/odoc/next/infer/IStdlib/RecencyMap/Make/index.html
@@ -1,2 +1,2 @@
-Make (infer.IStdlib.RecencyMap.Make)
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib/RecencyMap/module-type-S/index.html b/website/static/odoc/next/infer/IStdlib/RecencyMap/module-type-S/index.html
index 2328b7b1b..cf06fd47b 100644
--- a/website/static/odoc/next/infer/IStdlib/RecencyMap/module-type-S/index.html
+++ b/website/static/odoc/next/infer/IStdlib/RecencyMap/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (infer.IStdlib.RecencyMap.S)
Module type RecencyMap.S
A functional map interface where only the N most recently-accessed elements are guaranteed to be persisted, similarly to an LRU cache. The map stores at most 2*N elements.
type t
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
+S (infer.IStdlib.RecencyMap.S)
Module type RecencyMap.S
A functional map interface where only the N most recently-accessed elements are guaranteed to be persisted, similarly to an LRU cache. The map stores at most 2*N elements.
type t
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib__ISys/.dune-keep b/website/static/odoc/next/infer/IStdlib__ISys/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/IStdlib__ISys/index.html b/website/static/odoc/next/infer/IStdlib__ISys/index.html
new file mode 100644
index 000000000..38218e696
--- /dev/null
+++ b/website/static/odoc/next/infer/IStdlib__ISys/index.html
@@ -0,0 +1,2 @@
+
+IStdlib__ISys (infer.IStdlib__ISys)
Module IStdlib__ISys
val file_exists : ?follow_symlinks:bool-> string -> bool
Similar to Sys.file_exists_exn, but it returns false when the result is unknown, instead of raising an exception. follow_symlinks is true by default.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib__PrettyPrintable/MakePPMonoMap/index.html b/website/static/odoc/next/infer/IStdlib__PrettyPrintable/MakePPMonoMap/index.html
index 9a4a3cbe3..7d90426cb 100644
--- a/website/static/odoc/next/infer/IStdlib__PrettyPrintable/MakePPMonoMap/index.html
+++ b/website/static/odoc/next/infer/IStdlib__PrettyPrintable/MakePPMonoMap/index.html
@@ -1,2 +1,2 @@
-MakePPMonoMap (infer.IStdlib__PrettyPrintable.MakePPMonoMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib__PrettyPrintable/PPMonoMapOfPPMap/index.html b/website/static/odoc/next/infer/IStdlib__PrettyPrintable/PPMonoMapOfPPMap/index.html
index 901b1bace..ddb58986a 100644
--- a/website/static/odoc/next/infer/IStdlib__PrettyPrintable/PPMonoMapOfPPMap/index.html
+++ b/website/static/odoc/next/infer/IStdlib__PrettyPrintable/PPMonoMapOfPPMap/index.html
@@ -1,2 +1,2 @@
-PPMonoMapOfPPMap (infer.IStdlib__PrettyPrintable.PPMonoMapOfPPMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib__PrettyPrintable/module-type-MonoMap/index.html b/website/static/odoc/next/infer/IStdlib__PrettyPrintable/module-type-MonoMap/index.html
index 94502f014..54886b6f2 100644
--- a/website/static/odoc/next/infer/IStdlib__PrettyPrintable/module-type-MonoMap/index.html
+++ b/website/static/odoc/next/infer/IStdlib__PrettyPrintable/module-type-MonoMap/index.html
@@ -1,2 +1,2 @@
-MonoMap (infer.IStdlib__PrettyPrintable.MonoMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib__PrettyPrintable/module-type-PPMonoMap/index.html b/website/static/odoc/next/infer/IStdlib__PrettyPrintable/module-type-PPMonoMap/index.html
index 118073938..585d3b3a2 100644
--- a/website/static/odoc/next/infer/IStdlib__PrettyPrintable/module-type-PPMonoMap/index.html
+++ b/website/static/odoc/next/infer/IStdlib__PrettyPrintable/module-type-PPMonoMap/index.html
@@ -1,2 +1,2 @@
-PPMonoMap (infer.IStdlib__PrettyPrintable.PPMonoMap)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib__RecencyMap/Make/index.html b/website/static/odoc/next/infer/IStdlib__RecencyMap/Make/index.html
index fddda1ce8..4ffd57b7c 100644
--- a/website/static/odoc/next/infer/IStdlib__RecencyMap/Make/index.html
+++ b/website/static/odoc/next/infer/IStdlib__RecencyMap/Make/index.html
@@ -1,2 +1,2 @@
-Make (infer.IStdlib__RecencyMap.Make)
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IStdlib__RecencyMap/module-type-S/index.html b/website/static/odoc/next/infer/IStdlib__RecencyMap/module-type-S/index.html
index 1f195844f..732d353f4 100644
--- a/website/static/odoc/next/infer/IStdlib__RecencyMap/module-type-S/index.html
+++ b/website/static/odoc/next/infer/IStdlib__RecencyMap/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (infer.IStdlib__RecencyMap.S)
Module type IStdlib__RecencyMap.S
A functional map interface where only the N most recently-accessed elements are guaranteed to be persisted, similarly to an LRU cache. The map stores at most 2*N elements.
type t
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
+S (infer.IStdlib__RecencyMap.S)
Module type IStdlib__RecencyMap.S
A functional map interface where only the N most recently-accessed elements are guaranteed to be persisted, similarly to an LRU cache. The map stores at most 2*N elements.
type t
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration/Rebar3/index.html b/website/static/odoc/next/infer/Integration/Rebar3/index.html
new file mode 100644
index 000000000..9d80eb751
--- /dev/null
+++ b/website/static/odoc/next/infer/Integration/Rebar3/index.html
@@ -0,0 +1,2 @@
+
+Rebar3 (infer.Integration.Rebar3)
Module Integration.Rebar3
val capture : args:string list-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration__Rebar3/.dune-keep b/website/static/odoc/next/infer/Integration__Rebar3/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/Integration__Rebar3/index.html b/website/static/odoc/next/infer/Integration__Rebar3/index.html
new file mode 100644
index 000000000..428bca11f
--- /dev/null
+++ b/website/static/odoc/next/infer/Integration__Rebar3/index.html
@@ -0,0 +1,2 @@
+
+Integration__Rebar3 (infer.Integration__Rebar3)
Module Integration__Rebar3
val capture : args:string list-> unit
\ No newline at end of file
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 4bfc8aaaa..02b811741 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html
@@ -1,2 +1,2 @@
-AddressAttributes (infer.Pulselib.PulseAbductiveDomain.AddressAttributes)
Module PulseAbductiveDomain.AddressAttributes
attribute operations like BaseAddressAttributes but that also take care of propagating facts to the precondition
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/index.html b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/index.html
index 7de85e00c..856937bd2 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/index.html
@@ -1,2 +1,2 @@
-PulseAbductiveDomain (infer.Pulselib.PulseAbductiveDomain)
signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition
Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.
signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition
Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.
\ No newline at end of file
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 7272c8019..0fac4d254 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html
@@ -1,2 +1,2 @@
-Attributes (infer.Pulselib.PulseAttribute.Attributes)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html b/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html
index 63fb83759..ccf889e7e 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html
@@ -1,2 +1,2 @@
-PulseAttribute (infer.Pulselib.PulseAttribute)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html
index 6745b3414..0983b41db 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html
@@ -1,2 +1,2 @@
-PulseBaseAddressAttributes (infer.Pulselib.PulseBaseAddressAttributes)
merge the attributes of all the variables that are equal according to get_var_repr and remove non-canonical variables in favor of their rerpresentative
merge the attributes of all the variables that are equal according to get_var_repr and remove non-canonical variables in favor of their rerpresentative
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseDomain/GraphVisit/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseDomain/GraphVisit/index.html
new file mode 100644
index 000000000..81f5d7bb3
--- /dev/null
+++ b/website/static/odoc/next/infer/Pulselib/PulseBaseDomain/GraphVisit/index.html
@@ -0,0 +1,2 @@
+
+GraphVisit (infer.Pulselib.PulseBaseDomain.GraphVisit)
Generic graph traversal of the memory starting from each variable in the stack that pass var_filter, in order. Returns the result of folding over every address in the graph and the set of addresses that have been visited before f returned Stop or all reachable addresses were seen. f is passed each address together with the variable from which the address was reached and the access path from that variable to the address.
Similar to fold, but start from given addresses, instead of stack variables.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseDomain/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseDomain/index.html
index d6bb9f23b..2ee5afc86 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseBaseDomain/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseBaseDomain/index.html
@@ -1,2 +1,2 @@
-PulseBaseDomain (infer.Pulselib.PulseBaseDomain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseMemory/Edges/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseMemory/Edges/index.html
index ca722b39a..3ca9ecd9c 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseBaseMemory/Edges/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseBaseMemory/Edges/index.html
@@ -1,2 +1,2 @@
-Edges (infer.Pulselib.PulseBaseMemory.Edges)
Module PulseBaseMemory.Edges
type t
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
+Edges (infer.Pulselib.PulseBaseMemory.Edges)
Module PulseBaseMemory.Edges
type t
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseMemory/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseMemory/index.html
index f29d65ba6..bb982e73c 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseBaseMemory/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseBaseMemory/index.html
@@ -1,2 +1,2 @@
-PulseBaseMemory (infer.Pulselib.PulseBaseMemory)
replace each address in the heap by its canonical representative according to the current equality relation, represented by get_var_repr; also remove addresses that point to empty edges
replace each address in the heap by its canonical representative according to the current equality relation, represented by get_var_repr; also remove addresses that point to empty edges
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseStack/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseStack/index.html
index 2412d2507..32b406054 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseBaseStack/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseBaseStack/index.html
@@ -1,2 +1,2 @@
-PulseBaseStack (infer.Pulselib.PulseBaseStack)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseFormula/index.html b/website/static/odoc/next/infer/Pulselib/PulseFormula/index.html
index 61f61fe26..d9799c915 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseFormula/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseFormula/index.html
@@ -1,2 +1,2 @@
-PulseFormula (infer.Pulselib.PulseFormula)
get the canonical representative for the variable according to the both/pre+post equality relation
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulsePathCondition/index.html b/website/static/odoc/next/infer/Pulselib/PulsePathCondition/index.html
index 9a1bfcbdc..e5e05e6b3 100644
--- a/website/static/odoc/next/infer/Pulselib/PulsePathCondition/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulsePathCondition/index.html
@@ -1,2 +1,2 @@
-PulsePathCondition (infer.Pulselib.PulsePathCondition)
simplify ~can_be_pruned ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible, and tries to eliminate variables not in can_be_pruned from the "pruned" part of the formula
simplify ~can_be_pruned ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible, and tries to eliminate variables not in can_be_pruned from the "pruned" part of the formula
get the canonical representative for the variable according to the equality relation in the "both" (known + pruned) part of the formula
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseSkippedCalls/index.html b/website/static/odoc/next/infer/Pulselib/PulseSkippedCalls/index.html
index ea3378fb1..3d4074805 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseSkippedCalls/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseSkippedCalls/index.html
@@ -1,2 +1,2 @@
-PulseSkippedCalls (infer.Pulselib.PulseSkippedCalls)
\ No newline at end of file
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 d672b6776..a0325728e 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/AddressAttributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/AddressAttributes/index.html
@@ -1,2 +1,2 @@
-AddressAttributes (infer.Pulselib__PulseAbductiveDomain.AddressAttributes)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/index.html b/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/index.html
index d27102a84..286245c91 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseAbductiveDomain (infer.Pulselib__PulseAbductiveDomain)
signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition
Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.
signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition
Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.
\ No newline at end of file
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 a78e70a1f..e537a6cee 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseAttribute/Attributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseAttribute/Attributes/index.html
@@ -1,2 +1,2 @@
-Attributes (infer.Pulselib__PulseAttribute.Attributes)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseAttribute/index.html b/website/static/odoc/next/infer/Pulselib__PulseAttribute/index.html
index d5ef0c427..cfd531d31 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseAttribute/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseAttribute/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseAttribute (infer.Pulselib__PulseAttribute)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseBaseAddressAttributes/index.html b/website/static/odoc/next/infer/Pulselib__PulseBaseAddressAttributes/index.html
index 0cf78bbbd..aaf859a98 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseBaseAddressAttributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseBaseAddressAttributes/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseBaseAddressAttributes (infer.Pulselib__PulseBaseAddressAttributes)
merge the attributes of all the variables that are equal according to get_var_repr and remove non-canonical variables in favor of their rerpresentative
merge the attributes of all the variables that are equal according to get_var_repr and remove non-canonical variables in favor of their rerpresentative
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseBaseDomain/GraphVisit/index.html b/website/static/odoc/next/infer/Pulselib__PulseBaseDomain/GraphVisit/index.html
new file mode 100644
index 000000000..20b3de478
--- /dev/null
+++ b/website/static/odoc/next/infer/Pulselib__PulseBaseDomain/GraphVisit/index.html
@@ -0,0 +1,2 @@
+
+GraphVisit (infer.Pulselib__PulseBaseDomain.GraphVisit)
Generic graph traversal of the memory starting from each variable in the stack that pass var_filter, in order. Returns the result of folding over every address in the graph and the set of addresses that have been visited before f returned Stop or all reachable addresses were seen. f is passed each address together with the variable from which the address was reached and the access path from that variable to the address.
Similar to fold, but start from given addresses, instead of stack variables.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseBaseDomain/index.html b/website/static/odoc/next/infer/Pulselib__PulseBaseDomain/index.html
index d2d584cfc..b2aa5228d 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseBaseDomain/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseBaseDomain/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseBaseDomain (infer.Pulselib__PulseBaseDomain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseBaseMemory/Edges/index.html b/website/static/odoc/next/infer/Pulselib__PulseBaseMemory/Edges/index.html
index 7f820793c..af6cb87c6 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseBaseMemory/Edges/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseBaseMemory/Edges/index.html
@@ -1,2 +1,2 @@
-Edges (infer.Pulselib__PulseBaseMemory.Edges)
Module Pulselib__PulseBaseMemory.Edges
type t
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
+Edges (infer.Pulselib__PulseBaseMemory.Edges)
Module Pulselib__PulseBaseMemory.Edges
type t
Note that the derived compare and equal functions are sensitive to the underlying implementation and in particular won't equate some objects that denote the same map.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseBaseMemory/index.html b/website/static/odoc/next/infer/Pulselib__PulseBaseMemory/index.html
index ae82b4f17..6a8f99ce9 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseBaseMemory/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseBaseMemory/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseBaseMemory (infer.Pulselib__PulseBaseMemory)
replace each address in the heap by its canonical representative according to the current equality relation, represented by get_var_repr; also remove addresses that point to empty edges
replace each address in the heap by its canonical representative according to the current equality relation, represented by get_var_repr; also remove addresses that point to empty edges
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseBaseStack/index.html b/website/static/odoc/next/infer/Pulselib__PulseBaseStack/index.html
index f9e01fa69..4cc568119 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseBaseStack/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseBaseStack/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseBaseStack (infer.Pulselib__PulseBaseStack)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseFormula/index.html b/website/static/odoc/next/infer/Pulselib__PulseFormula/index.html
index f6f6f9063..4df7d3bef 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseFormula/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseFormula/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseFormula (infer.Pulselib__PulseFormula)
get the canonical representative for the variable according to the both/pre+post equality relation
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulsePathCondition/index.html b/website/static/odoc/next/infer/Pulselib__PulsePathCondition/index.html
index de50d70c5..53eb6c47b 100644
--- a/website/static/odoc/next/infer/Pulselib__PulsePathCondition/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulsePathCondition/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulsePathCondition (infer.Pulselib__PulsePathCondition)
simplify ~can_be_pruned ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible, and tries to eliminate variables not in can_be_pruned from the "pruned" part of the formula
simplify ~can_be_pruned ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible, and tries to eliminate variables not in can_be_pruned from the "pruned" part of the formula
get the canonical representative for the variable according to the equality relation in the "both" (known + pruned) part of the formula
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseSkippedCalls/index.html b/website/static/odoc/next/infer/Pulselib__PulseSkippedCalls/index.html
index a4f273f21..c58361e25 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseSkippedCalls/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseSkippedCalls/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseSkippedCalls (infer.Pulselib__PulseSkippedCalls)