Format for Violation Witnesses, version 2.0

Type: array of object

This schema describes the YAML format for violation witnesses.

A violation witness consists of one or more entries of type violation_sequence.

A violation witness is syntactically valid if it fulfills the below syntactical requirements.

The violation witness is semantically valid if it is syntactically valid and
it fulfills the following semantical requirements.

Each violation witness represents some program executions violating the specified property.
The witness is considered to be valid if the set is nonempty.

More precisely: Let us consider a violation witness with 𝑛 ≥ 1 segments.
An execution is represented by this witness, if it can be divided into 𝑛 parts
such that, for each 1 ≤ 𝑖 ≤ 𝑛, the 𝑖-th part matches the corresponding segment of the witness.
An execution part matches a normal segment if

The final execution part matches the final segment if

An assumption waypoint is evaluated at the sequence point immediately before the waypoint location.
The waypoint is passed if the given constraint evaluates to true.
A target waypoint marks the violation of the specification.

Each item of this array must be:

root root items
Type: object

Each entry consists of three key-value pairs, namely the key entry_type with value violation_sequence,
the key metadata, and the key content.

root root items entry_type
Type: enum (of string)

The entry_type defines what content is available in the content field.
The only allowed entry type for a correctness witness is violation_sequence.

Must be one of:

  • "violation_sequence"

root root items metadata
Type: object

The meta data describe the provenance of the data.

root root items metadata format_version
Type: string

The version of the format is given as a string (currently "2.0").

root root items metadata uuid
Type: stringFormat: uuid

The uuid is a unique identifier of the entry;
it uses the UUID format defined in RFC4122.

root root items metadata creation_time
Type: stringFormat: date-time

The creation_time describes the date and time when the entry was created;
it uses the format given by ISO 8601.

root root items metadata producer
Type: object

The key producer describes the tool that produced the entry.

root root items metadata producer name
Type: string

The name of the tool that produced the witness.

root root items metadata producer version
Type: string

The version of the tool.

root root items metadata producer configuration
Type: string

The configuration in which the tool ran.

root root items metadata producer command_line
Type: string

The command line with which the tool ran;
it should be a bash-compliant command.

root root items metadata producer description
Type: string

Any information not fitting in the previous items.

root root items metadata task
Type: object

The task describes the verification task to which the entry is related.

root root items metadata task input_files
Type: array of string

The list of files given as input to the verifier,
e.g. ["path/f1.c", "path/f2.c"].

Each item of this array must be:

root root items metadata task input_files input_files items
Type: string

root root items metadata task input_file_hashes
Type: object

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

root root items metadata task input_file_hashes additionalProperties
Type: string

root root items metadata task specification
Type: string

The specification considered by the verifier;
it uses the SV-COMP format given at
https://sv-comp.sosy-lab.org/2023/rules.php.

root root items metadata task data_model
Type: enum (of string)

The data model assumed for the input program.

Must be one of:

  • "ILP32"
  • "LP64"

root root items metadata task language
Type: enum (of string)

The programming language of the input files;
the format currently supports only C.

Must be one of:

  • "C"

root root items content
Type: array of object

The content represents the semantical content of the violation witness.
It is a sequence of one or more segments.

The content contains a sequence of zero or more normal segments and exactly one final segment at the end.

Each item of this array must be:

root root items content content items
Type: object

root root items content content items segment
Type: array of object

A segment is a sequence of one or more waypoints.
They are used to structure the waypoints into segments.
Each segment is a sequence of zero or more waypoints with action avoid and
exactly one waypoint of action follow at the end.
A segment is called final if it ends with the target waypoint and it is called normal otherwise.

Each item of this array must be:

root root items content content items segment segment items
Type: object

root root items content content items segment segment items waypoint
Type: object

