DATA
)Parametrization of the exploration range.
range
::= {
fields…}
Field | Format | Description |
---|---|---|
"backward" (opt.) |
number | range for the write dependencies |
"forward" (opt.) |
number | range for the read dependencies |
DATA
)Global parametrization of the exploration.
explorationWindow
::= {
fields…}
Field | Format | Description |
---|---|---|
"perception" |
range |
how far dive will explore from root nodes ; must be a finite range |
"horizon" |
range |
range beyond which the nodes must be hidden |
DATA
)A node identifier in the graph
nodeId
::=
number
DATA
)callsite
callsite
::=
{
"fun"
:
string ,"instr"
:
number |"global"
}
DATA
)The callstack context for a node
DATA
)The description of a node locality
nodeLocality
::= {
fields…}
Field | Format | Description |
---|---|---|
"file" |
string | file |
"callstack" (opt.) |
callstack |
callstack |
DATA
)The nature of a node
nodeKind
::=
tags…
Tags | Value | Description |
---|---|---|
Scalar | "scalar" |
a single memory cell |
Composite | "composite" |
a memory bloc containing cells |
Scattered | "scattered" |
a set of memory locations designated by an lvalue |
Unknown | "unknown" |
an unresolved memory location |
Alarm | "alarm" |
an alarm emitted by Frama-C |
Absolute | "absolute" |
a memory location designated by a range of adresses |
String | "string" |
a string literal |
Error | "error" |
a placeholder node when an error prevented the generation process |
Const | "const" |
a numeric constant literal |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
DATA
)Taint of a memory location
taint
::=
tags…
Tags | Value | Description |
---|---|---|
Untainted | "untainted" |
not tainted by anything |
Indirect | "indirect" |
tainted by control |
Direct | "direct" |
tainted by data |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
DATA
)The computation state of a node read or write dependencies
exploration
::=
tags…
Tags | Value | Description |
---|---|---|
Yes | "yes" |
all dependencies have been computed |
Partial | "partial" |
some dependencies have been explored |
No | "no" |
dependencies have not been computed |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
DATA
)A qualitative description of the range of values that this node can take.
nodeSpecialRange
::=
tags…
Tags | Value | Description |
---|---|---|
Empty | "empty" |
no value ever computed for this node |
Singleton | "singleton" |
this node can only have one value |
Wide | "wide" |
this node can take almost all values of its type |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
DATA
)A qualitative or quantitative description of the range of values that this node can take.
nodeRange
::=
number |nodeSpecialRange
DATA
)
node
::= {
fields…}
Field | Format | Description |
---|---|---|
"id" |
nodeId |
id |
"label" |
string | label |
"nkind" |
nodeKind |
nkind |
"locality" |
nodeLocality |
locality |
"is_root" |
boolean | is_root |
"backward_explored" |
exploration |
backward_explored |
"forward_explored" |
exploration |
forward_explored |
"writes" |
marker
[] |
writes |
"values" (opt.) |
string | values |
"range" |
nodeRange |
range |
"type" (opt.) |
string | type |
"taint" (opt.) |
taint |
taint |
DATA
)The dependency between two nodes
dependency
::= {
fields…}
Field | Format | Description |
---|---|---|
"id" |
number | id |
"src" |
nodeId |
src |
"dst" |
nodeId |
dst |
"dkind" |
string | dkind |
"origins" |
marker
[] |
origins |
DATA
)A graph element, either a node or a dependency
element
::=
node
|dependency
ARRAY
)The graph being built as a set of vertices and edges
SIGNAL
)Signal for array graph
DATA
)Data for array rows graph
graphData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
$graph |
Entry identifier. |
"element" |
element |
a graph element |
GET
)Data fetcher for array graph
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
$graph
[] |
removed entries |
"updated" |
graphData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET
)Force full reload for array graph
input
::=
null
output
::=
null
SET
)Set the exploration window
input
::=
explorationWindow
output
::=
null
EXEC
)Erase the graph and start over with an empty one
input
::=
null
output
::=
null
EXEC
)Add a node to the graph
input
::=
marker
output
::=
nodeId
?
EXEC
)Explore the graph starting from an existing vertex
input
::=
nodeId
output
::=
null
EXEC
)Show the dependencies of an existing vertex
input
::=
nodeId
output
::=
null
EXEC
)Hide the dependencies of an existing vertex
input
::=
nodeId
output
::=
null