[cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver

[Dominic Chen via cfe-dev]

I’m not sure what you mean by letting Z3 manage memory. Unless something has changed significantly since I looked at the source, the Z3 C++ API simply wraps memory management functions from the lower-level Z3 C API using C++ objects. Since the constraint manager is using the C API, due to compatibility issues with RTTI and exceptions, it needs to call the appropriate memory management functions.

Likewise, I’m not sure what cache memory you’re referring to. There was some discussion of a SMT query cache in CSA, but I don’t believe that was ever implemented.

Dominic

> On Mar 8, 2018, at 5:01 AM, Ashish Gahlot via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Hello,
> 
> I looked at the references on this mail http://lists.llvm.org/pipermail/cfe-dev/2018-March/057054.html <http://lists.llvm.org/pipermail/cfe-dev/2018-March/057054.html> and then looked at Z3ConstraintManager.cpp and I have some questions regarding the solver:
> 
> 1) Right now we are not letting Z3 manage memory. Will it be a good idea to do that?
> 2) Can we flush the cache memory in the destructor of Z3Solver https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp#L834 <https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp#L834> class?
> 
> Thank you very much,
> Ashish Kumar Gahlot
> 
> -- 
> Ashish Kumar Gahlot
> IV year, UG
> Govt. Engg. College, Ajmer, India
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180308/f4c03e87/attachment.html>