You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Sungkeun Cho b7b7e89159 [pulse] Address some modeled fields as pointers ... Summary: This diff addresses `GenericArrayBackedCollection.field` and others as pointers. The modeled fields are used as non-pointer struct fields, but their actual semantics are pointers that may have side effects. For example, `GenericArrayBackedCollection.field` is used for keeping an information that the previous vector's address could be invalid. ``` void foo(vector v) { v.push_back(0); // v's previous address may be invalid after push_back // PRE: {v -> {backing_array -> v1}} // POST: {v -> {backing_array -> v2}} // ATTR: {v1 may be invalidated} } ``` However, if we revert the modeled field values, it will return incorrect summary as follows, by reverting non-pointer parameter values. ``` // PRE: {v -> {backing_array -> v1}} // POST: {v -> {backing_array -> v1}} // ATTR: {v1 may be invalidated} ``` Reviewed By: jvillard Differential Revision: D28324161 fbshipit-source-id: 96451d4b0		4 years ago
..
Makefile	[biabd] rename test directories from {biabduction,errors,infer} to {biabduction}	5 years ago
array_test.cpp	[impurity] Consider functions with empty pulse summary as impure	5 years ago
exit_test.cpp	[impurity] Consider exited functions as impure	5 years ago
global_test.cpp	[pulse][impurity] Use pulse for detecting impurity	5 years ago
invalid_test.cpp	[impurity] Start checking equivalence at materialized addresses in pre	5 years ago
issues.exp	[pulse] Address some modeled fields as pointers	4 years ago
param_test.cpp	[pulse][impurity] Use pulse for detecting impurity	5 years ago
struct_test.cpp	[pulse] Only propagate existing WrittenTo attributes at function calls	5 years ago
unmodeled.cpp	[impurity] Rely on set of skipped functions to determine impurity	5 years ago
vector.cpp	[pulse] havoc formals passed by reference to unknown procedures	5 years ago