Skip to content
This repository has been archived by the owner on Oct 14, 2022. It is now read-only.

Reconsider the architecture description in the witness graphml files #22

Open
MartinSpiessl opened this issue Nov 26, 2020 · 1 comment

Comments

@MartinSpiessl
Copy link
Collaborator

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.

@PhilippWendler
Copy link
Member

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.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Development

No branches or pull requests

2 participants