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.

Jules Villard df49f318f6 [pulse] havoc formals passed by reference to unknown procedures ... Summary: This gets rid of false positives when something invalid (eg null) is passed by reference to an initialisation function. Havoc'ing what the contents of the pointer to results in being optimistic about said contents in the future. Also surprisingly gets rid of some FNs (which means it can also introduce FPs) in the `std::atomic` tests because a path condition becomes feasible with havoc'ing. There's a slight refinement possible where we don't havoc pointers to const but that's more involved and left as future work. Reviewed By: skcho Differential Revision: D18726203 fbshipit-source-id: 264b5daeb		5 years ago
..
Makefile	[pulse][impurity] Use pulse for detecting impurity	5 years ago
array_test.cpp	[pulse][impurity] Use pulse for detecting impurity	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] havoc formals passed by reference to unknown procedures	5 years ago
param_test.cpp	[pulse][impurity] Use pulse for detecting impurity	5 years ago
unmodeled.cpp	[pulse] havoc formals passed by reference to unknown procedures	5 years ago
vector.cpp	[pulse] havoc formals passed by reference to unknown procedures	5 years ago