search for: cvc4

Hi, I am wondering if anyone could run ArrayBoundChecks located in SafeCode-llvm37 (https://github.com/jtcriswell/safecode-llvm37) on llvm-3.8? Thanks. Syed -- Rafi

We are currently implementing the backends for other solvers (you can follow the progress here: https://github.com/mikhailramalho/clang). So far we got Boolector, MathSAT and Yices ready. CVC4 should be done soon. When used to refute bugs, they all give roughly the same results: a ~5% speedup if there are refuted bugs or a ~5% slowdown if no bug is refuted. I've only tried to analyze one full project (tmux) with Yices; the CSA ran for 24hrs and it didn't complete the analyze. F...

Hi all, Currently studying the impact of SMT solvers on Clang SA. Can anyone help in telling more about the SMT solvers use in clang SA ? ( Have already tested Z3 SMT solver implemented in GSoC 2018 , also looking for other SMT solvers if possible ) Thanks, Siddharth -------------- next part -------------- An HTML attachment was scrubbed... URL:

Thanks for the fast response John. On Thu, Oct 1, 2015, at 04:51 PM, John Criswell wrote: > Dear Ed, > > First, someone has updated the DSA code in the poolalloc project to LLVM > 3.7, and a Master's student worked for me over the summer to update a > large chunk of SAFECode to LLVM 3.7. However, the update to LLVM 3.7 > isn't finished (we need to finish integrating

...it-rotted away, and its implementation was not the most efficient (it >>exec()'ed the Omega solver for every query). A better approach today >>would be to integrate the constraint solver into the compiler proper. >>Additionally, you now have other tools available, such as CVC4, Z3, and >>SMACK/Boogie, for building and solving the constraints. > >We had already noticed that the limit to linear array access was way >behind state of the art (we have a lot of experience with constraint >solvers). Using an SMT solver would make sense, as you can use the &gt...