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
)Function names
fct
::=
$fct
DATA
)Localizable AST markers
marker
::=
$marker
DATA
)Location: function and marker
ARRAY
)Marker attributes
SIGNAL
)Signal for array markerAttributes
DATA
)Data for array rows markerAttributes
markerAttributesData
::= {
fields…}
Field | Format | Description |
---|---|---|
"marker" |
marker |
Entry identifier. |
"labelKind" |
string | Marker kind (short) |
"titleKind" |
string | Marker kind (long) |
"name" |
string | Marker short name or identifier when relevant. |
"descr" |
string | Marker declaration or description |
"isLval" |
boolean | Whether it is an l-value |
"isFunction" |
boolean | Whether it is a function symbol |
"isFunctionPointer" |
boolean | Whether it is a function pointer |
"isFunDecl" |
boolean | Whether it is a function declaration |
"scope" (opt.) |
string | Function scope of the marker, if applicable |
"sloc" (opt.) |
source |
Source location |
GET
)Data fetcher for array markerAttributes
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
marker
[] |
removed entries |
"updated" |
markerAttributesData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET
)Force full reload for array markerAttributes
input
::=
null
output
::=
null
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
signals
kernel.ast.changed
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? |
"extern" (opt.) |
boolean | Is the function extern? |
"sloc" |
source |
Source location |
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 |
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 ,"title"
:
string ,"descr"
:
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]
GET
)Get the currently analyzed source file names
input
::=
null
output
::=
string[]
SET
)Set the source file names to analyze.
input
::=
string[]
output
::=
null
GET
)Parse a C expression and returns the associated marker
input
::=
{
input…}
output
::=
marker
Input | Format | Description |
---|---|---|
"stmt" |
marker |
Marker position from where to localize the term |
"term" |
string | ACSL term to parse |
GET
)Parse a C lvalue and returns the associated marker
input
::=
{
input…}
output
::=
marker
Input | Format | Description |
---|---|---|
"stmt" |
marker |
Marker position from where to localize the term |
"term" |
string | ACSL term to parse |