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:
For abstract values representing one concrete value, create only one symbol instead of two.
Still create two symbols (lb, ub) for abstract values representing multiple concrete values (like array cells).
As a consequence, comparisons of symbolic values are more precise (we can even prove equality). I expect to remove a bunch of FPs.
Another consequence is the disappearance of `.lb` and `.ub` in many reports.
Reviewed By: skcho
Differential Revision: D13072084
fbshipit-source-id: 9bc0b9881
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
Summary:
- Bottom-lift abstract memory domain to express unreachable node
- Two cases to make a node unreachable
+ constant: when an evaluation result of condition expression is
bottom or false, e.g., "prune(0)".
+ alias: when the same structure e is compared to itself with "<",
">", and "!=", e.g., "prune(e < e)".
- Add test for the new prune (prune_constant.c, prune_alias.c)
- Debug the semantics of comparison
Reviewed By: mbouaziz
Differential Revision: D4938055
fbshipit-source-id: d0fadf0
Sungkeun Cho
Mehdi Bouaziz
Jules Villard