sosy-lab/sv-witnesses

Reconsider the `architecture` description in the witness graphml files

MartinSpiessl opened this issue · 1 comments

For the task definition files we now have a consistent filed named data_model that contains either ILP32 or LP64:
https://github.com/sosy-lab/sv-benchmarks#task-definitions

  • options: parameters that are relevant for verification or give extra information:

This is more precise than what we currently put under architecture in the witness(32bit/64bit), as the number of bits in the architecture doesn't fix the whole data model (e.g. there are differences in the data model for ARM64 vs. AMD64).

So we should consider to extend the witness format by a datamodel /data-model field that stores this more precise information. We could then deprecate the old architecture field, so validators still undetstand that one but use the data model if specified.

In general, using the same strings as in the task definitions is certainly a good idea.

Note sosy-lab/sv-benchmarks#1125: would be beneficial to come to a conclusion on that issue before adding the same values to the witness format.