Property Services

kernel.properties.propKind (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
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
module "module" Logic module
axiom "axiom" Logical axiom
lemma "lemma" Logical lemma
check_lemma "check_lemma" Logical check lemma
extension "extension" ACSL extension
generic "generic" Generic Property

kernel.properties.propKindTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

kernel.properties.propStatus (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)

kernel.properties.propStatusTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

kernel.properties.alarms (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

kernel.properties.alarmsTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

kernel.properties.status (ARRAY)

Status of Registered Properties

kernel.properties.signalStatus (SIGNAL)

Signal for array status

kernel.properties.statusData (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
"scope" (opt.) decl Declaration Scope
"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

kernel.properties.fetchStatus (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

kernel.properties.reloadStatus (GET)

Force full reload for array status

input ::= null

output ::= null