9618 Commits (d36aae1bcfceee08f52b7e51be2a47cc06e29bf3)
 

Author SHA1 Message Date
Nikos Gorogiannis caa7f9a7d7 [process pool] remove file locking protocol
4 years ago
Jules Villard e526cf157a [pulse] filter out unsat states earlier
4 years ago
Nikos Gorogiannis e152ba8f33 [stats] fix analyzed count
4 years ago
Sungkeun Cho e4b3971441 [frontend] Fix capture mode in ObjC
4 years ago
Sungkeun Cho 2d8f404a5f Revert "[Refactoring] Use pvar instead of mangled in CapturedVar"
4 years ago
Jules Villard ab2813e355 [pulse] canonicalize wrt equality relation
4 years ago
Jules Villard 5423bb1699 [pulse] make sure we checked satisfiability on summaries
4 years ago
Jules Villard 98b562c844 [pulse][refactor] extract and reuse a `SatUnsat` module
4 years ago
Jules Villard 581487ec61 [pulse] record aliasing information in the arithmetic
4 years ago
Sungkeun Cho 49bfd206a0 [Refactoring] Use pvar instead of mangled in CapturedVar
4 years ago
Sungkeun Cho 6972d9cb91 [Refactoring] Use inline record for captured variable type
4 years ago
Nikos Gorogiannis 695a3df7be [exe-env] refactor into a two-level hashtable
4 years ago
Nikos Gorogiannis 15943b1ea1 [biabduction] don't specialise models
4 years ago
Radu Grigore 6a61a85964 [topl] Refactor: Put constraint code in PulseTopl.Constraint.
4 years ago
Radu Grigore f8aa139b88 [topl] Be more precise in extracting summaries.
4 years ago
Radu Grigore 3478a8828f [topl] Added limits, to avoid high runtimes in corner-cases.
4 years ago
Ezgi Çiçek 7de9c49a6d [minor] Remove unnecessary exists check over singleton list
4 years ago
Nikos Gorogiannis 3ceac69079 [lru] strengthen tests with key-value pair order
4 years ago
Josh Berdine 3800a050f1 [sledge] Eliminate jumps to jumps
4 years ago
Josh Berdine 1e4e650dec [sledge] Change execution options from a record to a module
4 years ago
Josh Berdine 453068fa53 [sledge] Revise Control flow exploration algorithm
4 years ago
Josh Berdine bb52f96ded [sledge] Fix a fresh name clash when solving extract equations
4 years ago
Josh Berdine 77c630b7f4 [sledge] Normalize pure constraints when conjoining to a symbolic heap
4 years ago
Josh Berdine 481774c115 [sledge] Model operator new[](unsigned long)
4 years ago
Josh Berdine 10087c6281 [sledge] Strengthen spec of mallctl
4 years ago
Josh Berdine e7e1020e36 [sledge] Fix scope on return in case actual return clashes with formals
4 years ago
Josh Berdine 16a9b9f7d2 [sledge] Fix translation of alloca
4 years ago
Josh Berdine d33cecfa33 [sledge] Fix in Sh.simplify
4 years ago
Josh Berdine 86d129847c [sledge] Strengthen Arithmetic.solve_zero_eq
4 years ago
Josh Berdine 2726079a63 [sledge] Handle whether to follow exceptional control flow at model compilation
4 years ago
Josh Berdine c9185ae607 [sledge] Add __llair_unreachable intrinsic for use in model code
4 years ago
Josh Berdine 4605f505ce [sledge] Strengthen dynamic resolution of indirect calls
4 years ago
Josh Berdine 5c5126474e [sledge] Statically resolve known function calls
4 years ago
Josh Berdine 9e3ca541e8 [sledge] Revise name generation for return blocks of void-returning functions
4 years ago
Josh Berdine c346c5ec7f [sledge] Convert memset, memcpy, and memmov to intrinsics
4 years ago
Josh Berdine 6e5e127380 [sledge] Enable translation of intrinsic instructions for llvm intrinsics
4 years ago
Josh Berdine 31744dcfbf [sledge] Remove support for intrinsic functions
4 years ago
Josh Berdine 87ee0df07d [sledge] Convert intrinsic functions to instructions
4 years ago
Josh Berdine 1fddf1a5d0 [sledge] Add Exec.intrinsic for intrinsic instructions
4 years ago
Josh Berdine 4bae1ec07e [sledge] Rename exec_intrinsic to exec_intrinsic_func
4 years ago
Josh Berdine 9a07d6a778 [sledge] Reuse the translation of instruction intrinsics for Invoke
4 years ago
Josh Berdine f7894a3378 [sledge] Factor out computation of number of actuals for Call and Invoke
4 years ago
Josh Berdine 0603a7616b [sledge] Factor our Frontend normalization of callees
4 years ago
Josh Berdine 0fba102370 [sledge] Generate Intrinsic instructions in the frontend
4 years ago
Josh Berdine e9aff56bbc [sledge] Factor out Frontend translation of "instruction" intrinsics
4 years ago
Josh Berdine 074f668c00 [sledge] Add Intrinsic instruction
4 years ago
Josh Berdine c063a91c7c [sledge] Add Option.flat_map
4 years ago
Josh Berdine 2b89fa531a [sledge] Add CCBijection to Nonstdlib
4 years ago
Josh Berdine bb4c1e1133 [sledge] Represent function formal parameters and actual arguments in order
4 years ago
Josh Berdine b9bb3ca220 [sledge] Add Iter.fold_map and folding_map
4 years ago