The waypoint elements are the basic building block of violation witnesses.
They have the form of simple restrictions on program executions.
Technically, a waypoint is a mapping with four keys, namely type, location, constraint, and action.
The values of the first three keys specify the requirement on a program execution to pass a waypoint:
type describes the type of the requirement,
location specifies the program location where the requirement is evaluated, and
constraint gives the requirement itself and is not allowed for waypoints of type function_enter and target.
The key action then states whether the executions represented by the witness should
pass through the waypoint (value follow) or avoid it (value avoid).
The format currently supports two possible values of type with the following meanings:

  • assumption:
    The location has to point to the beginning of a statement or a declaration inside a compound statement.
    A requirement of this type says that a given constraint is satisfied before the pointed statement
    or declaration inside a compound statement.
    The constraint is a mapping with two keys: format specifies the language of the assumption and
    value contains a side-effect-free assumption over variables in the current scope.
    The value of format is c_expression as C expressions are the only assumptions currently supported.
    In future, we plan to support also assumptions in ACSL.
  • target:
    This type of requirement can be used only with action follow and it marks the program location where the property is violated.
    More precisely, the location points at the first character of the statement or
    full expression whose evaluation is sequenced directly before the violation occurs,
    i.e., there is no other evaluation sequenced before the violation and the sequence point associated with the location.
    This also implies that it can only point to a function call if it calls a function of the C standard library
    that violates the property or if the function call itself is the property violation.
    The key constraint has to be omitted for type target.
  • function_enter:
    The location points to the right parenthesis after the function arguments at the call site and the requirement
    says that the called function is entered. The key constraint has to be omitted in this case.
  • function_return:
    Such a requirement says that a given function call has been evaluated and the returned
    value satisfies a given constraint. The location points to the right parenthesis after the
    function arguments at the call site. The constraint is a mapping with keys format and value.
    We currently support only ACSL expressions of the form \result <op> <const_expression>,
    where <op> is one of ==, !=, <=, <, >, >= and <const_expression> is a constant expression.
    The value of format has to be acsl_expression.
  • branching:
    A requirement of this type says that a given branching is evaluated in a given way.
    The location points to a branching keyword like if, while, switch, or to the character ?
    in the ternary operator (?:). The constraint is then a mapping with only one key value.
    For binary branchings, value can be either true or false saying whether the true branch
    is used or not. For the keyword switch, value holds an integer constant or default. The
    integer constant specifies the value of the controlling expression of the switch statement.
    The value default says that the value of this expression does not match any case of the
    switch with the potential exception of the default case.

An assumption waypoint is evaluated at the sequence point
immediately before the waypoint location. The waypoint is passed if
the given constraint evaluates to true. A branching waypoint
is evaluated at the sequence point immediately after evaluation of the
controlling expression of the corresponding branching statement. The
waypoint is passed if the resulting value of the controlling
expression corresponds to the given constraint. A
function_enter waypoint is evaluated at the sequence point
immediately after evaluation of all arguments of the function
call. The waypoint is passed without any additional constraint. A
function_return waypoint is evaluated immediately after
evaluation of the corresponding function call. The waypoint is passed
if the returned value satisfies the given constraint.

root root items content content items segment segment items waypoint type
Type: enum (of string)

Must be one of:

  • "assumption"
  • "target"
  • "function_enter"
  • "function_return"
  • "branching"

root root items content content items segment segment items waypoint constraint
Type: object

The constraint of the waypoint.
A constraint is not allowed for type target.

root root items content content items segment segment items waypoint constraint value
Type: string or integer

root root items content content items segment segment items waypoint constraint format
Type: enum (of string)

Must be one of:

  • "c_expression"
  • "acsl_expression"

root root items content content items segment segment items waypoint location
Type: object

The location is a mapping with mandatory keys file_name and line.
All other keys are optional.

If the location provides an inconsistent information
(e.g., identifier specifies a function that is not called at the given column on the given line ),
the witness is syntactically invalid.

root root items content content items segment segment items waypoint location file_name
Type: string

The name of the file of the location.

root root items content content items segment segment items waypoint location line
Type: integer

The line number pf the program location in the file.

Value must be greater or equal to 1

root root items content content items segment segment items waypoint location column
Type: integer

The key column specifies the column number of the location,
i.e., the position of the column-th character in the line that the location points to
(value 1 is the position of the first character).
If the column is not given, then it is interpreted as the leftmost suitable position on the line,
where suitability is given by type.

Value must be greater or equal to 1

root root items content content items segment segment items waypoint location function
Type: string

The key function gives the name of the function containing the location.
It is usually determined by the file_name and line, but the information can improve human readability of the witness.

root root items content content items segment segment items waypoint action
Type: enum (of string)

Action follow means that the waypoint should be passed through.
Action avoid means that the waypoint should be avoided.

Must be one of:

  • "follow"
  • "avoid"