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.compute (EXEC)

run eva analysis

input ::= null

output ::= null

plugins.eva.general.abort (GET)

abort eva analysis

input ::= null

output ::= null

plugins.eva.general.clear (SET)

removes all results from previous Eva analyses, including emitted alarms, annotations and statuses

input ::= null

output ::= null

plugins.eva.general.CallSite (DATA)

Callee function and caller stmt

CallSite ::= { "call" : decl , "stmt" : marker }

plugins.eva.general.getCallers (GET)

Get the list of call sites for a function

input ::= decl

output ::= CallSite []

signals

plugins.eva.general.getCallees (GET)

Return the functions pointed to by a function pointer

input ::= marker

output ::= decl []

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
"reload" boolean array fully reloaded
"removed" $functions [] removed entries
"updated" functionsData [] updated entries
"pending" number remaining entries to be fetched

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
"reached" marker [] List of statements reached by the analysis.
"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 ::= decl

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 ::= decl

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
"reload" boolean array fully reloaded
"removed" marker [] removed entries
"updated" propertiesData [] updated entries
"pending" number remaining entries to be fetched

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
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

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" 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

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

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

plugins.eva.general.flamegraph (ARRAY)

Data for flamegraph: execution times by callstack

plugins.eva.general.signalFlamegraph (SIGNAL)

Signal for array flamegraph

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

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

plugins.eva.general.reloadFlamegraph (GET)

Force full reload for array flamegraph

input ::= null

output ::= null