Klever

Ilja Zakharov wrote:

Since a cil file can contain lines with only line numbers or even lines without line directives at all our witness trace processor should correctly process witnesses for such files. I observe the following issues currently:

1. If a line directive is given without a file our witness processor should add the last referred file but not any default one.

This is likely a bug in verification tool. As far as I understand default values should be used if no values are specified in accordance with the GraphML format.

1. If for a line there is no line directive such lines should be somehow hidden or processed differently since startline data tag refers in the case to cilled file instead of an original C file.

This also seems to be a bug in verification tool. There is a common assumption that if processed line numbers correspond original ones then line directives aren't printed.

I think that this is already so in master.