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

Marker kind

markerKind ::= tags…

Tags Value Description
Expression "expression" Expression
Lvalue "lvalue" Lvalue
Declaration "declaration" Declaration
Statement "statement" Statement
Global "global" Global
Term "term" Term
Property "property" Property

kernel.ast.markerKindTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

kernel.ast.markerVar (DATA)

Marker variable

markerVar ::= tags…

Tags Value Description
None "none" None
Variable "variable" Variable
Function "function" Function

kernel.ast.markerVarTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

kernel.ast.markerInfo (ARRAY)

Marker information

kernel.ast.signalMarkerInfo (SIGNAL)

Signal for array markerInfo

kernel.ast.markerInfoData (DATA)

Data for array rows markerInfo

markerInfoData ::= { fields… }

Field Format Description
"key" string Entry identifier.
"kind" markerKind Marker kind
"var" markerVar Marker variable
"name" string Marker short name
"descr" string Marker declaration or description
"sloc" source Source location

kernel.ast.fetchMarkerInfo (GET)

Data fetcher for array markerInfo

input ::= number

output ::= { output… }

Output Format Description
"pending" number remaining entries to be fetched
"updated" markerInfoData [] updated entries
"removed" string [] removed entries
"reload" boolean array fully reloaded

kernel.ast.reloadMarkerInfo (GET)

Force full reload for array markerInfo

input ::= null

output ::= null

kernel.ast.marker (DATA)

Localizable AST markers

marker ::= #stmt | #decl | #lval | #expr | #term | #global | #property

kernel.ast.location (DATA)

Location: function and marker

location ::= { fields… }

Field Format Description
"fct" #fct Function
"marker" marker Marker

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

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?
"sloc" source Source location

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

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 , "descr" : string , "title" : 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.markerFromTermInput (DATA)

input

markerFromTermInput ::= { fields… }

Field Format Description
"atStmt" marker The statement at which we will build the marker.
"term" string The ACSL term.

kernel.ast.markerFromTerm (GET)

Build a marker from an ACSL term.

input ::= markerFromTermInput

output ::= marker ?