Summary: This will facilitate accessing Inferbo abstract state at the instruction level from the Cost analysis
Reviewed By: ddino
Differential Revision: D7568701
fbshipit-source-id: 84ac648
Summary:
Got rid of `Itv.equal` which was ambiguous and use an abstract boolean type for abstract comparison results
Depends on D7568573
Reviewed By: jvillard
Differential Revision: D7568583
fbshipit-source-id: 0e897e9
Summary:
Convenience function for `prune_eq` with zero (needed for stacked diffs).
Renamed `prune_zero` to `prune_ne_zero` to avoid ambiguity.
Reviewed By: jvillard
Differential Revision: D7568556
fbshipit-source-id: b95ab6d
Summary: Only RacerD uses the Cluster callbacks but we used to compute a lot of things anyway.
Reviewed By: sblackshear
Differential Revision: D7516279
fbshipit-source-id: 22f2b86
Summary:
This information is already available in the trace, and can contain absolute
paths to system includes (or infer's own clang runtime), which confuses the
diff analysis.
Reviewed By: mbouaziz
Differential Revision: D7534609
fbshipit-source-id: 5bd8f8b
Summary:
This can be noticed when the format of the DB changes, and other fun things
like that. No longer require to `make clean` to be able to pass these tests.
Reviewed By: mbouaziz
Differential Revision: D7533559
fbshipit-source-id: 670cb60
Summary:
It renames `eval_locs` to `eval_arr` and we use it for getting array block values the given input expressions are pointing to. For example, when given a program variable `x` as an input, `eval_arr` returns array blocks that `x` is pointing to, on the other hand, `eval` returns an abstract location of `x`.
Depends on D7471891
Reviewed By: mbouaziz
Differential Revision: D7471915
fbshipit-source-id: b994944
Summary: In the pointer arithmetics, it returns top, if we cannot precisely follow the physical memory model, e.g., (&x + 1).
Reviewed By: mbouaziz
Differential Revision: D7453510
fbshipit-source-id: db8738e
Summary:
It feels risky to me to swallow the `Sys_error` here since this could hide deeper issues with the deserialization of summaries.
This is only used with the Buck Integration for Java when extracting the summaries from the jar files.
Reviewed By: sblackshear
Differential Revision: D7490123
fbshipit-source-id: 68cd556
Summary:
This is unused, but the logic for keeping its value up to date was still alive
and kicking.
I don't know that making use of this flag would be easy: we could just use it
in `Ondemand.should_analyze`, but it would be unsound because a procedure might
need to be re-analysed becauese its dependencies have changed. Since there's
not code to deal with that currently I think it's best to remove it and
re-introduce it when we have some idea how to use it.
Reviewed By: sblackshear, jeremydubreil
Differential Revision: D7444179
fbshipit-source-id: 99a1ec5
Summary:
Report nullable inconsistencies by relying on the bytecode, and not on the presence of analysis summary on disk.
This use the `--external-java-packages` to avoid reporting inconsistencies outside of the codebase.
Reviewed By: sblackshear
Differential Revision: D7481101
fbshipit-source-id: 281135d
Summary:
Utility function that's basically `Logging.progress` but with a more obvious
name for debugging.
The `[@deprecated ...]` ensures no uses gets landed, and the `[@warning "-32"]` ensures that it's not a compile error that there are no uses of this function.
Inspired by #716.
Reviewed By: mbouaziz
Differential Revision: D7443224
fbshipit-source-id: e94798f
Summary:
Without it `make` will not rebuild infer when "infer/src/infer.ml" changes
(since D7381842 moved it out of backend/).
Reviewed By: mbouaziz
Differential Revision: D7443275
fbshipit-source-id: 33ea10b
Tony Hu
Mehdi Bouaziz
Jules Villard
Dulma Churchill
Jeremy Dubreil
Dino Distefano
Sam Blackshear
Sungkeun Cho
Daiva Naudziuniene
Nikos Gorogiannis