Module dev.civl.mc

Package dev.civl.mc.model.IF.contract

Interface ContractFactory

public interface ContractFactory

This factory is to create new instances of function contract components.

Method Summary

Modifier and Type	Method	Description
DependsEvent	newAnyactEvent(CIVLSource source)	Creates a new instance of \anyact event
CallEvent	newCallEvent(CIVLSource source, CIVLFunction function, List<Expression> arguments)	Creates a new instance of call event.
CompositeEvent	newCompositeEvent(CIVLSource source, CompositeEvent.CompositeEventOperator op, DependsEvent left, DependsEvent right)	Creates a new instance of composite event.
FunctionBehavior	newFunctionBehavior(CIVLSource source)	Creates a new function behavior.
FunctionContract	newFunctionContract(CIVLSource source, Scope scope)	Creates a new function contract.
MemoryEvent	newMemoryEvent(CIVLSource source, DependsEvent.DependsEventKind kind, Set<Expression> memoryUnits)	Creates a new instance of memory event of the given kind.
NamedFunctionBehavior	newNamedFunctionBehavior(CIVLSource source, String name)	Creates a new named function behavior
DependsEvent	newNoactEvent(CIVLSource source)	Creates a new instance of \noact event

Method Details

newFunctionBehavior

FunctionBehavior newFunctionBehavior(CIVLSource source)

Creates a new function behavior.

Parameters:

source - the source of the function behavior

Returns:

newNamedFunctionBehavior

NamedFunctionBehavior newNamedFunctionBehavior(CIVLSource source,
 String name)

Creates a new named function behavior

Parameters:

source -

name -

Returns:

newFunctionContract

FunctionContract newFunctionContract(CIVLSource source,
 Scope scope)

Creates a new function contract.

Parameters:

source -

Returns:

newCallEvent

CallEvent newCallEvent(CIVLSource source,
 CIVLFunction function,
 List<Expression> arguments)

Creates a new instance of call event.

Parameters:

function -

arguments -

Returns:

newCompositeEvent

CompositeEvent newCompositeEvent(CIVLSource source,
 CompositeEvent.CompositeEventOperator op,
 DependsEvent left,
 DependsEvent right)

Creates a new instance of composite event.

Parameters:

source -

op -

right -

Returns:

newMemoryEvent

MemoryEvent newMemoryEvent(CIVLSource source,
 DependsEvent.DependsEventKind kind,
 Set<Expression> memoryUnits)

Creates a new instance of memory event of the given kind.

Parameters:

source -

kind - the kind of this memory event, which could be either READ, WRITE or REACH.

memoryUnits -

Returns:

newAnyactEvent

DependsEvent newAnyactEvent(CIVLSource source)

Creates a new instance of \anyact event

Parameters:

source -

Returns:

newNoactEvent

DependsEvent newNoactEvent(CIVLSource source)

Creates a new instance of \noact event

Parameters:

source -

Returns: