Module dev.civl.mc

Package dev.civl.mc.model.IF

Enum Class CIVLException.Certainty

java.lang.Object

java.lang.Enum<CIVLException.Certainty>

dev.civl.mc.model.IF.CIVLException.Certainty

All Implemented Interfaces:

Serializable, Comparable<CIVLException.Certainty>, Constable

Enclosing class:

CIVLException

public static enum CIVLException.Certainty
extends Enum<CIVLException.Certainty>

A certainty level gages how certain we are that this is error is a real error, i.e., not just a spurious error. There are 3 levels, from highest to lowest level of certainty.

Nested Class Summary

Nested classes/interfaces inherited from class java.lang.Enum

Enum.EnumDesc<E extends Enum<E>>

Enum Constant Summary

Enum Constants

Enum Constant	Description
CONCRETE	A concrete trace verifies this is an error: the highest level of certainty that this represents a real error in the program being analyzed.
MAYBE	The prover is not sure whether this is an error.
NONE	Probably an internal CIVL error: the theorem prover hasn't said anything.
PROVEABLE	A theorem prover says this is an error: second-highest level of certainty.

Method Summary

Modifier and Type	Method	Description
static CIVLException.Certainty	valueOf(String name)	Returns the enum constant of this class with the specified name.
static CIVLException.Certainty[]	values()	Returns an array containing the constants of this enum class, in the order they are declared.

Methods inherited from class java.lang.Enum

clone, compareTo, describeConstable, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Enum Constant Details

CONCRETE

public static final CIVLException.Certainty CONCRETE

A concrete trace verifies this is an error: the highest level of certainty that this represents a real error in the program being analyzed.

PROVEABLE

public static final CIVLException.Certainty PROVEABLE

A theorem prover says this is an error: second-highest level of certainty. However no conrete trace has been produced to verify the theorem prover's claim.

MAYBE

public static final CIVLException.Certainty MAYBE

The prover is not sure whether this is an error. It could be due to the incompleteness of the decision procecure, or it could be a real error.

NONE

public static final CIVLException.Certainty NONE

Probably an internal CIVL error: the theorem prover hasn't said anything. The lowest level of certaintly that this represents a real error in the program being analyzed.

Method Details

values

public static CIVLException.Certainty[] values()

Returns an array containing the constants of this enum class, in the order they are declared.

Returns:

an array containing the constants of this enum class, in the order they are declared

valueOf

public static CIVLException.Certainty valueOf(String name)

Returns the enum constant of this class with the specified name. The string must match exactly an identifier used to declare an enum constant in this class. (Extraneous whitespace characters are not permitted.)

Parameters:

name - the name of the enum constant to be returned.

Returns:

the enum constant with the specified name

Throws:

IllegalArgumentException - if this enum class has no constant with the specified name

NullPointerException - if the argument is null