DATA
)Property Kinds
propKind
::=
tags…
Tags | Value | Description |
---|---|---|
behavior | "behavior" |
Contract behavior |
complete | "complete" |
Complete behaviors clause |
disjoint | "disjoint" |
Disjoint behaviors clause |
assumes | "assumes" |
Clause @assumes |
requires | "requires" |
Function precondition |
instance | "instance" |
Instance of a precondition at a call site |
breaks | "breaks" |
Clause @breaks |
continues | "continues" |
Clause @continues |
returns | "returns" |
Clause @returns |
exits | "exits" |
Clause @exits |
ensures | "ensures" |
Function postcondition |
terminates | "terminates" |
Function termination clause |
allocates | "allocates" |
Function allocation |
decreases | "decreases" |
Clause @decreases |
assigns | "assigns" |
Function assigns |
froms | "froms" |
Functional dependencies in function assigns |
assert | "assert" |
Assertion |
check | "check" |
Check |
admit | "admit" |
Hypothesis |
loop_invariant | "loop_invariant" |
Clause
@loop invariant |
loop_assigns | "loop_assigns" |
Clause
@loop assigns |
loop_variant | "loop_variant" |
Clause
@loop variant |
loop_allocates | "loop_allocates" |
Clause
@loop allocates |
loop_pragma | "loop_pragma" |
Clause
@loop pragma |
reachable | "reachable" |
Reachable statement |
code_contract | "code_contract" |
Statement contract |
code_invariant | "code_invariant" |
Generalized loop invariant |
type_invariant | "type_invariant" |
Type invariant |
global_invariant | "global_invariant" |
Global invariant |
axiomatic | "axiomatic" |
Axiomatic definitions |
axiom | "axiom" |
Logical axiom |
lemma | "lemma" |
Logical lemma |
check_lemma | "check_lemma" |
Logical check lemma |
extension | "extension" |
ACSL extension |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
DATA
)Property Status (consolidated)
propStatus
::=
tags…
Tags | Value | Description |
---|---|---|
Unknown | "unknown" |
Unknown status |
Never tried | "never_tried" |
Unknown status (never tried) |
Inconsistent | "inconsistent" |
Inconsistent status |
Valid | "valid" |
Valid property |
Valid (?) | "valid_under_hyp" |
Valid (under hypotheses) |
Valid (!) | "considered_valid" |
Valid (external assumption) |
Invalid | "invalid" |
Invalid property (counter example found) |
Invalid (?) | "invalid_under_hyp" |
Invalid property (under hypotheses) |
Invalid (✝) | "invalid_but_dead" |
Dead property (but invalid) |
Valid (✝) | "valid_but_dead" |
Dead property (but valid) |
Unknown (✝) | "unknown_but_dead" |
Dead property (but unknown) |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
DATA
)Alarm Kinds
alarms
::=
tags…
Tags | Value | Description |
---|---|---|
division_by_zero | "division_by_zero" |
Integer division by zero |
mem_access | "mem_access" |
Invalid pointer dereferencing |
index_bound | "index_bound" |
Array access out of bounds |
pointer_value | "pointer_value" |
Invalid pointer computation |
shift | "shift" |
Invalid shift |
ptr_comparison | "ptr_comparison" |
Invalid pointer comparison |
differing_blocks | "differing_blocks" |
Operation on pointers within different blocks |
overflow | "overflow" |
Integer overflow or downcast |
float_to_int | "float_to_int" |
Overflow in float to int conversion |
separation | "separation" |
Unsequenced side-effects on non-separated memory |
overlap | "overlap" |
Overlap between left- and right-hand-side in assignment |
initialization | "initialization" |
Uninitialized memory read |
dangling_pointer | "dangling_pointer" |
Read of a dangling pointer |
is_nan_or_infinite | "is_nan_or_infinite" |
Non-finite (nan or infinite) floating-point value |
is_nan | "is_nan" |
NaN floating-point value |
function_pointer | "function_pointer" |
Pointer to a function with non-compatible type |
bool_value | "bool_value" |
Trap representation of a _Bool lvalue |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
ARRAY
)Status of Registered Properties
SIGNAL
)Signal for array status
DATA
)Data for array rows status
statusData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
marker |
Entry identifier. |
"descr" |
string | Full description |
"kind" |
propKind |
Kind |
"names" |
string
[] |
Names |
"status" |
propStatus |
Status |
"fct" (opt.) |
fct |
Function |
"kinstr" (opt.) |
marker |
Instruction |
"source" |
source |
Position |
"alarm" (opt.) |
string | Alarm name (if the property is an alarm) |
"alarm_descr"
(opt.) |
string | Alarm description (if the property is an alarm) |
"predicate" (opt.) |
string | Predicate |
GET
)Data fetcher for array status
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
marker
[] |
removed entries |
"updated" |
statusData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET
)Force full reload for array status
input
::=
null
output
::=
null