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

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 ?