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
16c0c03050
resource leaks tutorial
...
Summary: Publish solutions to the lab, and a Docker file and image to get started more quickly with infer hacking.
Reviewed By: mbouaziz
Differential Revision: D13648847
fbshipit-source-id: daf48ad03
6 years ago
9e91c9298b
[racerd] remove redundant ownership constructor/state
...
Reviewed By: jeremydubreil
Differential Revision: D13489018
fbshipit-source-id: b94c50664
6 years ago
e2bb049a5e
[racerd] fix bug in ownership transitivity 2
...
Reviewed By: ezgicicek
Differential Revision: D13488195
fbshipit-source-id: 3feed4322
6 years ago
db441ffc8a
[inferbo] Prevent deduplication of issues when different conditions
...
Summary:
This diff prevents deduplications of issues when they have different
conditions to reach.
Reviewed By: mbouaziz
Differential Revision: D13596220
fbshipit-source-id: 95f802edb
6 years ago
7bbb7fc869
[clang][objcpp] register exported methods and treat them as private in RacerD
...
Summary:
In ObjC there are no access modifiers. The strongest alternative is to put methods in the implementation but omit them from the interface declaration.
Put exported ObjC methods in their own field in the class structure and use that in RacerD to decide whether to report on the method.
Reviewed By: mbouaziz
Differential Revision: D13597504
fbshipit-source-id: c4a3d2705
6 years ago
98cd2e59da
[inferbo] Add tests: values representing multiple values
...
Reviewed By: mbouaziz
Differential Revision: D13606721
fbshipit-source-id: 594d24d4a
6 years ago
10f4ad06ba
[inferbo] Add traces on cast
...
Reviewed By: mbouaziz
Differential Revision: D13606790
fbshipit-source-id: a3d6d0c5c
6 years ago
2cf4905c74
bump version: 0.15.0 -> 0.16.0
...
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D13608804
fbshipit-source-id: b4b432979
6 years ago
405dee5ceb
[inferbo] Consider `this` to never be a pointer inside an array
...
Reviewed By: skcho
Differential Revision: D13128691
fbshipit-source-id: e74a168ba
6 years ago
f7deed7593
[cost] Add examples that we can't handle currently
...
Reviewed By: mbouaziz, jvillard
Differential Revision: D13596579
fbshipit-source-id: 7460d430d
6 years ago
05ec029e50
[inferbo] Suppress intended integer overflow
...
Summary:
It suppresses intended integer overflows that generate hash values or random numbers. For judging that the intention of integer overflow, it applies a heuristics: checking if traces of issues include a whitelisted words, e.g., "rand" or "seed".
While we would be able to suppress all integer overflows of unsigned integers since they have defined behaviors, we don't want to miss unintended integer overflows, e.g., that on unsigned index value.
Depends on D13595958
Reviewed By: mbouaziz
Differential Revision: D13595967
fbshipit-source-id: 8d3aca5a7
6 years ago
d6494f725b
[inferbo] Prepare supressing intended integer overflow
...
Reviewed By: mbouaziz
Differential Revision: D13595958
fbshipit-source-id: 39aef1d1b
6 years ago
499e6398b1
[CK][Linter Rule] Add CKRenderLayoutWithChildren component to Component Kit Conventional Superclass
...
Reviewed By: kfirapps, ddino
Differential Revision: D13590184
fbshipit-source-id: d4394839e
6 years ago
28c3ed50de
[CK][Linter Rule] Add CKRenderLayout component to Component Kit Conventional Superclass
...
Reviewed By: kfirapps, ddino
Differential Revision: D13590155
fbshipit-source-id: 1a9f4ba15
6 years ago
322066d248
Rename {has_,}cxx_full_name to {has_,}cxx_fully_qualified_name.
...
Reviewed By: jvillard
Differential Revision: D13597510
fbshipit-source-id: 4b48d6444
6 years ago
d5faf2de52
[inferbo] Ignore encoding error in the snprintf model
...
Reviewed By: mbouaziz
Differential Revision: D13588979
fbshipit-source-id: 4cd9de71d
6 years ago
be4c5aaa0f
[infer] ignore the visibility field when creating the HTML reports
...
Reviewed By: mbouaziz
Differential Revision: D13586918
fbshipit-source-id: 35f459780
6 years ago
05ceaebb7d
[inferbo] Add model of String::operator==
...
Reviewed By: jvillard
Differential Revision: D13552213
fbshipit-source-id: a74460e87
6 years ago
5c1b862bbd
[infer] Fix test script (build_utf8_in_pwd_test)
...
Reviewed By: mbouaziz
Differential Revision: D13571885
fbshipit-source-id: b499eb22b
6 years ago
7f70251eff
[infer] Fix filename to relative
...
Reviewed By: jvillard
Differential Revision: D13552198
fbshipit-source-id: b9be4dd2e
6 years ago
0e5a902ac6
[inferbo] Add model of String::length
...
Reviewed By: mbouaziz
Differential Revision: D13547914
fbshipit-source-id: 7d496d11a
6 years ago
7ba4386199
[logging] Simplified and faster debug
...
Reviewed By: jberdine
Differential Revision: D13544862
fbshipit-source-id: d2d25eada
6 years ago
a726c34940
Logging: Fix delayed prints
...
Reviewed By: jvillard
Differential Revision: D13572280
fbshipit-source-id: 032a98873
6 years ago
5df11674dc
Io_infer.with_color
...
Reviewed By: jvillard
Differential Revision: D13572262
fbshipit-source-id: eb40fa96b
6 years ago
1fa459967b
Prune_node_kind: sum type rather than string
...
Reviewed By: jvillard
Differential Revision: D13572273
fbshipit-source-id: 17b0c1637
6 years ago
Sungkeun Cho
Nikos Gorogiannis
Jules Villard
David Lively
Jeremy Dubreil
Mehdi Bouaziz
Ezgi Çiçek
Fabio Milano