Module dev.civl.mc

Package dev.civl.mc.log.IF

Class CIVLErrorLogger

java.lang.Object

dev.civl.gmc.ErrorLog

dev.civl.mc.log.IF.CIVLErrorLogger

public class CIVLErrorLogger
extends dev.civl.gmc.ErrorLog

CIVLErrorLogger logs all errors of the system.

Constructor Summary

Constructors

Constructor	Description
CIVLErrorLogger(File directory, String sessionName, PrintStream out, CIVLConfiguration civlConfig, dev.civl.gmc.GMCConfiguration gmcConfig, StateFactory stateFactory, dev.civl.sarl.IF.SymbolicUniverse universe, boolean solve)	creates a new instance of error logger.

Method Summary

Modifier and Type	Method	Description
State	logError(CIVLSource source, State state, int pid, StringBuffer stateString, dev.civl.sarl.IF.expr.BooleanExpression claim, dev.civl.sarl.IF.ValidityResult.ResultType resultType, CIVLProperty property, String message)	Report a (possible) error detected in the course of evaluating an expression.
void	logSimpleError(CIVLSource source, State state, int pid, String process, StringBuffer stateString, CIVLProperty property, String message)	Checks whether the path condition is satisfiable and logs an error if it is (or might be).

Methods inherited from class dev.civl.gmc.ErrorLog

errorBound, getDirectory, getIgnoreErrors, getLogFile, getMinimalCounterexampleSize, getMinimize, numEntries, numErrors, print, report, save, searcher, setErrorBound, setIgnoreErrors, setMinimize, setSearcher

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

CIVLErrorLogger

public CIVLErrorLogger(File directory,
 String sessionName,
 PrintStream out,
 CIVLConfiguration civlConfig,
 dev.civl.gmc.GMCConfiguration gmcConfig,
 StateFactory stateFactory,
 dev.civl.sarl.IF.SymbolicUniverse universe,
 boolean solve)

creates a new instance of error logger.

Parameters:

directory -

sessionName -

out -

universe -

solve -

config -

Method Details

logError

public State logError(CIVLSource source,
 State state,
 int pid,
 StringBuffer stateString,
 dev.civl.sarl.IF.expr.BooleanExpression claim,
 dev.civl.sarl.IF.ValidityResult.ResultType resultType,
 CIVLProperty property,
 String message)
               throws UnsatisfiablePathConditionException

Report a (possible) error detected in the course of evaluating an expression. This is the method that should normally be used for logging, reporting, and recovering from errors.

This is the general protocol for checking conditions and reporting and recovering from errors: first, check some condition holds and call the result of that check "condsat", which may be YES, NO, or MAYBE. If condsat is YES, proceed. Otherwise, there is a problem and you should call this method.

This method first checks the satisfiability of the path condition, call the result "pcsat". Logs a violation with certainty determined as follows:

• pcsat=YES invalid input: '&'invalid input: '&' condsat=NO : certainty=PROVEABLE
• pcsat=YES invalid input: '&'invalid input: '&' condsat=MAYBE : certainty=MAYBE
• pcsat=MAYBE invalid input: '&'invalid input: '&' condsat=NO : certainty=MAYBE
• pcsat=MAYBE invalid input: '&'invalid input: '&' condsat=MAYBE : certainty=MAYBE
• pcsat=NO: no error to report

Returns the state obtained by adding the claim to the pc of the given state.

Parameters:

source - the source of the expression being evaluated

state - the state in which the evaluation is taking place

stateString - a string representation of the state which is used in CIVLExecutionException that is recorded in the log

claim - the boolean expression which was expected to hold. This should already have been checked for validity before invoking this method. The result of that check should not have been "YES" (i.e., definitely valid); that is why you are calling this method

resultType - the result of evaluating the validity of the claim (which you did before you called this method).

property - the kind of error you want to report if it turns out there is an error

message - the message you want to include in the error report if it turns out there is an error

process - a string representation of the process that is evaluating the expression; used for reporting errors

Returns:

the state obtained by adding the claim to the pc of the given state.

Throws:

UnsatisfiablePathConditionException - if it turns out the path condition is unsatisfiable; in this case no error will be reported since the current path is infeasible

logSimpleError

public void logSimpleError(CIVLSource source,
 State state,
 int pid,
 String process,
 StringBuffer stateString,
 CIVLProperty property,
 String message)
                    throws UnsatisfiablePathConditionException

Checks whether the path condition is satisfiable and logs an error if it is (or might be). If the path condition is definitely unsatisfiable, there is no error to log, and an UnsatisfiablePathConditionException is thrown.

Parameters:

source - source code element used to report the error

state - the current state in which the possible error is detected

process - the process name, i.e, "p"+process identifier

stateString - the string representation of state where the error occurs

message - the message to include in the error report

civlProp - the kind of error (e.g., DEREFERENCE)

Throws:

UnsatisfiablePathConditionException - if the path condition is definitely unsatisfiable