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

Ashish Gahlot via cfe-dev cfe-dev at lists.llvm.org
Thu Mar 8 02:01:47 PST 2018


Hello,

I looked at the references on this mail
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180308/3a5be83c/attachment.html>


More information about the cfe-dev mailing list