- User Since
- Jun 22 2020, 11:10 PM (22 w, 5 d)
Thu, Nov 26
Mon, Nov 23
Some of my fixes still need to be improved (see the comments in the code). If any reviewers have better ideas, I will update the patch.
Sun, Nov 22
Thu, Nov 19
- Replace fatal errors with assertions.
Tue, Nov 17
Mon, Nov 16
Fri, Nov 13
Oct 22 2020
Since SymbolRef is just a const SymExpr * in the current codebase, I'd prefer using const SymExpr * directly, just like how MemRegion is used, which would be clearer than both SymbolRef and SymExprRef as far as I am thinking.
Oct 15 2020
Yes, it's being used in the FindZ3.cmaks script.
I have another try in a newly installed system without Z3 installed from the distribute software source, and the following tests are carried out in /tmp/ella.z3-patch.
Oct 11 2020
Sep 23 2020
Sep 9 2020
After reviewing the code of this snippet, I think it would be very difficult to make a regression test case for the crash, as far as what I know about Z3 and SMT solvers.
Sep 8 2020
We have tried to trigger the crash with the original project where the crash was encountered. But the problem is we cannot trigger the crash with the project, and we have lost all the previous records about this crash. Besides, both I and the bug reporter himself are now working on our own research right now. We have very limited time working on this patch in recent months. We are now planning to just make a simple regression test case to trigger the crash during our spire time. Sorry for the delay.
Aug 23 2020
Aug 12 2020
Ok, I got it. I will pay attention to this in the future submits.
Aug 11 2020
Now it has a link to the getEndPath.
Aug 2 2020
Jul 14 2020
Might in the future I would spend some time on it - we will see.
@steakhal My boss always asks me about how to improve the performance for SMT solver based constraint solving, on both the engine side and the SMT solver side. If there is anything that our research group can do, you are free to contact us.
BTW nice catch & fix.
Thank you. This crash was discovered by one of our team members when we were testing our CSA based tool. If the patch gets merged in the future, I'd like to use his name and email for the commit.
do you accidentally have a test case to reproduce the crash
@NoQ I am now working with the reporter of this bug to make a simple test case to trigger the crash.
Jul 13 2020
@vsavchenko Ella Ma <firstname.lastname@example.org>. Thank you.
@vsavchenko @dcoughlin @NoQ
I do not know whether it is correct to ping somebody like this. As this is my first submitted review, I do not know what should I do next, when the patch has been accepted by one of the reviewers while others have not given any comments. Should I continue waiting for other reviewers? And what should I do with the bug report (https://bugs.llvm.org/show_bug.cgi?id=44753)?