Module dev.civl.mc

Package dev.civl.mc.semantics.IF

Interface LibraryEvaluator

public interface LibraryEvaluator

A Library Evaluator provides a method to "evaluate" the guard of each system function call. 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 enabler is: "Lib" + library name + "Evaluator". For example, the stdio library enabler is implemented as the class dev.civl.mc.library.stdio.LibstdioEnabler.

Method Summary

Modifier and Type	Method	Description
Evaluation	evaluateGuard(CIVLSource source, State state, int pid, String function, Expression[] arguments)	Evaluates the guard of a system function.
void	setPrimaryEvaluator(Evaluator primaryEvaluator)

Method Details

evaluateGuard

Evaluation evaluateGuard(CIVLSource source,
 State state,
 int pid,
 String function,
 Expression[] arguments)
                  throws UnsatisfiablePathConditionException

Evaluates the guard of a system function. This is an extra guard related to the particular system function, and needs to be checked in addition to the "regular" guard in the transition system.

Parameters:

source - The source code information for error report.

state - The state where the evaluation happens.

pid - The PID of the process that triggers this evaluation.

function - The name of the function.

arguments - The arguments of the function.

Returns:

The result of the guard with a possibly new state caused by side effects.

Throws:

UnsatisfiablePathConditionException

setPrimaryEvaluator

void setPrimaryEvaluator(Evaluator primaryEvaluator)

Parameters:

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