Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Cannot run LogicalCompare to completion #264

Open
JChen677 opened this issue Jul 11, 2020 · 7 comments
Open

Cannot run LogicalCompare to completion #264

JChen677 opened this issue Jul 11, 2020 · 7 comments

Comments

@JChen677
Copy link

Hello,
I am trying to use LogicalCompare to compare invariants, but when I do I consistently receive a java.lang.NullPointerException directly after "Testing Postconditions:" of the LogicalCompare output.

I built Daikon and Kvasir from the git repo, following exactly the instructions in the documentation. I installed Simplify from the zip file pointed to by the documentation and marked Simplify-1.5.4.linux for usage. An exact bash command log is attached below.
cmds.txt

I am running on Ubuntu version 18.04 and have attached a copy of the output from LogicalCompare below.
lcOut.txt

Thank you,
Jeffrey Chen

@markro49
Copy link
Contributor

Thanks for submitting an issue. We hope to investigate shortly.

@markro49 markro49 transferred this issue from codespecs/fjalar Jul 13, 2020
@JChen677
Copy link
Author

Hello,
As per the Daikon documentation, I have been trying to see if I can replace Simplify with an older version of Z3 when using LogicalCompare. However, the documentation does not say which version of Z3 is useable or how to tell Daikon to utilize Z3 instead of Simplify. Could you answer these questions or point me to documentation which answers these questions?

Thank you,
Jeffrey

@mernst
Copy link
Member

mernst commented Jul 15, 2020

I don't have information about the right version of Z3. Sorry about that.

(Daikon should really be upgraded to use the current version of Z3 rather than an old file format that current tools don't support.)

@mernst
Copy link
Member

mernst commented Jul 16, 2020

By the way, this particular bug is likely to be in Daikon itself, rather than in Simplify. So seeking a version of Z3 is probably not fruitful right now.

@mernst
Copy link
Member

mernst commented Jul 16, 2020

Thanks for including the commands to reproduce the problem. That is very helpful. They did not work for me -- a few of the file and directory names were wrong. I have attached a slightly edited set of commands that worked for me.
cmds.txt

@JChen677
Copy link
Author

Hello,
I was wondering if you had an estimated time frame for how long this might take to resolve, or to at least become usable in some form.

Thank you,
Jeffrey Chen

@mernst
Copy link
Member

mernst commented Jul 22, 2020

Sorry for the delay. I make fixes outside my normal work, because Daikon is a hobby. I went backpacking last weekend instead of bug-fixing. :-)

I'll get to this as soon as possible. The time depends on how deep the bug is. I understand the first problem, but I also know there is another problem which is masked by that one.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants