The version of cbmc at the tip of develop now includes in its coverage output an xml/json element for each basic block that gives the set of source lines contributing to that basic block. Prior versions of cbmc encoded this set of source lines in a text string used as the description of the coverage goal corresponding to this basic block. Parsing this string encoding source lines was too brittle to handle function names used by kani.
This pull request modifies viewer to use the new xml/json elements if they exist, and to revert to paring the text string if they do not. It also advances version 3.0.1 -> 3.1.
Testing: For cbmc version 5.56.0 and cbmc version at the tip of develop, I have compared the output of viewer 3.0.1 and 3.1 on the coreHTTP proofs and found the outputs to be identical. So the new 3.1 works with the xml/json elements (produced by the new cbmc) and without (produced by the old cbmc). And the new cbmc does not break either of the old and new viewers. The two versions of cbmc change their output enough that comparing across versions of cbmc is not practical.
The commits have been prepared carefully to make it easy to review this pull request commit by commit.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
The version of cbmc at the tip of develop now includes in its coverage output an xml/json element for each basic block that gives the set of source lines contributing to that basic block. Prior versions of cbmc encoded this set of source lines in a text string used as the description of the coverage goal corresponding to this basic block. Parsing this string encoding source lines was too brittle to handle function names used by kani.
This pull request modifies viewer to use the new xml/json elements if they exist, and to revert to paring the text string if they do not. It also advances version 3.0.1 -> 3.1.
Testing: For cbmc version 5.56.0 and cbmc version at the tip of develop, I have compared the output of viewer 3.0.1 and 3.1 on the coreHTTP proofs and found the outputs to be identical. So the new 3.1 works with the xml/json elements (produced by the new cbmc) and without (produced by the old cbmc). And the new cbmc does not break either of the old and new viewers. The two versions of cbmc change their output enough that comparing across versions of cbmc is not practical.
The commits have been prepared carefully to make it easy to review this pull request commit by commit.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.