Loop invariants are important building blocks in software verification. Many verification approaches use loop invariants as lemmata to construct proofs of correctness.
A loop invariant should hold at various locations:
1. before the loop,
2. in the beginning of the loop body,
3. at the end of the loop body,
4. after the loop.
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
"loop_invariant" Information that identifies the entry and describes the context of its production.
Version of the format of the entry.
Specific value:"0.1" Date and time in ISO8601 format when the entry (not the file) was created.
Producer of the entry.
Name of the producer.
Version of the producer.
Configuration of the producer. Should be used to distinguish different configurations of the same version of the producer.
Additional description about the producer. Could be used for any information that does not fit into any of the other producer properties.
Bash-compliant command line used to produce the entry. Should be used to improve reproducibility.
Verification task for which the entry was produced.
Files belonging to the verification task that were given as input to the producer.
Bash-compliant file name pattern, which must represent exactly one file.
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
Type: stringSHA-256 hash.
Must match regular expression:[0-9a-fA-F]{64} Data model to be assumed for the task.
Source language of the input files.
C
Java
Location in the source code where the loop invariant holds.
As the loop invariant has stronger semantics than a single location invariant, it does not correspond to an assertion at a single location. Therefore, this location should be such that a validator is able to associate it with a particular loop, for example, by placing the loop invariant immediately before the loop.
Name of the file. Must be present in task.input_files.
SHA-256 hash of the file.
Must match regular expression:[0-9a-fA-F]{64} Line in the file (starting with 1).
Value must be greater or equal to 1
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
Name of the surrounding function.
The loop invariant description.
The invariant itself.
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.Format of string. The following values are supported:
C: Expression in C language.Invariant at a program location, which does not necessarily correspond to a loop.
entry_type: location_invariant
metadata:
format_version: 0.1
uuid: 92c380d6-00a1-4e97-8c63-0f246206c6ab
creation_time: '2022-05-16T11:56:13.480Z'
producer:
name: A2Y
version: '1'
task:
input_files:
- c/loops/trex04.c
input_file_hashes:
c/loops/trex04.c: f70ffe9cd45c37f44e9e780e31340fab45b6a2fb7f7ef23a2d90faf4241229d6
specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
data_model: ILP32
language: C
location:
file_name: c/loops/trex04.c
file_hash: f70ffe9cd45c37f44e9e780e31340fab45b6a2fb7f7ef23a2d90faf4241229d6
line: 47
column: 0
function: main
location_invariant:
string: x <= 0
type: assertion
format: C
"location_invariant" Information that identifies the entry and describes the context of its production.
Version of the format of the entry.
Specific value:"0.1" Date and time in ISO8601 format when the entry (not the file) was created.
Producer of the entry.
Name of the producer.
Version of the producer.
Configuration of the producer. Should be used to distinguish different configurations of the same version of the producer.
Additional description about the producer. Could be used for any information that does not fit into any of the other producer properties.
Bash-compliant command line used to produce the entry. Should be used to improve reproducibility.
Verification task for which the entry was produced.
Files belonging to the verification task that were given as input to the producer.
Bash-compliant file name pattern, which must represent exactly one file.
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
Type: stringSHA-256 hash.
Must match regular expression:[0-9a-fA-F]{64} Data model to be assumed for the task.
Source language of the input files.
C
Java
Location in the source code where the invariant holds.
Name of the file. Must be present in task.input_files.
SHA-256 hash of the file.
Must match regular expression:[0-9a-fA-F]{64} Line in the file (starting with 1).
Value must be greater or equal to 1
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
Name of the surrounding function.
The invariant description.
The invariant itself.
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.Format of string. The following values are supported:
C: Expression in C language.Invariant certificates document validation attempts of various invariants, for example by trying to use the target loop invariant in a proof of correctness.
Certificates document correctness and trustworthiness of invariants.
entry_type: 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
"invariant_certificate" Information that identifies the certificate entry and describes the context of its production.
Version of the format of the certificate entry.
Specific value:"0.1" Date and time in ISO8601 format when the certificate entry (not the file or target entry) was created.
Producer of the certificate entry.
Name of the producer.
Version of the producer.
Configuration of the producer. Should be used to distinguish different configurations of the same version of the producer.
Additional description about the producer. Could be used for any information that does not fit into any of the other producer properties.
Bash-compliant command line used to produce the entry. Should be used to improve reproducibility.
Target entry of some invariant type which is being certified.
Unique identifier of the target entry.
entry_type of the target entry.
SHA-256 hash of the target file.
Must match regular expression:[0-9a-fA-F]{64} The invariant certification result description.
The certification result itself.
Interpretation of string. The following values are supported:
verdict: Verdict about the targeted entry.Format of string. The following values are supported:
confirmed | rejected: Either "confirmed" or "rejected".Declares and initializes a ghost variable used in this witness. Ghost variables can be updated at specific points during the execution of the program, and may be referred to in location invariants and other witness entries, unless otherwise specified.
entry_type: ghost_variable
metadata:
format_version: 0.1
uuid: ee9cc5a7-2f8d-43c2-bcac-cde6f5b6d048
creation_time: '2023-07-07T17:17:17.000Z'
producer:
name: Ultimate GemCutter
version: 0.2.3-dev
task:
input_files:
- ghosts.c
input_file_hashes:
ghosts.c: 2b56726d10d5a52c002223c251596e534cc0842633245a85ece0f2a6f854bd14
specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
data_model: ILP32
language: C
variable: g
scope: global
type: int
initial: '0'
"ghost_variable" Information that identifies the entry and describes the context of its production.
Version of the format of the entry.
Specific value:"0.1" Date and time in ISO8601 format when the entry (not the file) was created.
Producer of the entry.
Name of the producer.
Version of the producer.
Configuration of the producer. Should be used to distinguish different configurations of the same version of the producer.
Additional description about the producer. Could be used for any information that does not fit into any of the other producer properties.
Bash-compliant command line used to produce the entry. Should be used to improve reproducibility.
Verification task for which the entry was produced.
Files belonging to the verification task that were given as input to the producer.
Bash-compliant file name pattern, which must represent exactly one file.
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
Type: stringSHA-256 hash.
Must match regular expression:[0-9a-fA-F]{64} Data model to be assumed for the task.
Source language of the input files.
C
Java
A valid identifier used as name of the ghost variable. This identifier must be unique across the witness, and must not be used in the program.
Must match regular expression:[_a-zA-Z][_a-zA-Z0-9]* The scope of the ghost variable. For now, only global ghost variables are supported.
A C type, either built-in or declared in the program.
A syntactically well-formed C 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; this evaluation must not lead to undefined behaviour.
Updates the value of a ghost variable used in this witness. Ghost variables can be updated at specific points during the execution of the program, and may be referred to in location invariants and other witness entries, unless otherwise specified.
entry_type: ghost_update
metadata:
format_version: 0.1
uuid: dc7c0b90-d998-4920-b9a0-af8a9f058875
creation_time: '2023-07-07T17:17:17.000Z'
producer:
name: Ultimate GemCutter
version: 0.2.3-dev
task:
input_files:
- ghosts.c
input_file_hashes:
ghosts.c: 2b56726d10d5a52c002223c251596e534cc0842633245a85ece0f2a6f854bd14
specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
data_model: ILP32
language: C
variable: g
expression: '5'
location:
file_name: ghosts.c
file_hash: 511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c
line: 22
column: 0
function: main
branching:
constraint:
value: true
"ghost_update" Information that identifies the entry and describes the context of its production.
Version of the format of the entry.
Specific value:"0.1" Date and time in ISO8601 format when the entry (not the file) was created.
Producer of the entry.
Name of the producer.
Version of the producer.
Configuration of the producer. Should be used to distinguish different configurations of the same version of the producer.
Additional description about the producer. Could be used for any information that does not fit into any of the other producer properties.
Bash-compliant command line used to produce the entry. Should be used to improve reproducibility.
Verification task for which the entry was produced.
Files belonging to the verification task that were given as input to the producer.
Bash-compliant file name pattern, which must represent exactly one file.
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
Type: stringSHA-256 hash.
Must match regular expression:[0-9a-fA-F]{64} Data model to be assumed for the task.
Source language of the input files.
C
Java
The identifier for the updated ghost variable. This variable must be declared in an entry of type ghost_variable in the witness.
Must match regular expression:[_a-zA-Z][_a-zA-Z0-9]* A syntactically well-formed C 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 (see below), 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 however that the evaluation is performed atomically, i.e., by assumption the evaluation does not cause a data race.
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 exiting the location.
Name of the file. Must be present in task.input_files.
SHA-256 hash of the file.
Must match regular expression:[0-9a-fA-F]{64} Line in the file (starting with 1).
Value must be greater or equal to 1
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
Name of the surrounding function.
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.