Summary:
This diff does not copy callee's parameters on instantiating abstract
memories at call sites. Before this diff, it copied all reachable
values from callee's parameters including the parameters themselves.
However, they are local variables of callees and should not be copied
to callers.
Reviewed By: mbouaziz
Differential Revision: D13877370
fbshipit-source-id: d70c2c317
Summary: We do not want to export unnecessary information from clang plugin, hence, the solution to this false positive would be to annotate with `__unused__` attribute.
Reviewed By: jvillard
Differential Revision: D13861333
fbshipit-source-id: 774009f37
Summary:
This will allow to get the numerical results for Cost, Hoisting, Purity without the Inferbo issues.
For now, I still forced Inferbo issues for Cost and Purity to avoid lots of changes in tests, that will go away soon.
Reviewed By: ezgicicek, skcho
Differential Revision: D13826741
fbshipit-source-id: 796d1a50d
Summary: The goal of this diff is to avoid using reporting (which as side-effects on the reportlog) during the checking pass, and only report everything at the end.
Reviewed By: skcho
Differential Revision: D13825520
fbshipit-source-id: ed2217c11
Summary:
The `oenv` is an option.
This diff ensures that it is `Some` during the analysis and `None` when it is stored in a summary.
It could have been resolved with another type, e.g. `unit`, but an option was needed to avoid duplicating code that is generic up to some point.
The price to pay is a parametric type.
Reviewed By: skcho
Differential Revision: D13825418
fbshipit-source-id: 71824609d
Summary:
In some rare cases, the CFG is broken, the analysis cannot reach the exit node and we won't update the summary for this procedure.
In this diff, the summary is gonna be updated with `Bottom` instead.
Reviewed By: skcho
Differential Revision: D13801731
fbshipit-source-id: 79d412429
Summary:
This diff extends the abstract domain to keep binary conditions on
prunings, so Inferbo can suppress more proof obligations (i.e., false
positives) that are known to be unreachable according to the binary
conditions.
Depends on D13729600
Reviewed By: mbouaziz
Differential Revision: D13749914
fbshipit-source-id: 314f048f1
Summary:
This will allow disjunctive analyzers to return sets of states as a
result instead of always returning one state. More precisely, this will
be needed for pulse when it becomes inter-procedural, if we take
summaries of functions to be disjunctive too (like, e.g., biabduction
does with several specs per function).
Reviewed By: mbouaziz
Differential Revision: D13537601
fbshipit-source-id: f54caf802
Summary:
Printing "N specs" next to function definitions in the HTML debug is
misleading because there are more checkers than just biabduction.
Reviewed By: mbouaziz
Differential Revision: D13572456
fbshipit-source-id: 209b874df
Summary:
`memcpy` should copy the contents of the source to the destination.
Depends on D13634754
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D13668414
fbshipit-source-id: cb0ff2010
Ezgi Çiçek
Nikos Gorogiannis
Dino Distefano
Katie Ots
Sungkeun Cho
Mehdi Bouaziz
Jeremy Dubreil
Daiva Naudziuniene
David Lively
Jules Villard