Summary: Sometimes reports need traces to be fully understood, but sometimes reporting where the exception takes place can save time to developers.
Reviewed By: jvillard
Differential Revision: D4914037
fbshipit-source-id: 039ab63
Summary:
There are 2 possible places where to find toplevel.cmo:
- infer/_build/infer/toplevel.cmo, built by `make toplevel`
- infer/_build/test/infer/toplevel.cmo, built by `make test`
The test loading and running toplevel.cmo would give priority to the non-test
version of toplevel.cmo, which might be stale because `make test` doesn't
rebuild it.
This diff makes sure we use the test version of toplevel.cmo in `make test`.
Reviewed By: akotulski
Differential Revision: D4960550
fbshipit-source-id: 9c817ba
Summary: The purpose of the annotation reachability analysis is to report when a method annotated with `X` never calls, directly or indirectly, another method annotated with `Y`. However, there can be different call stacks following different execution paths from `X` to `Y`. Reporting more than one call stack ending with the same annotated procedure does not bring more signal to the end user. So the purpose of this diff is to avoid those duplicated reports and report at most one annotation reachability issue per end of call stack.
Reviewed By: sblackshear
Differential Revision: D4942765
fbshipit-source-id: 46325a7
Summary: The analysis logic was split between the treatment of the instructions and the definition of the domain, making the code more complicated that it should. This diff moves more of the logic into the domain definition and change to variable names to more descriptive ones
Reviewed By: sblackshear
Differential Revision: D4936414
fbshipit-source-id: ff59de7
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
Summary: This will be needed to generate man pages with an accurate date.
Reviewed By: jberdine, mbouaziz
Differential Revision: D4937498
fbshipit-source-id: b5ebd31
Summary:
Went through the trouble of killing these warnings, make sure they do not creep
up again in the future.
Reviewed By: mbouaziz
Differential Revision: D4937493
fbshipit-source-id: 0e2eda4
Summary:
We won't be needing to know the terminal size when we move the help to
manpages. Hopefully if we need C stubs again in the future we can refer back to
this diff to revive them.
Reviewed By: jberdine
Differential Revision: D4937491
fbshipit-source-id: 99139fa
Summary: This is necessary to create a `report` subcommand (see later diffs).
Reviewed By: jberdine, dulmarod
Differential Revision: D4937488
fbshipit-source-id: 3fec0b5
Summary:
As an interprocedural checker, SIOF should not run unless explicitly required.
Make it a new type of analyzer like other similar checkers.
Reviewed By: mbouaziz
Differential Revision: D4937820
fbshipit-source-id: a9e2d38
Summary: This makes the build less likely to break because of package upgrades in opam.
Reviewed By: mbouaziz
Differential Revision: D4937908
fbshipit-source-id: 5ce9ec7
Summary: There was unncecessary abstraction here - instead of looking up sil type in the map, simply store it as part of variant payload
Reviewed By: jberdine
Differential Revision: D4938114
fbshipit-source-id: 9fb8dd4
Summary: `bufferoverrun` is not part of `checkers` yet so bufferoverrun tests require their own Makefile
Reviewed By: jvillard
Differential Revision: D4937558
fbshipit-source-id: 20380f1
Summary:
Whenever running CTL in debug mode, you can now stop the execution and attach a step-by-step debugger by placing a breakpoint in the source code.
A breakpoint is the comment containing `INFER_BREAKPOINT`, placed on the line of interest.
You can attach the debugger to your breakpoint by running Infer with the following command
```
infer --linters-def-file my_linter.al --linters-developer-mode -- clang -c file.m
```
Reviewed By: dulmarod
Differential Revision: D4843358
fbshipit-source-id: acebde4
Summary: Handling special case of DeclStmt with VarDecl: emit the VarDecl node then emit the statements in DeclStmt as children of VarDecl. This is because despite being equal, the statements inside VarDecl and those inside DeclStmt belong to different instances, hence they fail the phys_equal check that should colour them
Reviewed By: dulmarod
Differential Revision: D4850681
fbshipit-source-id: b9683dc
Summary:
This cuts the resulting image from ~4.6GB to ~1.6GB.
Infer functionality is not sacrificed and the following commands run successfully without any extra user interaction (including Android example provided the user has accepted the Android SDK license which they'll be prompted to do when running the Docker image, see https://github.com/facebook/infer/pull/597#issuecomment-284864016):
```bash
cd /infer/examples && infer -- javac Hello.java
cd /infer/examples && infer -- gcc -c hello.c
cd /infer/examples && infer -- clang -c hello.c
cd /infer/examples/c_hello && infer -- make
cd /infer/examples/java_hello && infer -- javac Hello.java Pointers.java Resources.java
cd /infer/examples/android_hello && infer -- ./gradlew build
```
The OPAM installation is no longer retained. This may impact Infer developers if they're using the Docker images and require OPAM packages to be installed as part of their workflow.
Closes https://github.com/facebook/infer/pull/597
Differential Revision: D4906386
Pulled By: jvillard
fbshipit-source-id: 6bc09d2
Summary:
We lost InferClang++ a long time ago... It was installed properly on `make
install` but not during normal compilation!
Reviewed By: akotulski
Differential Revision: D4905947
fbshipit-source-id: 56375c2
Summary:
The error was complaining about a missing `etree` package but that's actually
part of the `lxml` package and that wasn't clear from the output.
See for instance https://github.com/facebook/infer/issues/635
Reviewed By: martinoluca
Differential Revision: D4905953
fbshipit-source-id: 28b26af
Summary: Sawja assigns them on multiple control-flow paths, so they're not SSA.
Reviewed By: peterogithub
Differential Revision: D4896745
fbshipit-source-id: c805216
Summary:
There are false positives in the current analysis due to the
use of conjunction in the treatment of threaded. Changing conjunction to disjunction
removes these false positives. Some new false negatives arise, but all the old tests pass.
This is a stopgap towards a better solution being planned.
Reviewed By: sblackshear
Differential Revision: D4883280
fbshipit-source-id: c2a7e6e
Summary:
These were showing up as allocation huge amounts of memory on some analysis
profiles from OpenSSL using Spacetime. Doesn't hurt to make them allocate less.
Reviewed By: jeremydubreil
Differential Revision: D4884520
fbshipit-source-id: e79b815
Martino Luca
Jules Villard
Jeremy Dubreil
Sam Blackshear
Andrzej Kotulski
Dulma Churchill
Sungkeun Cho
Mehdi Bouaziz
Kihong Heo
Adil Aliyev
Matthew Haughton
Peter O'Hearn
Josh Berdine