Cannot run LogicalCompare to completion

[JChen677]

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]

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

[JChen677]

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]

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]

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]

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]

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]

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.