Schema Docs

One of

Loop invariant
Loop invariant certificate

Type: object

Loop invariants are important building blocks in software verification. Many verification approaches use loop invariants as lemmata to construct proofs of correctness.

Example:

entry_type: loop_invariant
metadata:
  format_version: 0.1
  uuid: 91023a0f-9f45-4385-88c4-1152ade45537
  creation_time: '2021-05-05T13:18:43.000Z'
  producer:
    name: CPAchecker
    version: 2.0.1-svn
    configuration: svcomp21--04-kInduction
  task:
    input_files:
    - multivar_1-1.c
    input_file_hashes:
      multivar_1-1.c: 511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c
    specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
    data_model: ILP32
    language: C
location:
  file_name: multivar_1-1.c
  file_hash: 511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c
  line: 22
  column: 0
  function: main
loop_invariant:
  string: (x >= 1024U) && (x <= 4294967295U) && (y == x)
  type: assertion
  format: C

root root items oneOf Loop invariant entry_type

Type: const
Specific value: "loop_invariant"

root root items oneOf Loop invariant metadata

Type: object

Information that identifies the entry and describes the context of its production.

root root items oneOf Loop invariant metadata format_version

Type: const

Version of the format of the entry.

Specific value: "0.1"

root root items oneOf Loop invariant metadata uuid

Type: string

Unique identifier of the entry (RFC4122 defines the UUID format).

root root items oneOf Loop invariant metadata creation_time

Type: stringFormat: date-time

Date and time in ISO8601 format when the entry (not the file) was created.

root root items oneOf Loop invariant metadata producer

Type: object

Producer of the entry.

root root items oneOf Loop invariant metadata producer name

Type: string

Name of the producer.

root root items oneOf Loop invariant metadata producer version

Type: string

Version of the producer.

root root items oneOf Loop invariant metadata producer configuration

Type: string

Configuration of the producer. Should be used to distinguish different configurations of the same version of the producer.

root root items oneOf Loop invariant metadata producer description

Type: string

Additional description about the producer. Could be used for any information that does not fit into any of the other producer properties.

root root items oneOf Loop invariant metadata producer command_line

Type: string

Bash-compliant command line used to produce the entry. Should be used to improve reproducibility.

root root items oneOf Loop invariant metadata task

Type: object

Verification task for which the entry was produced.

root root items oneOf Loop invariant metadata task input_files

Type: array of string

Files belonging to the verification task that were given as input to the producer.

Each item of this array must be:

root root items oneOf Loop invariant metadata task input_files input_files items

Type: string

Bash-compliant file name pattern, which must represent exactly one file.

root root items oneOf Loop invariant metadata task input_file_hashes

Type: object

SHA-256 hashes of each file in input_files. Every file name pattern listed in input_files must appear as a key.

Each additional property must conform to the following schema

root root items oneOf Loop invariant metadata task input_file_hashes hash

Type: string

SHA-256 hash.

Must match regular expression: [0-9a-fA-F]{64}

root root items oneOf Loop invariant metadata task specification

Type: string

Specification in SV-COMP format against which the verification is done.

root root items oneOf Loop invariant metadata task data_model

Type: enum (of string)

Data model to be assumed for the task.

Must be one of:

"ILP32"
"LP64"

root root items oneOf Loop invariant metadata task language

Type: string

Source language of the input files.

Examples:

Java

root root items oneOf Loop invariant location

Type: object

Location in the source code where the loop invariant holds.

root root items oneOf Loop invariant location file_name

Type: string

Name of the file. Must be present in task.input_files.

root root items oneOf Loop invariant location file_hash

Type: string

SHA-256 hash of the file.

Must match regular expression: [0-9a-fA-F]{64}

root root items oneOf Loop invariant location line

Type: integer

Line in the file (starting with 1).

Value must be greater or equal to 1

root root items oneOf Loop invariant location column

Type: integer

Column in the file (starting with 0). Column 0 refers to the very beginning of the line (before any characters).

Value must be greater or equal to 0

root root items oneOf Loop invariant location function

Type: string

Name of the surrounding function.

root root items oneOf Loop invariant loop_invariant

Type: object

The loop invariant description.

root root items oneOf Loop invariant loop_invariant string

Type: string

The invariant itself.

root root items oneOf Loop invariant loop_invariant type

Type: enum (of string)

Interpretation of string. The following values are supported:

assertion: Assertion, e.g. assert(<string>) in C, inserted at the specified location. The insertion is hypothetical and doesn't affect other locations.

Must be one of:

"assertion"

root root items oneOf Loop invariant loop_invariant format

Type: enum (of string)

Format of string. The following values are supported:

C: Expression in C language.

Must be one of:

root root items oneOf Loop invariant certificate

Type: object

Loop invariant certificates document validation attempts of loop invariants, for example by trying to use the target loop invariant in a proof of correctness.

Certificates document correctness and trustworthiness of invariants.

Example:

entry_type: loop_invariant_certificate
metadata:
  format_version: 0.1
  uuid: 954affa9-32e4-4b35-85ae-888da3a6a53b
  creation_time: '2021-05-05T13:18:43.000Z'
  producer:
    name: CPAchecker
    version: 2.0.1-svn
    configuration: svcomp21--04-kInduction
target:
  uuid: 91023a0f-9f45-4385-88c4-1152ade45537
  type: loop-invariant
  file_hash: 511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c
certification:
  string: confirmed
  type: verdict
  format: confirmed | rejected