Dive Services

plugins.dive.range (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

plugins.dive.explorationWindow (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

plugins.dive.nodeId (DATA)

A node identifier in the graph

nodeId ::= number

plugins.dive.callsite (DATA)

callsite

callsite ::= { "fun" : string , "instr" : number | "global" }

plugins.dive.callstack (DATA)

The callstack context for a node

callstack ::= callsite []

plugins.dive.nodeLocality (DATA)

The description of a node locality

nodeLocality ::= { fields… }

Field Format Description
"file" string file
"callstack" (opt.) callstack callstack

plugins.dive.nodeKind (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

plugins.dive.nodeKindTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

plugins.dive.taint (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

plugins.dive.taintTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

plugins.dive.exploration (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

plugins.dive.explorationTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

plugins.dive.nodeSpecialRange (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

plugins.dive.nodeSpecialRangeTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

plugins.dive.nodeRange (DATA)

A qualitative or quantitative description of the range of values that this node can take.

nodeRange ::= number | nodeSpecialRange

plugins.dive.node (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" location [] writes
"values" (opt.) string values
"range" nodeRange range
"type" (opt.) string type
"taint" (opt.) taint taint

plugins.dive.dependency (DATA)

The dependency between two nodes

dependency ::= { fields… }

Field Format Description
"id" number id
"src" nodeId src
"dst" nodeId dst
"dkind" string dkind
"origins" location [] origins

plugins.dive.element (DATA)

A graph element, either a node or a dependency

element ::= node | dependency

plugins.dive.graph (ARRAY)

The graph being built as a set of vertices and edges

plugins.dive.signalGraph (SIGNAL)

Signal for array graph

plugins.dive.graphData (DATA)

Data for array rows graph

graphData ::= { fields… }

Field Format Description
"key" $graph Entry identifier.
"element" element a graph element

plugins.dive.fetchGraph (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

plugins.dive.reloadGraph (GET)

Force full reload for array graph

input ::= null

output ::= null

plugins.dive.window (SET)

Set the exploration window

input ::= explorationWindow

output ::= null

plugins.dive.clear (EXEC)

Erase the graph and start over with an empty one

input ::= null

output ::= null

plugins.dive.add (EXEC)

Add a node to the graph

input ::= marker

output ::= nodeId ?

plugins.dive.explore (EXEC)

Explore the graph starting from an existing vertex

input ::= nodeId

output ::= null

plugins.dive.show (EXEC)

Show the dependencies of an existing vertex

input ::= nodeId

output ::= null

plugins.dive.hide (EXEC)

Hide the dependencies of an existing vertex

input ::= nodeId

output ::= null