Summary:
The SLEdge internal first-order theory solver targets the "word
problem", where a query has the form `C ⊢ L` where `C` is a
conjunction of literals and `L` is a single literal. This can be
abused to implement a naive SMT solver using an expansion to
disjunctive-normal form and checking `C ⊢ false` for each branch `C`
of the DNF. This is not useful as an SMT solver, but can be used for
testing.
Reviewed By: ngorogiannis
Differential Revision: D23459524
fbshipit-source-id: 5483e5a84
Summary:
The dune build info embedded into executables is broken with dune <
2.7 and an flambda compiler.
Reviewed By: ngorogiannis
Differential Revision: D23459510
fbshipit-source-id: 18b3e3e15
Summary:
It is now possible to not spew dune files all over the repo, and opam
files aren't needed either.
Reviewed By: jvillard
Differential Revision: D21720978
fbshipit-source-id: 553e1d154
Summary:
It seems to be effectively unmaintained, as it still doesn't support
4.08.
Reviewed By: jvillard
Differential Revision: D18708467
fbshipit-source-id: dcb3361fc
Summary:
Add a new interval abstract domain. This domain uses the APRON
numerical analysis library to keep track of the range of values held
by llair variables where possible. This works by translating LLAIR
expressions into APRON tree expressions, so only handles the
subset of the LLAIR expression language that can be embedded.
Note also that function summarization is not yet implemented.
Future commits will add summarization and improve coverage of
LLAIR's expression language.
Reviewed By: jberdine
Differential Revision: D17763517
fbshipit-source-id: 826ce4cc5
Summary:
Replace custom version reporting support using a shell script with
code using dune's Build_info API.
Note that after this diff, the executables under _build/<context> are
not version-stamped, but those under _build/_install are. The symlinks
in bin point to the latter, stamped, exes.
Reviewed By: bennostein
Differential Revision: D16985446
fbshipit-source-id: 7afac87be
Summary:
This adds an optimized debug build mode, which is compiled with
optimizations, and without assertions, but still has tracing enabled.
Reviewed By: kren1
Differential Revision: D16069452
fbshipit-source-id: 445cfa329
Summary:
Change command line interface to include buck and llvm integration as
separate subcommands.
Reviewed By: kren1
Differential Revision: D15614567
fbshipit-source-id: b7618571b
Summary:
* Adds compilation of cxxabi.bc
* Includes the cxxabi.bc into the sledge executable via opam-crunch
* Links cxxabi.bc in sledge frontend
Reviewed By: jberdine
Differential Revision: D15415190
fbshipit-source-id: cc42f09fb
Summary:
This triggers dune to build the minimum necessary to type-check and
populate files merlin uses for cross-module information.
Reviewed By: mbouaziz
Differential Revision: D10389480
fbshipit-source-id: 1ac7e0584
Summary: Dune now includes support for ocamlformat, so use it to format in parallel.
Reviewed By: mbouaziz
Differential Revision: D10389485
fbshipit-source-id: cb1dfbe38
Summary:
Call __cxa_demangle from libstdc++ using Ctypes instead of the
wrapper in Llvm.
Reviewed By: mbouaziz
Differential Revision: D9939682
fbshipit-source-id: a9f02fff5
Josh Berdine
Benno Stein
Timotej Kapus