search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

Better error traces #742

Closed shaobo-he closed 3 years ago

zvonimir commented 3 years ago

Do you pretty print from json? Or is pretty printing completely independent from json generation?

You say: "Pretty-printing includes removal of duplicate lines as well as Boogie assertion failures that should be opaque to the users." Does that mean that json will include duplicate lines and Boogie assertion failures?

Thx!

shaobo-he commented 3 years ago

Do you pretty print from json? Or is pretty printing completely independent from json generation?

You say: "Pretty-printing includes removal of duplicate lines as well as Boogie assertion failures that should be opaque to the users." Does that mean that json will include duplicate lines and Boogie assertion failures?

Thx!

I think they are independent. JSON output contains duplicate lines while they are merged during pretty printing.

zvonimir commented 3 years ago

Coming back to this. I think it is weird that json output and pretty printing are not consistent. I think that duplicates should be first removed from json. Pretty printing should not ideally do any post-processing, but just spit out whatever is in json. Does that make sense? @shaobo-he ? Thanks!

shaobo-he commented 3 years ago

Coming back to this. I think it is weird that json output and pretty printing are not consistent. I think that duplicates should be first removed from json. Pretty printing should not ideally do any post-processing, but just spit out whatever is in json. Does that make sense? @shaobo-he ? Thanks!

Yes, it makes sense. Let me try to fix it.

shaobo-he commented 3 years ago

Ok. I moved pruning redundant lines from printing to the end of JSON data generation.