Ast Services

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.fct (DATA)

Function names

fct ::= $fct

kernel.ast.marker (DATA)

Localizable AST markers

marker ::= $marker

kernel.ast.location (DATA)

Location: function and marker

location ::= { "fct" : fct , "marker" : marker }

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.
"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

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 ::= fct ?

kernel.ast.getFunctions (GET)

Collect all functions in the AST

input ::= null

output ::= fct []

kernel.ast.printFunction (GET)

Print the AST of a function

input ::= fct

output ::= text

signals

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.
"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.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.

input ::= [ string , number , number ]

output ::= [ fct ? , marker ? ]

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