You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Oct 14, 2022. It is now read-only.
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
The text was updated successfully, but these errors were encountered:
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.
The witness linter will reject the example witness files from the repo:
The text was updated successfully, but these errors were encountered: