Add toolinfo module for MetaVal 2.0

[marian-lingsch]

This PR adds the toolinfo module for a new tool called MetaVal 2.0. It is a witness validator, which is based on the ideas of transforming a task such that a backend tool can validate the witness.

Currently it mostly supports deductive verifiers like Frama-C as backend.

[PhilippWendler]

Why should this have a new tool-info module? Can't the existing tool-info module for MetaVal handle this or be extended to handle this?

[marian-lingsch]

Why should this have a new tool-info module? Can't the existing tool-info module for MetaVal handle this or be extended to handle this?

Thanks a lot for your comment!

Because they are two completely different tools. In particular there is no commonality in their code bases nor with how they are called, since they are based on completely different workflows and frameworks.

Extending the tool-info module for MetaVal is in principle possible, but reduces to having a flag checking which tool is being called and then delegating to the corresponding code. IMO it is nicer to have the separation be explicit as two different tool-info modules rather than implicitly as if statement in the code. This also indicates that that MetaVal 2.0 is not backwards compatible with MetaVal.

The only commonality is that they are based on the same principle i.e. instrument the program with the witness and pass it along to a backend verifier, but everything else differs completely. The name was suggested by Dirk to indicate that they are based on the same principle and to not have too many tool names.