sosy-lab/sv-witnesses

Example witness files in the repo do not pass linter

RyanGlScott opened this issue · 2 comments

RyanGlScott commented

The witness linter will reject the example witness files from the repo:

$ ./lint/witnesslinter.py minepump_spec1_product33_false-unreach-call_false-termination.cil.c --witness minepump_spec1_product33_false-unreach-call_false-termination.cil.graphml 
WARNING : Creationtime has not been specified

witnesslint finished with exit code 1

$ ./lint/witnesslinter.py minepump_spec1_product33_false-unreach-call_false-termination.cil.c --witness minepump_spec1_product33_false-unreach-call_false-termination.cil.ultimateautomizer.graphml 
WARNING : line 4: Unexpected default namespace: http://graphml.graphdrawing.org/xmlns/graphml
WARNING : Key 'architecture' has been used but not defined
WARNING : Key 'specification' has been used but not defined
WARNING : Key 'programfile' has been used but not defined
WARNING : Key 'programhash' has been used but not defined
WARNING : Key 'producer' has been used but not defined
WARNING : Creationtime has not been specified

witnesslint finished with exit code 1

$ ./lint/witnesslinter.py minepump_spec1_product33_false-unreach-call_false-termination.cil.c --witness multivar_true-unreach-call1.graphml 
WARNING : line 54: Programhash does not match the hash specified in the witness
WARNING : Creationtime has not been specified

witnesslint finished with exit code 1
SvenUmbricht commented

True, those example witnesses should be replaced with more recent ones that conform to the format.

Neither witness contains a creationtime, which is required according to the spec and would not pass the linter for that reason alone. The automizer witness is also missing some key declarations that are not required by the witness format, but by the GraphML specification.. Similarly for the namespace that is xmlns="http://graphml.graphdrawing.org/xmlns/graphml" instead of the expected xmlns="http://graphml.graphdrawing.org/xmlns".

Both producing tools were used in SV-COMP '21 and should therefore now produce witnesses for the example programs that pass the linter checks.

The programhash mismatch for multivar_true-unreach-call1.graphml is due to using the wrong program as input, the witness was actually created for multivar_true-unreach-call1.i not for minepump_spec1_product33_false-unreach-call_false-termination.cil.c.

SvenUmbricht commented

All examples also use the SHA-1 hash of the program, which is no longer supported (cf. #42), and fail the corresponding linter check since 5b18209.

@MartinSpiessl @danieldietsch Could you replace the example witnesses with more recent ones that comply with the format?

  • 👍1