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