8ef9bf7641
Expose WTO in ProcCfg
...
Reviewed By: jberdine
Differential Revision: D10376596
fbshipit-source-id: 0162a5cf3
6 years ago
b324dbd8dd
Use WTO to get loop heads
...
Reviewed By: jberdine
Differential Revision: D10376587
fbshipit-source-id: 7f808832a
6 years ago
0d4c06efc5
WTO: use a partial ProcCfg
...
Reviewed By: jberdine
Differential Revision: D10376574
fbshipit-source-id: 09e0f0ca5
6 years ago
dd2b9675d6
[log] print only innermost source file context of crash
...
Summary:
When the backend crashes we print which instruction/file/... we were analysing,
but because of recursion we can end up repeating that information all
the way to the toplevel call.
This makes sure we only print the innermost one, we don't care about the
calling context because the analysis is compositional.
Reviewed By: mbouaziz
Differential Revision: D10381141
fbshipit-source-id: 1c92bb861
6 years ago
bee7649048
[perf] fix capture traces and record clang events
...
Summary:
Trace events would crash when infer subprocesses were spawned by the build
system because they didn't detect if the file was already initialised
correctly.
Also trace the clang capture.
Reviewed By: mbouaziz
Differential Revision: D10380745
fbshipit-source-id: 76e1d4d7e
6 years ago
fd660f42f5
[inferbo] Suppress exception on placement new
...
Summary:
It avoids raising an exception when unexpected arguments are given to
placement new. We will revert this after fixing the frontend to parse
user defined `new` correctly in the future.
Reviewed By: mbouaziz
Differential Revision: D10378136
fbshipit-source-id: d494f781b
6 years ago
2e64566a6c
Finding stateless CKComponents
...
Reviewed By: jberdine
Differential Revision: D10161169
fbshipit-source-id: dd82e48ee
6 years ago
371e1267d9
[debug] Get rid of proof_cover/isproof
...
Reviewed By: jberdine
Differential Revision: D10376563
fbshipit-source-id: 783c4a78e
6 years ago
b71af05f00
Stats: merge visited_fp and visited_re
...
Reviewed By: da319
Differential Revision: D10376556
fbshipit-source-id: a0db1485a
6 years ago
f873debc96
[inferbo] Debug latest prune abstract value
...
Reviewed By: skcho
Differential Revision: D10376611
fbshipit-source-id: dc891fe81
6 years ago
78a865b14e
[hosting] Disable purity and cost callbacks temporarily
...
Reviewed By: mbouaziz
Differential Revision: D10356668
fbshipit-source-id: a04c329c9
6 years ago
99c2a6da8d
[hoisting] Hoist only expensive pure functions
...
Reviewed By: mbouaziz
Differential Revision: D10236706
fbshipit-source-id: c51a9ff0c
6 years ago
e71ea9f0ed
[sledge] Switch from Llvm.demangle to __cxa_demangle via Ctypes
...
Summary:
Call __cxa_demangle from libstdc++ using Ctypes instead of the
wrapper in Llvm.
Reviewed By: mbouaziz
Differential Revision: D9939682
fbshipit-source-id: a9f02fff5
6 years ago
27f08ab53a
[sledge] Update entry point and command line interface
...
Reviewed By: mbouaziz
Differential Revision: D9846737
fbshipit-source-id: 016add93d
6 years ago
b712a57bf9
[sledge] Add analysis based on iterative bounded exploration
...
Reviewed By: mbouaziz
Differential Revision: D9846736
fbshipit-source-id: 3c3a687b3
6 years ago
0a09581431
[sledge] Add abstract domain interface
...
Reviewed By: mbouaziz
Differential Revision: D9846739
fbshipit-source-id: 56b4d63de
6 years ago
4633419b1c
[sledge] Add symbolic execution
...
Reviewed By: jvillard
Differential Revision: D9846734
fbshipit-source-id: cf3f36f93
6 years ago
e397a43f80
[sledge] Add frame inference solver over symbolic heaps
...
Reviewed By: jvillard
Differential Revision: D9846747
fbshipit-source-id: 5b3bea318
6 years ago
83eff4c734
[sledge] Add symbolic heap formulas
...
Reviewed By: ngorogiannis
Differential Revision: D9846733
fbshipit-source-id: 8772f77b9
6 years ago
a32890a1e3
[sledge] Add congruence closure with integer offsets
...
Reviewed By: mbouaziz
Differential Revision: D9846748
fbshipit-source-id: 575c6ee15
6 years ago
f7a9a0c323
[sledge] Update frontend
...
Reviewed By: jvillard
Differential Revision: D9846735
fbshipit-source-id: 1a2293a47
6 years ago
2c116474e5
[sledge] Update llair
...
Reviewed By: jvillard
Differential Revision: D9846740
fbshipit-source-id: 16d039b04
6 years ago
8e7eeb8d1f
[sledge] Update global
...
Reviewed By: mbouaziz
Differential Revision: D9846746
fbshipit-source-id: f5c465dd5
6 years ago
2b53e53504
[sledge] Update loc
...
Reviewed By: mbouaziz
Differential Revision: D9846744
fbshipit-source-id: b72291e5b
6 years ago
392f596b02
[sledge] Update exp
...
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D9846743
fbshipit-source-id: c293970c7
6 years ago
742b181282
[sledge] Update typ
...
Reviewed By: mbouaziz
Differential Revision: D9846741
fbshipit-source-id: 1c2876954
6 years ago
6a7c21e7c9
[sledge] Update trace and ppx_trace
...
Reviewed By: mbouaziz
Differential Revision: D9846738
fbshipit-source-id: 14adee4c4
6 years ago
91888c4c41
[sledge] Update import, vector
...
Reviewed By: mbouaziz
Differential Revision: D9934559
fbshipit-source-id: a446f386c
6 years ago
f6ba0c8137
[sledge] Update build system, etc.
...
Reviewed By: jvillard
Differential Revision: D9850346
fbshipit-source-id: 16fa35ae2
6 years ago
e1d4aad487
[ocamlformat] upgrade ocamlformat to 0.8
...
Reviewed By: mbouaziz
Differential Revision: D10359577
fbshipit-source-id: e7f5286e3
6 years ago
9eecd1bb9b
[racerd] reconcile java and clang report corellation code
...
Summary:
Use same code for deciding whether two accesses conflict across java/clang, by adapting that of the clang version.
Eliminate/simplify some code.
Reviewed By: mbouaziz, jberdine
Differential Revision: D10217383
fbshipit-source-id: dc0986d05
6 years ago
08a26d4ba1
First approximation of stateless
...
Reviewed By: jvillard
Differential Revision: D10141376
fbshipit-source-id: a1dbb4c21
6 years ago
c3f2fbc8c6
[inferbo] Do not alias values representing multiple values (Java, C partially)
...
Reviewed By: skcho
Differential Revision: D10317894
fbshipit-source-id: d9bf25699
6 years ago
d94ba863c6
[infer] Add type in binary operator
...
Reviewed By: mbouaziz
Differential Revision: D10216263
fbshipit-source-id: 84f0fa936
6 years ago
eca0b491d6
Weak Topological Order and Abstract Interpreter using it
...
Reviewed By: jberdine
Differential Revision: D7783487
fbshipit-source-id: 15b4c84e1
6 years ago
c9b89b54dd
Preparing for WeakTopologicalOrder-based abstract interpreter
...
Reviewed By: ngorogiannis
Differential Revision: D10069200
fbshipit-source-id: 5d6d5d12c
6 years ago
2be4710811
[AI] Enable debugging only based on --write-html
...
Reviewed By: ezgicicek
Differential Revision: D10238681
fbshipit-source-id: 08eeedd26
6 years ago
62b1f39540
[Uninit][8/13] Rename UninitVars to MaybeUninitVars
...
Reviewed By: jeremydubreil
Differential Revision: D10250193
fbshipit-source-id: bd4cd332f
6 years ago
5679105c15
[Uninit][7/13] Add new tests
...
Reviewed By: jeremydubreil
Differential Revision: D10250168
fbshipit-source-id: 5e5983f04
6 years ago
01f3f39760
[Uninit][6/13] Move some operations to the domain
...
Reviewed By: jeremydubreil
Differential Revision: D10250152
fbshipit-source-id: 332a83565
6 years ago
6ca6de80c3
[Uninit][5/13] Use callee_formals directly
...
Reviewed By: jeremydubreil
Differential Revision: D10250131
fbshipit-source-id: 528d1ee4b
6 years ago
fcf2ce1e8f
[Uninit][4/13] extras
...
Reviewed By: jeremydubreil
Differential Revision: D10250076
fbshipit-source-id: d1e412bcf
6 years ago
6fd02b272f
[Uninit][3/13] Modules Models and Initial
...
Reviewed By: jeremydubreil
Differential Revision: D10250064
fbshipit-source-id: 248d96e73
6 years ago
89700a7d95
Added new predicated for captured values
...
Reviewed By: jvillard
Differential Revision: D10162271
fbshipit-source-id: 47f9420b8
6 years ago
f639906496
[Uninit][2/13] Move summary type
...
Reviewed By: jeremydubreil
Differential Revision: D10250040
fbshipit-source-id: 12e02cb32
6 years ago
8cac7df447
[Uninit][1/13] Move interproc tests
...
Reviewed By: jeremydubreil
Differential Revision: D10250022
fbshipit-source-id: d82863d5a
6 years ago
b90c2f3bfc
[debug] Print proc attributes on the procedure page
...
Reviewed By: jeremydubreil
Differential Revision: D10238661
fbshipit-source-id: 2de9ee425
6 years ago
15839539a7
Annot.Method: record rather than pair
...
Reviewed By: ngorogiannis
Differential Revision: D10238615
fbshipit-source-id: 7f7785275
6 years ago
0b4beda1cd
[starvation] also consider subclasses of Future
...
Reviewed By: jberdine
Differential Revision: D10192090
fbshipit-source-id: 94384a4a5
6 years ago
1330475032
[infer] Fix placement_new translation
...
Summary:
It unsets `var_exp_typ` of `trans_state` during the translations of
placement parameters, so they are translated independently against the
target variable and class of the `new` function.
Reviewed By: mbouaziz, jvillard
Differential Revision: D10161419
fbshipit-source-id: 7f588a91c
6 years ago
Mehdi Bouaziz
Jules Villard
Sungkeun Cho
Dino Distefano
Ezgi Çiçek
Josh Berdine
Nikos Gorogiannis