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

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