This schema describes the YAML format for correctness witnesses.
A correctness witness consists of one or more entries of type invariant_set or ghost_instrumentation.
If there are more than one entries of type invariant_set, or
if there are more than one loop or location invariants in the content,
the order of their occurrence is not important.
The order of ghost_instrumentation entries and ghost_updates in the content is however important,
as it defines the order in which multiple ghost updates at the same location are performed.
A correctness witness is syntactically valid if it fulfills the below syntactical requirements.
The correctness witness is semantically valid if it is syntactically valid and
it fulfills the following semantical requirements.
loop_invariant, the invariant must hold on every execution of the programghost_instrumentations have been applied) whenever the condition of thelocation_invariant, the invariant must hold on every execution of the programghost_instrumentations have been applied) whenever the execution is going toEach entry consists of three key-value pairs, namely the key entry_type with value invariant_set or ghost_instrumentation,
the key metadata, and the key content.
If the conditions in the "If" tab are respected, then the conditions in the "Then" tab should be respected. Otherwise, the conditions in the "Else" tab should be respected.
"invariant_set" The content represents the semantical content of the correctness witness.
It is a sequence of one or more invariant elements.
The key invariant is the basic building block of correctness witnesses.
It is a mapping that describes one invariant.
The type has the value loop_invariant for iteration statements, or location_invariant for arbitrary statements.
It specifies the type of the invariant.
The location points to the first keyword character in a source file.
More specifically, the location of a loop invariant must point to the first keyword
(for, while, do) character of an iteration statement,
while the location of a location invariant must point to the first character of an arbitrary
statement or a declaration that is within a compound statement.
If column is not given, it is assumed to match the leftmost suitable position.
The key value holds the actual invariant string
(e.g., "s <= i*255 && 0 <= i && i <= 255 && n <= 255").
The invariant value must be a side-effect-free C expression (the only supported format for invariants so far)
over program variables in the scope of the statement or declaration inside a compound statement to which the location points,
as well as any ghost variables declared in the witness (if they are in scope).
Evaluation of the expression at the location must not lead to undefined behaviour.
Invariants in concurrent programs are evaluated atomically, i.e., there may be no context switches during the evaluation.
An invariant in some thread may only be evaluated when all other currently running threads are at a sequence point.
By assumption, invariant evaluation does not cause data races.
The format specifies the format of the invariant string (e.g., c_expression).
If the conditions in the "If" tab are respected, then the conditions in the "Then" tab should be respected. Otherwise, the conditions in the "Else" tab should be respected.
"ghost_instrumentation" The content represents the semantical content of the correctness witness.
It is a sequence of one or more ghost variable instrumentations composed of ghost variable declarations and ghost updates.
Ghost variables can be updated at specific locations during the execution of the program, and may be referred to in location invariants and other witness elements, unless otherwise specified.
A set of ghost variable declarations.
No Additional ItemsDeclares and initializes a ghost variable used in this correctness witness.
A valid identifier used as name of the ghost variable.
This identifier must be unique across the correctness witness, and must not be used in the program.
A data type for the ghost variable, either built-in or declared in the program.
The scope of the ghost variable.
For now, only global ghost variables are supported.
Initial value of the ghost variable.
A syntactically well-formed expression without side-effects, and without calls to functions defined in the program.
The only variables allowed in this expression are the global variables of the program.
The expression is evaluated after global variables declared in the program are initialized.
Evaluation of the expression must not lead to undefined behaviour.
The format of the expression from the value string for the ghost variable's initial value.
A list of ghost variable updates.
No Additional ItemsUpdates the value of a ghost variable used in this correctness witness.
Ghost variables can be updated at specific locations during the execution of the program, and may be referred to in location invariants and other witness entries, unless otherwise specified.
The location at which the ghost variable is updated.
Specifically, the ghost update is executed when control exits the specified location.
The ghost update is performed atomically together with the action leaving the location.
If there are multiple ghost updates for the same location, they are performed in the order in which they appear in the witness.
Optionally, the ghost update may be performed only for certain actions leaving a location rather than for all actions; for instance, only if a branch evaluates to true.
The specification of the selected actions should be analogous to branching waypoints in violation witnesses.
A list of ghost updates that are executed at the specified location.
The ghost updates are executed in the order in which they are specified.
Updates a ghost variable at the specified location.
The identifier for the updated ghost variable.
This ghost variable must be declared in a ghost_variables object in the correctness witness.
A syntactically well-formed expression without side-effects, and without calls to functions defined in the program.
The expression may use any program variables that are in scope at the specified location, as well as any ghost variables declared in the witness (if they are in scope).
Evaluation of the expression upon reaching the location must not lead to undefined behaviour.
We assume that the evaluation is performed atomically, i.e., there may be no context switches during the evaluation.
A ghost update in some thread may only be performed when all other currently running threads are at a sequence point.
By assumption, the evaluation does not cause data races.
The format of the expression from the value string for the ghost update.
The entry_type defines what content is available in the content field.
The only allowed entry types for a correctness witness are invariant_set and ghost_instrumentation.
The meta data describe the provenance of the data.
The version of the format is given as a string (currently "2.1").
The uuid is a unique identifier of the entry;
it uses the UUID format defined in RFC4122.
The creation_time describes the date and time when the entry was created;
it uses the format given by ISO 8601.
The key producer describes the tool that produced the entry.
The name of the tool that produced the witness.
The version of the tool.
The configuration in which the tool ran.
The command line with which the tool ran;
it should be a bash-compliant command.
Any information not fitting in the previous items.
The task describes the verification task to which the entry is related.
The list of files given as input to the verifier,
e.g. ["path/f1.c", "path/f2.c"].
The SHA-256 hashes of all files in input_files,
e.g. {"path/f1.c": 511..., "path/f2.c": f70...}
Each additional property must conform to the following schema
Type: stringThe specification considered by the verifier;
it uses the SV-COMP format given at
https://sv-comp.sosy-lab.org/2023/rules.php.
The data model assumed for the input program.
The programming language of the input files;
the format currently supports only C.