DATA
)State of the computation of Eva Analysis.
computationStateType
::=
"not_computed"
|"computing"
|"computed"
|"aborted"
STATE
)The current computation state of the analysis.
SIGNAL
)Signal for state computationState
GET
)Getter for state computationState
input
::=
null
output
::=
computationStateType
DATA
)Call site, combining function and stmt
GET
)Get the list of call site of a function
input
::=
fct
output
::=
CallSite
[]
signals
plugins.eva.general.signalComputationState
GET
)Return the functions pointed to by a function pointer
input
::=
marker
output
::=
fct
[]
signals
plugins.eva.general.signalComputationState
ARRAY
)AST Functions
SIGNAL
)Signal for array functions
DATA
)Data for array rows functions
functionsData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
#functions |
Entry identifier. |
"eva_analyzed"
(opt.) |
boolean | Has the function been analyzed by Eva |
GET
)Data fetcher for array functions
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"pending" |
number | remaining entries to be fetched |
"updated" |
functionsData
[] |
updated entries |
"removed" |
#functions
[] |
removed entries |
"reload" |
boolean | array fully reloaded |
GET
)Force full reload for array functions
input
::=
null
output
::=
null
DATA
)Unreachable and non terminating statements.
deadCode
::= {
fields…}
Field | Format | Description |
---|---|---|
"unreachable" |
marker
[] |
List of unreachable statements. |
"nonTerminating" |
marker
[] |
List of reachable but non terminating statements. |
GET
)Get the lists of unreachable and of non terminating statements in a function
input
::=
fct
output
::=
deadCode
signals
plugins.eva.general.signalComputationState
DATA
)Taint status of logical properties
taintStatus
::=
tags…
Tags | Value | Description |
---|---|---|
"not_computed" |
Not computed: the Eva taint domain has not been enabled, or the Eva analysis has not been run | |
Error | "error" |
Error: the memory zone on which this property depends could not be computed |
— | "not_applicable" |
Not applicable: no taint for this kind of property |
Tainted (direct) | "direct_taint" |
Direct taint: this property is related to a memory location that can be affected by an attacker |
Tainted (indirect) | "indirect_taint" |
Indirect taint: this property is related to a memory location whose assignment depends on path conditions that can be affected by an attacker |
Untainted | "not_tainted" |
Untainted property: this property is safe |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
DATA
)Lvalue taint status
LvalueTaints
::= {
fields…}
Field | Format | Description |
---|---|---|
"lval" |
marker |
tainted lvalue |
"taint" |
taintStatus |
taint status |
GET
)Get the tainted lvalues of a given function
input
::=
fct
output
::=
LvalueTaints
[]
signals
plugins.eva.general.signalComputationState
ARRAY
)Status of Registered Properties
SIGNAL
)Signal for array properties
DATA
)Data for array rows properties
propertiesData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
marker |
Entry identifier. |
"priority" |
boolean | Is the property invalid in some context of the analysis? |
"taint" |
taintStatus |
Is the property tainted according to the Eva taint domain? |
GET
)Data fetcher for array properties
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"pending" |
number | remaining entries to be fetched |
"updated" |
propertiesData
[] |
updated entries |
"removed" |
marker
[] |
removed entries |
"reload" |
boolean | array fully reloaded |
GET
)Force full reload for array properties
input
::=
null
output
::=
null
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 |
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" |
fct |
Entry identifier. |
"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 |
---|---|---|
"pending" |
number | remaining entries to be fetched |
"updated" |
functionStatsData
[] |
updated entries |
"removed" |
fct
[] |
removed entries |
"reload" |
boolean | array fully reloaded |
GET
)Force full reload for array functionStats
input
::=
null
output
::=
null
GET
)Get the domain states about the given marker
input
::=
[
marker
, boolean]
output
::=
[
string , string , string]
[]
signals
plugins.eva.general.signalComputationState