Summary:
There are two changes:
1/ Fix incorrect merge of two cases (empty and not-empty)
```
let<*> astate_equal_zero = ... in
let<*> astate_not_zero = ... in
[Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)]
```
This was an incorrect merge, because if there is an error in the former
case `astate_equal_zero`, it doesn't even evaluate the latter case
`astate_not_zero`.
2/ Cover all cases precisely. There are actually three cases to cover:
* `TextUtils.is_empty(null) = true`
* `TextUtils.is_empty("") = true`
* `TextUtils.is_empty("abc") = false`
However, in the previous model, it missed the second case.
Reviewed By: jvillard
Differential Revision: D29393579
fbshipit-source-id: e59d9a60d
Summary:
This diff adds some semantic models for C++ string length. It introduces
an virtual field for string length and use the value in the models.
* basic_string constructor given a constant string
* string.empty
* string.length
Reviewed By: jvillard
Differential Revision: D29390815
fbshipit-source-id: 99d67e48e
Summary:
Unknown functions may create false positives as well as false negatives
for Pulse. Let's consider that unknown functions behave "functionally",
or at least that a functional behaviour is a possible behaviour for
them: when called with the same parameter values, they should return the
same value.
This is implemented purely in the arithmetic domain by recording
`v_return = f_unknown(v1, v2, ..., vN)` for each call to unknown
functions `f_unknown` with values `v1`, `v2`, ..., `vN` (and return
`v_return`). The hope is that this will create more false negatives than
false positives, as several FPs have been observed on real code that
would be suppressed with this heuristic.
The other effect this has on reports is to record hypotheses made on the
return values of unknown functions into the "pruned" part of formulas,
which inhibits reporting on paths whose feasibility depends on the
return value of unknown functions (by making these issues latent
instead). This should allow us to control the amount of FPs until we
model more functions.
Reviewed By: skcho
Differential Revision: D27798275
fbshipit-source-id: d31cfb8b6
Summary:
Turns out the mistake was pretty simple: we just forgot to keep the
history of the return value in the callee and add it to the caller's.
Reviewed By: skcho
Differential Revision: D28385941
fbshipit-source-id: 40fe09c99
Summary:
- Changed "passed as argument to f" to "in call to f", as these do not
always correspond to passing an argument (eg could be a value returned
from f)
- Changed "assigned" to "returned" when appropriate
- Changed the model of malloc() to not say "allocated" in the null case
- Don't print "returned from f" when there was no event inside f: just
print "in call to f".
Reviewed By: da319
Differential Revision: D28413900
fbshipit-source-id: bc85625e3
Summary:
The order was reversed when printing the trace, leading to confusion.
Also make sure we indicate which part of the trace we are printing when
there is more than one part (either context + access or invalidation +
access, or all three).
Also start nesting at <calling context length> to better represent the
role of the calling context visually.
Reviewed By: da319
Differential Revision: D28329263
fbshipit-source-id: b691fb1f4
Summary:
There's been regressions in --pulse-isl. Without tests, everything is
temporary!
Note: the regressions are presumably still there, this just records the
current status of pulse.isl.
Also, no objective-C(++) at the moment. Should we add them too? (in
another diff)
Reviewed By: skcho
Differential Revision: D28256703
fbshipit-source-id: 700b2cc57
Sungkeun Cho
Daiva Naudziuniene
Loc Le
Jules Villard