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
)AST Declarations markers
decl
::=
$decl
DATA
)Localizable AST markers
marker
::=
$marker
DATA
)Declaration kind
declKind
::=
$ENUM
|$UNION
|$STRUCT
|$TYPEDEF
|$GLOBAL
|$FUNCTION
ARRAY
)Declaration attributes
SIGNAL
)Signal for array declAttributes
DATA
)Data for array rows declAttributes
declAttributesData
::= {
fields…}
Field | Format | Description |
---|---|---|
"decl" |
decl |
Entry identifier. |
"kind" |
declKind |
Declaration kind |
"self" |
marker |
Declaration’s marker |
"name" |
string | Declaration identifier |
"label" |
string | Declaration label (uncapitalized kind & name) |
"source" |
source |
Source location |
GET
)Data fetcher for array declAttributes
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
decl [] |
removed entries |
"updated" |
declAttributesData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET
)Force full reload for array declAttributes
input
::=
null
output
::=
null
GET
)Prints an AST Declaration
input
::=
decl
output
::=
text
signals
kernel.ast.changed
DATA
)Marker kind
markerKind
::=
$STMT
|$LFUN
|$DFUN
|$LVAR
|$DVAR
|$LVAL
|$EXP
|$TERM
|$TYPE
|$PROPERTY
|$DECLARATION
ARRAY
)Marker attributes
SIGNAL
)Signal for array markerAttributes
DATA
)Data for array rows markerAttributes
markerAttributesData
::= {
fields…}
Field | Format | Description |
---|---|---|
"marker" |
marker |
Entry identifier. |
"kind" |
markerKind |
Marker kind (key) |
"scope" (opt.) |
decl |
Marker Scope (where it is printed in) |
"definition"
(opt.) |
marker |
Marker’s Target Definition (when applicable) |
"labelKind" |
string | Marker kind label |
"titleKind" |
string | Marker kind title |
"name" (opt.) |
string | Marker identifier (when applicable) |
"descr" |
string | Marker description |
"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
::=
decl
?
GET
)Collect all functions in the AST
input
::=
null
output
::=
decl
[]
ARRAY
)AST Functions
SIGNAL
)Signal for array functions
DATA
)Data for array rows functions
functionsData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
$functions |
Entry identifier. |
"decl" |
decl |
Declaration Tag |
"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
ARRAY
)AST global variables
SIGNAL
)Signal for array globals
DATA
)Data for array rows globals
globalsData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
$globals |
Entry identifier. |
"decl" |
decl |
Declaration Tag |
"name" |
string | Name |
"type" |
string | Type |
"stdlib" |
boolean | Is the variable from the Frama-C stdlib? |
"extern" |
boolean | Is the variable extern? |
"const" |
boolean | Is the variable const? |
"volatile" |
boolean | Is the variable volatile? |
"ghost" |
boolean | Is the variable ghost? |
"init" |
boolean | Is the variable explicitly initialized? |
"source" |
boolean | Is the variable in the source code? |
"sloc" |
source |
Source location |
GET
)Data fetcher for array globals
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
$globals
[] |
removed entries |
"updated" |
globalsData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET
)Force full reload for array globals
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. File can be empty, in case no marker is returned.
input
::=
{
input…}
output
::=
marker
?
Input | Format | Description |
---|---|---|
"file" |
string | File path |
"line" |
number | Line (1-based) |
"column" |
number | Column (0-based) |
signals
kernel.ast.changed
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 |