cfa33bd993
[clang] skip unknown `-fno-absolute-module-directory` flag
...
Reviewed By: ngorogiannis
Differential Revision: D13990619
fbshipit-source-id: 8afac8a96
6 years ago
d904ab76ec
[infer] remove the option --ignore-trivial-traces which is no longer used
...
Reviewed By: mbouaziz
Differential Revision: D13831343
fbshipit-source-id: 4c3efec36
6 years ago
adfd5a6418
[nullsafe] consistent models for the scrict containers
...
Reviewed By: mbouaziz
Differential Revision: D13977297
fbshipit-source-id: a32be3431
6 years ago
168e9099f7
[clang] upgrade to 7.0.1
...
Summary:
Just catching up.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz, martintrojer
Differential Revision: D13987271
fbshipit-source-id: 8f2c4c92a
6 years ago
d8846cf040
[inferbo] Parametric in Ondemand
...
Reviewed By: skcho
Differential Revision: D13852045
fbshipit-source-id: eacd6485c
6 years ago
137e070ece
[infer][PR] Move to base64.3.0.0
...
Summary:
Move codebase to `base64.3.0.0` which is more safe (see [CHANGELOG](https://github.com/mirage/ocaml-base64/releases/tag/v3.0.0 ).
Pull Request resolved: https://github.com/facebook/infer/pull/1056
Reviewed By: mbouaziz
Differential Revision: D13986683
Pulled By: jvillard
fbshipit-source-id: a89b8cf89
6 years ago
bd136ac24e
[inferbo] Prune string length at "if(fgets(s, ...))"
...
Summary:
If the result of `fgets` is not-null, the length of `s` should be
bigger than or equal to 1.
Reviewed By: mbouaziz
Differential Revision: D13939994
fbshipit-source-id: 298fe33f4
6 years ago
ea486c59d8
[purity] Always show PURE_FUNCTION issues
...
Reviewed By: mbouaziz
Differential Revision: D13973375
fbshipit-source-id: f23dab260
6 years ago
a0bae375db
[cfg] add option to print CFGs after the fact
...
Summary:
Add the `--source-files-cfg` option to emit CFGs as .dot files just as if one
had run with `--debug` to begin with. The usual `--source-files-filter`
applies. For example:
```
$ cd examples
$ infer -- clang -c hello.c
$ infer --continue -- javac Hello.java
$ infer --continue -- make -C c_hello
$ infer explore --source-files --source-files-cfg --source-files-filter ".*\.c$"
hello.c
c_hello/example.c
CFGs written in /home/jul/infer.fb/examples/infer-out/captured/*/icfg.dot
```
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D13973062
fbshipit-source-id: 3077e8b91
6 years ago
6e0682b463
[purity] Mark unmodeled functions as modifying global state
...
Reviewed By: mbouaziz
Differential Revision: D13941653
fbshipit-source-id: 02a15b29c
6 years ago
d08cabe7ed
[eradicate] match the different re-definitions of Preconditions.checkState
...
Reviewed By: mbouaziz
Differential Revision: D13966540
fbshipit-source-id: 3cdbb3fbc
6 years ago
50b1533921
[loop-invariance] Make InvariantModels based on ProcName
...
Reviewed By: mbouaziz
Differential Revision: D13971492
fbshipit-source-id: c47d6b858
6 years ago
c5890238f0
[Config] support arbitrary named symbol lists
...
Reviewed By: jvillard
Differential Revision: D13903005
fbshipit-source-id: b1cf9b4e5
6 years ago
9cce84ac6c
dont report biabduction NPE's on tmp variables
...
Reviewed By: da319
Differential Revision: D13800608
fbshipit-source-id: 2f54c8be6
6 years ago
caf61461ac
[inferbo] Update reachability conditions at function call
...
Summary:
This diff updates the reachability conditions of proof obligations at every function calls.
Depends on D13781124
Reviewed By: mbouaziz
Differential Revision: D13781147
fbshipit-source-id: 3c8768bd9
6 years ago
5a5f83a492
[inferbo] Add strcat model
...
Reviewed By: mbouaziz
Differential Revision: D13915381
fbshipit-source-id: e385130f3
6 years ago
f250ca7e06
[inferbo] Evaluation of abstract location of literal string
...
Summary:
It adds a semantics for evaluation of abstract location of literal
string, which was missing.
Reviewed By: mbouaziz
Differential Revision: D13915265
fbshipit-source-id: 741df843b
6 years ago
c72f381520
[purity] Refactor global writes and get rid of BottomLifting
...
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D13878260
fbshipit-source-id: bafd3cfbe
6 years ago
374538a02f
[crashcontext] die
...
Reviewed By: jeremydubreil, mbouaziz, jvillard
Differential Revision: D13861427
fbshipit-source-id: 85e340bb5
6 years ago
e6d2872a4e
Using record data structure for the cost domain
...
Reviewed By: mbouaziz
Differential Revision: D13897572
fbshipit-source-id: 4148b18b4
6 years ago
6621bc950a
[inferbo] Do not copy callee's parameter
...
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
6 years ago
1b8927badd
[inferbo/cost] Do not produce inferbo issues on Cost and Purity analysis
...
Reviewed By: skcho
Differential Revision: D13827167
fbshipit-source-id: 734950a1e
6 years ago
e4bb3c9d68
[inferbo] Only callee formals are needed
...
Reviewed By: skcho
Differential Revision: D13865391
fbshipit-source-id: bfe3b4d13
6 years ago
1765b66916
[eradicate] add model for com.google.common.base.Verify.verifyNotNull
...
Reviewed By: ezgicicek
Differential Revision: D13726750
fbshipit-source-id: 446ce1130
6 years ago
dc290555f1
[eradicate] fix conflict between null assertions methods with a var args and the modeled methods using string formatter
...
Reviewed By: mbouaziz
Differential Revision: D13633856
fbshipit-source-id: caae3631b
6 years ago
5ba8bbe08f
[inferbo] Split summary
...
Reviewed By: skcho
Differential Revision: D13853028
fbshipit-source-id: 77e81eb08
6 years ago
3fabbfdcad
[inferbo] Split Analysis and Checker
...
Reviewed By: skcho
Differential Revision: D13852741
fbshipit-source-id: f0da54257
6 years ago
0447c5b8d5
[inferbo] Give a widening threshold for array offset
...
Reviewed By: mbouaziz
Differential Revision: D13859243
fbshipit-source-id: 9a81505cc
6 years ago
7b7e6990e4
[inferbo] Add models for basic array iterator
...
Reviewed By: mbouaziz
Differential Revision: D13858898
fbshipit-source-id: 4518dad05
6 years ago
40ead0ac3d
[infer] remove the visibility field from the Infer JSON report
...
Reviewed By: mbouaziz
Differential Revision: D9689136
fbshipit-source-id: fabdb3ffc
6 years ago
764e9ee1be
[AI] empty is not (necessarily) bottom
...
Reviewed By: mbouaziz
Differential Revision: D13358254
fbshipit-source-id: 7f5d7e409
6 years ago
8a3592c34e
[inferbo] Uncouple numerical analysis and numerical checks
...
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
6 years ago
83dad3e1d4
[infer] set the default value for --ignore-trivial-traces to be false
...
Reviewed By: mbouaziz
Differential Revision: D13831335
fbshipit-source-id: 58a5ef188
6 years ago
9463b25702
[classloads] move sources to more appropriate location
...
Reviewed By: mbouaziz
Differential Revision: D13838506
fbshipit-source-id: 249806ad2
6 years ago
5e7fd7c326
[inferbo] Uncouple condition reporting and propagating
...
Reviewed By: skcho
Differential Revision: D13825862
fbshipit-source-id: 63ccce7ba
6 years ago
c3182b7032
[inferbo] Collect all issues before reporting
...
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
6 years ago
34ed67fea3
[inferbo] Stronger typing to ensure absence of on-demand env in summary
...
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
6 years ago
c6b222c757
[inferbo] Always update summary
...
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
6 years ago
2ee8ab2990
[class-loads] catch expressions
...
Reviewed By: ezgicicek
Differential Revision: D13832128
fbshipit-source-id: 1d3778763
6 years ago
7a4862b994
[inferbo] Revise std::array::at model
...
Reviewed By: mbouaziz
Differential Revision: D13814848
fbshipit-source-id: c03153927
6 years ago
b4a22a5bdd
[classloads] prune and multidimensional arrays
...
Reviewed By: ezgicicek
Differential Revision: D13818684
fbshipit-source-id: 8e5289f8f
6 years ago
3e55f8eb60
[classloads] class object expressions
...
Reviewed By: mbouaziz
Differential Revision: D13818059
fbshipit-source-id: 785d557e0
6 years ago
3f9eb37246
[classloads] casts and instanceof
...
Reviewed By: mbouaziz
Differential Revision: D13817582
fbshipit-source-id: c40be6bf8
6 years ago
c1a00b2358
[classloads] restrict loads via fields
...
Reviewed By: ezgicicek
Differential Revision: D13817232
fbshipit-source-id: 470d5ce11
6 years ago
a8c946f1d9
new predicate is_in_source_file and placeholders %source_file% and %kind%
...
Reviewed By: ddino
Differential Revision: D13745562
fbshipit-source-id: b3e646001
6 years ago
ca463d17c1
[inferbo] Add strcpy model
...
Reviewed By: mbouaziz
Differential Revision: D13800678
fbshipit-source-id: 7816ecc4b
6 years ago
371dc2060f
[inferbo] Add strndup model
...
Reviewed By: mbouaziz
Differential Revision: D13668557
fbshipit-source-id: e6d3d4161
6 years ago
f171d0496b
[classloads] array expressions
...
Reviewed By: mbouaziz
Differential Revision: D13786746
fbshipit-source-id: 9774da835
6 years ago
7fda4f1cc2
[inferbo] Revise strncpy model
...
Summary:
`strncpy` should update the `c_strlen` value.
Depends on D13668505
Reviewed By: mbouaziz
Differential Revision: D13668536
fbshipit-source-id: 64e09c734
6 years ago
11854ac037
[inferbo] Print reachability of proof obligation in debug mode
...
Reviewed By: mbouaziz
Differential Revision: D13781124
fbshipit-source-id: f6b1138db
6 years ago
Jules Villard
Jeremy Dubreil
Mehdi Bouaziz
Calascibetta Romain
Sungkeun Cho
Ezgi Çiçek
David Lively
Martin Trojer
Nikos Gorogiannis
Dino Distefano