Josh Berdine
a9cdf69010
[sledge] Use dune ocamlformat integration for `make fmt`
...
Summary: Dune now includes support for ocamlformat, so use it to format in parallel.
Reviewed By: mbouaziz
Differential Revision: D10389485
fbshipit-source-id: cb1dfbe38
6 years ago
Josh Berdine
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
Josh Berdine
27f08ab53a
[sledge] Update entry point and command line interface
...
Reviewed By: mbouaziz
Differential Revision: D9846737
fbshipit-source-id: 016add93d
6 years ago
Josh Berdine
b712a57bf9
[sledge] Add analysis based on iterative bounded exploration
...
Reviewed By: mbouaziz
Differential Revision: D9846736
fbshipit-source-id: 3c3a687b3
6 years ago
Josh Berdine
0a09581431
[sledge] Add abstract domain interface
...
Reviewed By: mbouaziz
Differential Revision: D9846739
fbshipit-source-id: 56b4d63de
6 years ago
Josh Berdine
4633419b1c
[sledge] Add symbolic execution
...
Reviewed By: jvillard
Differential Revision: D9846734
fbshipit-source-id: cf3f36f93
6 years ago
Josh Berdine
e397a43f80
[sledge] Add frame inference solver over symbolic heaps
...
Reviewed By: jvillard
Differential Revision: D9846747
fbshipit-source-id: 5b3bea318
6 years ago
Josh Berdine
83eff4c734
[sledge] Add symbolic heap formulas
...
Reviewed By: ngorogiannis
Differential Revision: D9846733
fbshipit-source-id: 8772f77b9
6 years ago
Josh Berdine
a32890a1e3
[sledge] Add congruence closure with integer offsets
...
Reviewed By: mbouaziz
Differential Revision: D9846748
fbshipit-source-id: 575c6ee15
6 years ago
Josh Berdine
f7a9a0c323
[sledge] Update frontend
...
Reviewed By: jvillard
Differential Revision: D9846735
fbshipit-source-id: 1a2293a47
6 years ago
Josh Berdine
2c116474e5
[sledge] Update llair
...
Reviewed By: jvillard
Differential Revision: D9846740
fbshipit-source-id: 16d039b04
6 years ago
Josh Berdine
8e7eeb8d1f
[sledge] Update global
...
Reviewed By: mbouaziz
Differential Revision: D9846746
fbshipit-source-id: f5c465dd5
6 years ago
Josh Berdine
2b53e53504
[sledge] Update loc
...
Reviewed By: mbouaziz
Differential Revision: D9846744
fbshipit-source-id: b72291e5b
6 years ago
Josh Berdine
392f596b02
[sledge] Update exp
...
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D9846743
fbshipit-source-id: c293970c7
6 years ago
Josh Berdine
742b181282
[sledge] Update typ
...
Reviewed By: mbouaziz
Differential Revision: D9846741
fbshipit-source-id: 1c2876954
6 years ago
Josh Berdine
6a7c21e7c9
[sledge] Update trace and ppx_trace
...
Reviewed By: mbouaziz
Differential Revision: D9846738
fbshipit-source-id: 14adee4c4
6 years ago
Josh Berdine
91888c4c41
[sledge] Update import, vector
...
Reviewed By: mbouaziz
Differential Revision: D9934559
fbshipit-source-id: a446f386c
6 years ago
Josh Berdine
f6ba0c8137
[sledge] Update build system, etc.
...
Reviewed By: jvillard
Differential Revision: D9850346
fbshipit-source-id: 16fa35ae2
6 years ago
Josh Berdine
e1d4aad487
[ocamlformat] upgrade ocamlformat to 0.8
...
Reviewed By: mbouaziz
Differential Revision: D10359577
fbshipit-source-id: e7f5286e3
6 years ago
Josh Berdine
40ab73037e
[ocamlformat] upgrade to ocamlformat 0.7
...
Reviewed By: mbouaziz
Differential Revision: D9496601
fbshipit-source-id: 83c6fd241
6 years ago
Jules Villard
83a4a8fa5b
[dune] jbuilder -> dune
...
Summary: the_future_is_now
Reviewed By: jberdine
Differential Revision: D8933124
fbshipit-source-id: e5df1a9a3
6 years ago
Jules Villard
8b882ac1df
Change license to MIT
...
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
7 years ago
Josh Berdine
16988b0a7a
[ocamlformat] Upgrade to ocamlformat 0.5
...
Summary:
Upgrade ocamlformat, and base which needs to be done in sync in order to build
ocamlformat, and the other deps can come for the ride.
Reviewed By: jvillard
Differential Revision: D7663537
fbshipit-source-id: 3e90970
7 years ago
Josh Berdine
dcc0f646fe
Add demo LLAIR client
...
Reviewed By: mbouaziz
Differential Revision: D6892205
fbshipit-source-id: cae4354
7 years ago
Josh Berdine
446ac6d87c
Add initial version of LLAIR and LLVM to LLAIR translation
...
Reviewed By: mbouaziz
Differential Revision: D6892016
fbshipit-source-id: 3720749
7 years ago
Josh Berdine
d61b93b1d2
Create sledge directory
...
Reviewed By: jvillard
Differential Revision: D6871629
fbshipit-source-id: 57beac0
7 years ago