DATA)The alarms are counted after being grouped by these categories
alarmCategory::=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_alignment | "pointer_alignment" |
Unaligned pointer computation |
| shift | "shift" |
Invalid shift |
| overflow | "overflow" |
Integer overflow or downcast |
| 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 |
| float_to_int | "float_to_int" |
Overflow in float to int conversion |
| other | "other" |
Any other alarm |
GET)Registered tags for the above type.
input
::=null
output
::=tag[]
DATA)Statuses count.
statusesEntry::={"valid":number ,"unknown":number ,"invalid":number}
DATA)Alarm count for each alarm category.
alarmEntry::={"category":alarmCategory,"count":number}
DATA)Statistics about an Eva analysis.
programStatsType::={"progFunCoverage":{"reachable":number ,"dead":number},"progStmtCoverage":{"reachable":number ,"dead":number},"progAlarms":alarmEntry[],"evaEvents":{"errors":number ,"warnings":number},"kernelEvents":{"errors":number ,"warnings":number},"alarmsStatuses":statusesEntry,"assertionsStatuses":statusesEntry,"precondsStatuses":statusesEntry}
STATE)Statistics about the last Eva analysis for the whole program
SIGNAL)Signal for state programStats
GET)Getter for state programStats
input
::=null
output
::=programStatsType
ARRAY)Statistics about the last Eva analysis for each function
SIGNAL)Signal for array functionStats
DATA)Data for array rows functionStats
functionStatsData::= {fields…}
| Field | Format | Description |
|---|---|---|
"key" |
decl |
Entry identifier. |
"fctName" |
string | Function name |
"coverage" |
{
"reachable" : number ,
"dead" : number
} |
Coverage of the Eva analysis |
"alarmCount" |
alarmEntry
[] |
Alarms raised by the Eva analysis by category |
"alarmStatuses" |
statusesEntry |
Alarms statuses emitted by the Eva analysis |
GET)Data fetcher for array functionStats
input
::=number
output
::={output…}
| Output | Format | Description |
|---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
decl
[] |
removed entries |
"updated" |
functionStatsData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET)Force full reload for array functionStats
input
::=null
output
::=null
ARRAY)Data for flamegraph: execution times by callstack
SIGNAL)Signal for array flamegraph
DATA)Data for array rows flamegraph
flamegraphData::= {fields…}
| Field | Format | Description |
|---|---|---|
"key" |
$flamegraph |
Entry identifier. |
"stackNames" |
string
[] |
Callstack as functions name list, starting from main |
"nbCalls" |
number | Number of times the callstack has been analyzed |
"selfTime" |
number | Computation time for the callstack itself |
"totalTime" |
number | Total computation time, including functions called |
"kfDecl" |
decl |
Declaration of the top function |
GET)Data fetcher for array flamegraph
input
::=number
output
::={output…}
| Output | Format | Description |
|---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
$flamegraph
[] |
removed entries |
"updated" |
flamegraphData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET)Force full reload for array flamegraph
input
::=null
output
::=null