[cfe-dev] [GSoC] Re: CSA constraint solver improvements

[via cfe-dev]

Good to hear that someone is interested in the SMT Solver part of the analyzer.

Mikhail Ramalho is probably the primary driving factor in this direction, but I try to participate/help as much as I can.
You probably already know, Artem Dergachev is the code owner of the CSA, so I guess, you can count on him as well.

Unfortunately, the SMT solver is not maintained, thus it is in pretty bad shape. It can not pass the tests for various reasons.
I planned to improve the situation, but it was always a low priority for me. My primary concern is the Z3 solver for bugreport refutation for the range-based solver.

I recommend you have a look at patches in the past using git blame.
AFAIK these three are the most important patches which not landed yet:
D83677, D83660, D85528

Regards, Balazs.

-----Original Message-----
From: cfe-dev <cfe-dev-bounces at lists.llvm.org> On Behalf Of Manas via cfe-dev
Sent: 2021. április 9., péntek 10:01
To: clang-front-end mailing list <cfe-dev at lists.llvm.org>
Subject: [cfe-dev] [GSoC] Re: CSA constraint solver improvements

Hi everyone, 

I am a pre-final year undergraduate in computer science. I am interested in "Clang Static Analyzer: constraint solver improvements" project.

I have around 8 months of experience with LLVM/Clang during my compilers class where I also implemented some dataflow analysis techniques for LLVM IR. I am also in middle of completing my decision procedures course at university. This course has helped me in gaining fundamental knowledge about solvers. I am familiar with range-based logic. Along with these, I have tried z3 while learning about solvers, and I think I can learn more about it fairly quickly.

I think this project fits for me. It will also help me in improving my knowledge further. I have started working on my proposal.

Can you give me further directions regarding the proposal for this project?

Thank you
--
Manas
CSAM Undergraduate | 2022
IIIT-Delhi, India
_______________________________________________
cfe-dev mailing list
cfe-dev at lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev