6095 Commits (81909abf23e8f797e30de2a2488c48d54da047c7)
 

Author SHA1 Message Date
Mehdi Bouaziz 81f31068e2 [Uninit][9/13] Check rhs using prestate
6 years ago
Mehdi Bouaziz d8ecfbfc4b Do not compare types of array elements in access paths and access expressions
6 years ago
Mehdi Bouaziz b3cef556b7 [debug] Print types in access paths/expressions in verbose mode
6 years ago
Mehdi Bouaziz 5ee9ea9e48 Fix warning
6 years ago
Josh Berdine 9e724842f6 [sledge] Update todo
6 years ago
Josh Berdine 889f7abc6f [sledge] Dump program to file between frontend and backend
6 years ago
Josh Berdine 080c843856 [sledge] Add maybe-alloc instruction that may fail
6 years ago
Josh Berdine f3d25d3a23 [sledge] Refactor issue reporting to Report module
6 years ago
Josh Berdine 1b11a0df0e [sledge] Improve debug tracing
6 years ago
Josh Berdine cf2a985073 [sledge] Add Trace.{printf,fprintf,kprintf}
6 years ago
Josh Berdine da89fc8f95 [sledge] Warn of each uninterpreted intrinsic only once
6 years ago
Josh Berdine 452e240e67 [sledge] Simplify CLI implementation using ppx_deriving_cmdliner
6 years ago
Josh Berdine 85d9e5bdb0 [sledge] Add `make check` using `dune build @check`
6 years ago
Josh Berdine d5a83894b0 [sledge] Run executables from dune install dir
6 years ago
Josh Berdine a9cdf69010 [sledge] Use dune ocamlformat integration for `make fmt`
6 years ago
Dino Distefano 3d07754275 Giving cost 1 to procedure with empty body
6 years ago
Jules Villard 7bd4aaa819 [pulse] pulse models
6 years ago
Jules Villard 3821be4b7f [pulse] fix compilation error in test
6 years ago
Mehdi Bouaziz dffdd9c2ad [cost] Print constraints in HTML debug
6 years ago
Jules Villard d28d0528d1 [pulse] initial commit
6 years ago
Jules Villard 98f65298c5 [log] do not crash when logging errors
6 years ago
Mehdi Bouaziz a2230bca9d [debug] Print nodes using weak topological order
6 years ago
Mehdi Bouaziz 8ef9bf7641 Expose WTO in ProcCfg
6 years ago
Mehdi Bouaziz b324dbd8dd Use WTO to get loop heads
6 years ago
Mehdi Bouaziz 0d4c06efc5 WTO: use a partial ProcCfg
6 years ago
Jules Villard dd2b9675d6 [log] print only innermost source file context of crash
6 years ago
Jules Villard bee7649048 [perf] fix capture traces and record clang events
6 years ago
Sungkeun Cho fd660f42f5 [inferbo] Suppress exception on placement new
6 years ago
Dino Distefano 2e64566a6c Finding stateless CKComponents
6 years ago
Mehdi Bouaziz 371e1267d9 [debug] Get rid of proof_cover/isproof
6 years ago
Mehdi Bouaziz b71af05f00 Stats: merge visited_fp and visited_re
6 years ago
Mehdi Bouaziz f873debc96 [inferbo] Debug latest prune abstract value
6 years ago
Ezgi Çiçek 78a865b14e [hosting] Disable purity and cost callbacks temporarily
6 years ago
Ezgi Çiçek 99c2a6da8d [hoisting] Hoist only expensive pure functions
6 years ago
Josh Berdine e71ea9f0ed [sledge] Switch from Llvm.demangle to __cxa_demangle via Ctypes
6 years ago
Josh Berdine 27f08ab53a [sledge] Update entry point and command line interface
6 years ago
Josh Berdine b712a57bf9 [sledge] Add analysis based on iterative bounded exploration
6 years ago
Josh Berdine 0a09581431 [sledge] Add abstract domain interface
6 years ago
Josh Berdine 4633419b1c [sledge] Add symbolic execution
6 years ago
Josh Berdine e397a43f80 [sledge] Add frame inference solver over symbolic heaps
6 years ago
Josh Berdine 83eff4c734 [sledge] Add symbolic heap formulas
6 years ago
Josh Berdine a32890a1e3 [sledge] Add congruence closure with integer offsets
6 years ago
Josh Berdine f7a9a0c323 [sledge] Update frontend
6 years ago
Josh Berdine 2c116474e5 [sledge] Update llair
6 years ago
Josh Berdine 8e7eeb8d1f [sledge] Update global
6 years ago
Josh Berdine 2b53e53504 [sledge] Update loc
6 years ago
Josh Berdine 392f596b02 [sledge] Update exp
6 years ago
Josh Berdine 742b181282 [sledge] Update typ
6 years ago
Josh Berdine 6a7c21e7c9 [sledge] Update trace and ppx_trace
6 years ago
Josh Berdine 91888c4c41 [sledge] Update import, vector
6 years ago