Module dev.civl.mc

Package dev.civl.mc.semantics.IF

Interface LibraryExecutor

public interface LibraryExecutor

A Library Executor provides the semantics for system functions defined in a library. It provides a method to "execute" each system library function.A new library is implemented in the package named as "dev.civl.mc.library." (

invalid reference

CommonLibraryLoader#CLASS_PREFIX

) + library name. And the class name of the executor is: "Lib" + library name + "Enabler". For example, the stdio library executor is implemented as the class dev.civl.mc.library.stdio.LibstdioExecutor.

Method Summary

Modifier and Type	Method	Description
Evaluation	execute(State state, int pid, CallOrSpawnStatement statement, String functionName)	Executes the given call statement for a certain process at the given state.
void	setEvaluator(Evaluator evaluator)

Method Details

execute

Evaluation execute(State state,
 int pid,
 CallOrSpawnStatement statement,
 String functionName)
            throws UnsatisfiablePathConditionException

Executes the given call statement for a certain process at the given state.

Precondition: the given call statement is enabled for the process with the given pid, and the function of the call statement is provided by this library.

Parameters:

state - The state where the call statement is to be executed.

pid - The PID of the process that the statement belongs to.

statement - The call statement to be executed.

functionName - The name of the system function that this call is going to executed. Note: we need this when the function of the call statement is a function pointer.

Returns:

The resulting state after executing the call statement, plus the return value of the function call, which is NULL if the function returns void.

Throws:

UnsatisfiablePathConditionException

setEvaluator

void setEvaluator(Evaluator evaluator)

Parameters:

evaluator - the Evaluator that will be used by this library executor after setting