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
9bb5738675
[inferbo] Add test for contents of std::array
...
Reviewed By: mbouaziz
Differential Revision: D13800142
fbshipit-source-id: c8a2be87b
6 years ago
6226722c22
[inferbo] Add a test of comparison operator as function
...
Reviewed By: mbouaziz
Differential Revision: D13798721
fbshipit-source-id: 85fb0e91c
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
1bcdc6e761
[inferbo] Extend conditional proof obligation for inequalities
...
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
6 years ago
3fc4ccbc14
[classloads] load super classes recursively
...
Reviewed By: mbouaziz
Differential Revision: D13771265
fbshipit-source-id: da600f912
6 years ago
bc6829344f
[inferbo] Change RiskyLibCall trace to non-final
...
Reviewed By: mbouaziz
Differential Revision: D13709906
fbshipit-source-id: 146ee0e08
6 years ago
0d07a240ea
[inferbo] Literal string on stack location
...
Summary:
It adds semantics of assignment of literal string to stack locations, e.g., `char s[] = "hello";`.
Depends on D13668414
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D13668505
fbshipit-source-id: 72caf35c3
6 years ago
49ca4eeecd
[HIL][disjunctive] allow underlying transfer function to return disjunctions
...
Summary:
This will allow disjunctive analyzers to return sets of states as a
result instead of always returning one state. More precisely, this will
be needed for pulse when it becomes inter-procedural, if we take
summaries of functions to be disjunctive too (like, e.g., biabduction
does with several specs per function).
Reviewed By: mbouaziz
Differential Revision: D13537601
fbshipit-source-id: f54caf802
6 years ago
4ac9fb8fd8
[html] stop printing number of (biabduction) specs
...
Summary:
Printing "N specs" next to function definitions in the HTML debug is
misleading because there are more checkers than just biabduction.
Reviewed By: mbouaziz
Differential Revision: D13572456
fbshipit-source-id: 209b874df
6 years ago
89e396571d
[classloads] treat loads and stores wrt to field derefs
...
Reviewed By: mbouaziz
Differential Revision: D13761363
fbshipit-source-id: bcaddd13b
6 years ago
d390a6f08a
[CType_decl] Add missing case to `get_record_typename`
...
Reviewed By: ddino
Differential Revision: D13736334
fbshipit-source-id: c088d1aa8
6 years ago
5686d67072
[classloads] fix treatment of static initializers
...
Reviewed By: jvillard
Differential Revision: D13751141
fbshipit-source-id: f64af292b
6 years ago
00df708f98
[classloads] record at most one load for each class
...
Reviewed By: ezgicicek
Differential Revision: D13750609
fbshipit-source-id: cd55a3370
6 years ago
6e04a9469b
[inferbo] Revise memcpy model
...
Summary:
`memcpy` should copy the contents of the source to the destination.
Depends on D13634754
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D13668414
fbshipit-source-id: cb0ff2010
6 years ago
09a5671ef4
[inferbo] Add a test for conditional inequality
...
Reviewed By: mbouaziz
Differential Revision: D13729600
fbshipit-source-id: d460093e1
6 years ago
39b11619b8
[classloads] overhaul test infra & fix treatment of self-class loading in method calls
...
Reviewed By: ddino
Differential Revision: D13622717
fbshipit-source-id: 233cc5d74
6 years ago
13e8c21bef
[lab] fix issues discovered during POPL tutorial
...
Summary: .
Reviewed By: ngorogiannis
Differential Revision: D13750261
fbshipit-source-id: 4ec935b99
6 years ago
9bd1191669
[inferbo] Add fgets model
...
Summary: It adds the fgets model.
Reviewed By: mbouaziz
Differential Revision: D13634754
fbshipit-source-id: 147745483
6 years ago
58cdefc118
[inferbo] Add strlen model
...
Summary: It extends the abstract location for C string length, i.e., the first index of the null character in character array.
Reviewed By: mbouaziz
Differential Revision: D13634241
fbshipit-source-id: d2727d5f5
6 years ago
5aa26dc32e
[inferbo] Add an allocsite type for literal strings
...
Reviewed By: mbouaziz
Differential Revision: D13689870
fbshipit-source-id: 658884b9c
6 years ago
f4b4f68e6f
[inferbo] Move decl_local to BufferOverrunUtils
...
Reviewed By: mbouaziz
Differential Revision: D13690953
fbshipit-source-id: 85cd11b2f
6 years ago
87a8ddc8fa
[nullsafe] merge the option names
...
Reviewed By: mbouaziz
Differential Revision: D13682855
fbshipit-source-id: 28c990725
6 years ago
910def4262
[nullsafe] rename the method for unsafe access to lists and maps
...
Reviewed By: ezgicicek
Differential Revision: D13668339
fbshipit-source-id: 3b07fff32
6 years ago
148c269b0d
[infer] make the visibility field optional
...
Reviewed By: mbouaziz
Differential Revision: D13643462
fbshipit-source-id: b13f08698
6 years ago
339911bb75
[labs] more instructions
...
Summary: .
Reviewed By: mbouaziz
Differential Revision: D13651081
fbshipit-source-id: aab5356f2
6 years ago
8e4fea7693
[labs] fiddling
...
Summary: Changing the text a bit.
Reviewed By: mbouaziz
Differential Revision: D13650583
fbshipit-source-id: a1ff99124
6 years ago
57451e65a2
[labs] fix Docker command
...
Reviewed By: mbouaziz
Differential Revision: D13650264
fbshipit-source-id: 52cfa1ea0
6 years ago
Mehdi Bouaziz
Sungkeun Cho
Jeremy Dubreil
Nikos Gorogiannis
David Lively
Jules Villard