Ast Services

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.

kernel.ast.compute (EXEC)

Ensures that AST is computed

input ::= null

output ::= null

kernel.ast.changed (SIGNAL)

Emitted when the AST has been changed

kernel.ast.source (DATA)

Source file positions.

source ::= { "dir" : string , "base" : string , "file" : string , "line" : number }

kernel.ast.decl (DATA)

AST Declarations markers

decl ::= $decl

kernel.ast.marker (DATA)

Localizable AST markers

marker ::= $marker

kernel.ast.declKind (DATA)

Declaration kind

declKind ::= $ENUM | $UNION | $STRUCT | $TYPEDEF | $GLOBAL | $FUNCTION | $LFUNPRED | $INVARIANT | $AXIOMATIC | $MODULE | $LEMMA | $EXTENSION | $VOLATILE | $LTYPE | $MODEL

kernel.ast.declAttributes (ARRAY)

Declaration attributes

kernel.ast.signalDeclAttributes (SIGNAL)

Signal for array declAttributes

kernel.ast.declAttributesData (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

kernel.ast.fetchDeclAttributes (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

kernel.ast.reloadDeclAttributes (GET)

Force full reload for array declAttributes

input ::= null

output ::= null

kernel.ast.printDeclaration (GET)

Prints an AST Declaration

input ::= decl

output ::= text

signals

kernel.ast.markerKind (DATA)

Marker kind

markerKind ::= $STMT | $LFUN | $DFUN | $LVAR | $DVAR | $LVAL | $EXP | $TERM | $TYPE | $PROPERTY | $DECLARATION

kernel.ast.markerAttributes (ARRAY)

Marker attributes

kernel.ast.signalMarkerAttributes (SIGNAL)

Signal for array markerAttributes

kernel.ast.markerAttributesData (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

kernel.ast.fetchMarkerAttributes (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

kernel.ast.reloadMarkerAttributes (GET)

Force full reload for array markerAttributes

input ::= null

output ::= null

kernel.ast.getMainFunction (GET)

Get the current ‘main’ function.

input ::= null

output ::= decl ?

kernel.ast.getFunctions (GET)

Collect all functions in the AST

input ::= null

output ::= decl []

kernel.ast.functions (ARRAY)

AST Functions

kernel.ast.signalFunctions (SIGNAL)

Signal for array functions

kernel.ast.functionsData (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

kernel.ast.fetchFunctions (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

kernel.ast.reloadFunctions (GET)

Force full reload for array functions

input ::= null

output ::= null

kernel.ast.globals (ARRAY)

AST global variables

kernel.ast.signalGlobals (SIGNAL)

Signal for array globals

kernel.ast.globalsData (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

kernel.ast.fetchGlobals (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

kernel.ast.reloadGlobals (GET)

Force full reload for array globals

input ::= null

output ::= null

kernel.ast.getInformationUpdate (SIGNAL)

Updated AST information

kernel.ast.getInformation (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.getMarkerAt (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.getFiles (GET)

Get the currently analyzed source file names

input ::= null

output ::= string []

kernel.ast.setFiles (SET)

Set the source file names to analyze.

input ::= string []

output ::= null

kernel.ast.parseExpr (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

kernel.ast.parseLval (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