Replies: 1 comment 1 reply
-
The easiest (and nicest IMHO) approach is to use clang's bug report: it generates an HTML file with the actual code, and you can follow the bug with the 'j' and 'k' keys on your keyboard. I think it generates another formats as well, but I'm not sure. It offers options to add notes to each step, with the values assigned to variables and whatnot. Another advantage is that we wouldn't need to create anything new, just reuse a well-maintained code. Implementation-wise we would probably need to keep the clang AST alive for the whole verification, but this is usually not a big overhead. |
Beta Was this translation helpful? Give feedback.
1 reply
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Just wanted to start this discussion about the readablity of counter-examples in order to collect ideas:
Suppose, instead of or in addition to printing the current counter-example, we could generate an .html file displaying the given original source code and highlighting the following:
I believe we do have all this information available to us via the locations of GOTO statements and the counter-example's values. Would it be feasible to generate such an output? I imagine it would help with clarifying the counter-examples produced, and it could also help in understanding the witness files better if those were linked to this display as well.
Beta Was this translation helpful? Give feedback.
All reactions