The Frama-C internal representation of source files need to be computed before being accessed. This generally involves preprocessing of sources and finally parsing, typechecking and normalization.
Although this step is generally performed silently on-demand
inside Frama-C, from the Server point of view, this is a
non-trivial procedure that should not be triggered
outside an EXEC
request.
Hence, most AST services might fail or return empty data if the AST has not been actually computed before. However, in typical usage of Frama-C from the command-line, the AST would have been computed just before any other plug-in, including the Server.
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 |
---|---|---|
"pending" |
number | remaining entries to be fetched |
"updated" |
markerAttributesData
[] |
updated entries |
"removed" |
marker
[] |
removed entries |
"reload" |
boolean | array fully reloaded |
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 |
---|---|---|
"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 ,"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 |
---|---|---|
"term" |
string | ACSL term to parse |
"stmt" |
marker |
Marker position from where to localize the term |