Eva General Services

plugins.eva.general.computationStateType (DATA)

State of the computation of Eva Analysis.

computationStateType ::= "not_computed" | "computing" | "computed" | "aborted"

plugins.eva.general.computationState (STATE)

The current computation state of the analysis.

plugins.eva.general.signalComputationState (SIGNAL)

Signal for state computationState

plugins.eva.general.getComputationState (GET)

Getter for state computationState

input ::= null

output ::= computationStateType

plugins.eva.general.CallSite (DATA)

Call site, combining function and stmt

CallSite ::= { "kf" : fct , "stmt" : marker }

plugins.eva.general.getCallers (GET)

Get the list of call site of a function

input ::= fct

output ::= CallSite []

signals

plugins.eva.general.getCallees (GET)

Return the functions pointed to by a function pointer

input ::= marker

output ::= fct []

signals

plugins.eva.general.functions (ARRAY)

AST Functions

plugins.eva.general.signalFunctions (SIGNAL)

Signal for array functions

plugins.eva.general.functionsData (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

plugins.eva.general.fetchFunctions (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

plugins.eva.general.reloadFunctions (GET)

Force full reload for array functions

input ::= null

output ::= null

plugins.eva.general.deadCode (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.

plugins.eva.general.getDeadCode (GET)

Get the lists of unreachable and of non terminating statements in a function

input ::= fct

output ::= deadCode

signals

plugins.eva.general.taintStatus (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

plugins.eva.general.taintStatusTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

plugins.eva.general.LvalueTaints (DATA)

Lvalue taint status

LvalueTaints ::= { fields… }

Field Format Description
"lval" marker tainted lvalue
"taint" taintStatus taint status

plugins.eva.general.taintedLvalues (GET)

Get the tainted lvalues of a given function

input ::= fct

output ::= LvalueTaints []

signals

plugins.eva.general.properties (ARRAY)

Status of Registered Properties

plugins.eva.general.signalProperties (SIGNAL)

Signal for array properties

plugins.eva.general.propertiesData (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?

plugins.eva.general.fetchProperties (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

plugins.eva.general.reloadProperties (GET)

Force full reload for array properties

input ::= null

output ::= null

plugins.eva.general.alarmCategory (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

plugins.eva.general.alarmCategoryTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

plugins.eva.general.statusesEntry (DATA)

Statuses count.

statusesEntry ::= { "valid" : number , "unknown" : number , "invalid" : number }

plugins.eva.general.alarmEntry (DATA)

Alarm count for each alarm category.

alarmEntry ::= { "category" : alarmCategory , "count" : number }

plugins.eva.general.programStatsType (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 }

plugins.eva.general.programStats (STATE)

Statistics about the last Eva analysis for the whole program

plugins.eva.general.signalProgramStats (SIGNAL)

Signal for state programStats

plugins.eva.general.getProgramStats (GET)

Getter for state programStats

input ::= null

output ::= programStatsType

plugins.eva.general.functionStats (ARRAY)

Statistics about the last Eva analysis for each function

plugins.eva.general.signalFunctionStats (SIGNAL)

Signal for array functionStats

plugins.eva.general.functionStatsData (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

plugins.eva.general.fetchFunctionStats (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

plugins.eva.general.reloadFunctionStats (GET)

Force full reload for array functionStats

input ::= null

output ::= null

plugins.eva.general.getStates (GET)

Get the domain states about the given marker

input ::= [ marker , boolean ]

output ::= [ string , string , string ] []

signals