Detailed Description

TESLA intermediate representation (Protocol Buffers).

Definition in file tesla.proto.

Classes
struct	tesla::ManifestFile
	A file that describes TESLA automata. More...

struct	tesla::Usage
	How an automaton is used for instrumentation. More...

struct	tesla::AutomatonDescription
	An inline assertion describing the temporal behaviour of software. More...

struct	tesla::Identifier
	Something that uniquely identifies an automaton. More...

struct	tesla::Location
	An identifier for an automaton based on where it was defined. More...

struct	tesla::Expression
	A temporal expression. More...

struct	tesla::BooleanExpr
	A boolean combination of expressions (with equal precedence). More...

struct	tesla::Sequence
	A sequence of temporal events. More...

struct	tesla::NowEvent
	Execution has reached the point in the instrumented code where an inline assertion was defined. More...

struct	tesla::FunctionEvent
	A function has been called or has returned. More...

struct	tesla::FunctionEvent::CallKind

struct	tesla::FunctionRef
	A function that can be instrumented. More...

struct	tesla::FieldAssignment
	Assignment to a field in a structure. More...

struct	tesla::StructField
	A field within a structure. More...

struct	tesla::Argument
	An argument to a function. More...

Class Documentation

struct tesla::ManifestFile

Collaboration diagram for tesla::ManifestFile:

Class Members
repeated AutomatonDescription	automaton	All of the automata described by the manifest.
repeated Usage	root	The automata that are actually used in their own right (as opposed to those that are only included by other automata).

struct tesla::Usage

Collaboration diagram for tesla::Usage:

Class Members
optional Expression	beginning	Where the automaton begins: a bound, a place for initialisation.
optional Expression	end	Where the automataon ends: a bound, a place for cleanup.
required Identifier	identifier	The identifier of the automaton in question.

struct tesla::Identifier

Collaboration diagram for tesla::Identifier:

Class Members
optional Location	location	If there is no assigned name, the location the automaton is defined.
optional string	name	Programmer-assigned name.

struct tesla::Location

Collaboration diagram for tesla::Location:

struct tesla::Sequence

Collaboration diagram for tesla::Sequence:

Class Members
repeated Expression	expression

struct tesla::NowEvent

Collaboration diagram for tesla::NowEvent:

Class Members
required Location	location

struct tesla::FunctionEvent::CallKind

struct tesla::FunctionRef

Collaboration diagram for tesla::FunctionRef:

Class Members
required string	name	The function's name. TODO: we may need further disambiguation if two modules contain static functions with the same name. This may only matter when compiling via LLVM IR: I think this will fail when linking ELF object files.

struct tesla::StructField

Collaboration diagram for tesla::StructField:

Class Members
required Argument	base	Reference to the structure.
required int32	index	Index of the field within the struct.
required string	name	Name of the struct field.
required string	type	Name of the structure type.