MartinSpiessl

Make repository reuse compliant

1

This should be easy to implement, we just need to add the appropriate license comments to each file and add a CI pipeline that runs the reuse tool, cf. https://reuse.software/

Clarification of keys `cycle-head` and `invariant` is needed for termination witnesses

2

It has become unclear whether enforcing the [current spec](https://github.com/sosy-lab/sv-witnesses/blob/master/termination/README.md) that says: > Thus, a node for which the cyclehead key is set, must also contain an invariant description. makes sense....

It is clear that the witness linter might break unexpectedly in case we do not have a set of tests that is continuously executed.

Reconsider the `architecture` description in the witness graphml files

1

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...

Example for a correctness witness contains forbidden data key `control`

13

The example [multivar_true-unreach-call1.graphml](https://github.com/sosy-lab/sv-witnesses/blob/master/multivar_true-unreach-call1.graphml) for a correctness witness in this repository contains control annotations like the following: [!(x < 1024)] 12 305 condition-false According to the `README.md`, the data key `control`...

This way it would be easier for users to execute the witnes linter against their witnesses to check whether they are conformant with the spec

Link to the corresponding issue: https://projects.theforeman.org/issues/37857 This fixes some bugs that I found in the clevis/tang that was added via https://github.com/theforeman/foreman/pull/9887 It should overall increase the usefulness of this feature...

Fixes #38424: correct response code of oauth2 token request to registry

4

If oauth2 authentication (via POST request) is not supported, a container registry should respond with code 404, but we currently respond with 415 (Unsupported Media Type). By disabling the media...

This adds a playbook/remote execution feature to upgrade an orcharhino Proxy. It also ensures that the distinction between Foreman, Satellite, and orcharhino is properly made everywhere where the proxy upgrade...