EXEC
)Ensures that AST is computed
input
::=
null
output
::=
null
SIGNAL
)Emitted when the AST has been changed
DATA
)Source file positions.
source
::=
{
"dir"
:
string ,"base"
:
string ,"file"
:
string ,"line"
:
number}
DATA
)Marker kind
markerKind
::=
tags…
Tags | Value | Description |
---|---|---|
Expression | "expression" |
Expression |
Lvalue | "lvalue" |
Lvalue |
Declaration | "declaration" |
Declaration |
Statement | "statement" |
Statement |
Global | "global" |
Global |
Term | "term" |
Term |
Property | "property" |
Property |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
DATA
)Marker variable
markerVar
::=
tags…
Tags | Value | Description |
---|---|---|
None | "none" |
None |
Variable | "variable" |
Variable |
Function | "function" |
Function |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
ARRAY
)Marker information
SIGNAL
)Signal for array markerInfo
DATA
)Data for array rows markerInfo
markerInfoData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
string | Entry identifier. |
"kind" |
markerKind |
Marker kind |
"var" |
markerVar |
Marker variable |
"name" |
string | Marker short name |
"descr" |
string | Marker declaration or description |
"sloc" |
source |
Source location |
GET
)Data fetcher for array markerInfo
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"pending" |
number | remaining entries to be fetched |
"updated" |
markerInfoData
[] |
updated entries |
"removed" |
string
[] |
removed entries |
"reload" |
boolean | array fully reloaded |
GET
)Force full reload for array markerInfo
input
::=
null
output
::=
null
DATA
)Localizable AST markers
marker
::=
#stmt
|#decl
|#lval
|#expr
|#term
|#global
|#property
DATA
)Location: function and marker
location
::= {
fields…}
Field | Format | Description |
---|---|---|
"fct" |
#fct |
Function |
"marker" |
marker |
Marker |
GET
)Get the current ‘main’ function.
input
::=
null
output
::=
#fct
?
GET
)Collect all functions in the AST
input
::=
null
output
::=
#fct
[]
GET
)Print the AST of a function
input
::=
#fct
output
::=
text
ARRAY
)AST Functions
SIGNAL
)Signal for array functions
DATA
)Data for array rows functions
functionsData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
#functions |
Entry identifier. |
"name" |
string | Name |
"signature" |
string | Signature |
"main" (opt.) |
boolean | Is the function the main entry point |
"defined" (opt.) |
boolean | Is the function defined? |
"stdlib" (opt.) |
boolean | Is the function from the Frama-C stdlib? |
"builtin" (opt.) |
boolean | Is the function a Frama-C builtin? |
"sloc" |
source |
Source location |
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 |
GET
)Force full reload for array functions
input
::=
null
output
::=
null
SIGNAL
)Updated AST information
GET
)Get available information about markers. When no marker is
given, returns all kinds of information (with empty
descr
field).
input
::=
marker
?
output
::=
{
"id"
:
string ,"label"
:
string ,"descr"
:
string ,"title"
:
string ,"text"
:
text
}
[]
signals
kernel.ast.getInformationUpdate
GET
)Returns the marker and function at a source file position, if any. Input: file path, line and column.
input
::=
[
string , number , number]
output
::=
[
#fct
?
,marker
?
]
GET
)Get the currently analyzed source file names
input
::=
null
output
::=
string[]
SET
)Set the source file names to analyze.
input
::=
string[]
output
::=
null
DATA
)
markerFromTermInput
::= {
fields…}
Field | Format | Description |
---|---|---|
"atStmt" |
marker |
The statement at which we will build the marker. |
"term" |
string | The ACSL term. |
GET
)Build a marker from an ACSL term.
input
::=
markerFromTermInput
output
::=
marker
?