Safe Haskell	Safe-Inferred
Language	Haskell2010

Crux.SVCOMP.Witness

Description

This module defines a data type for SV-COMP witness automatons, as specified in https://github.com/sosy-lab/sv-witnesses.

Synopsis

data Witness = Witness {
- witnessType :: WitnessType
- witnessSourceCodeLang :: SourceCodeLang
- witnessProducer :: String
- witnessSpecification :: String
- witnessProgramFile :: FilePath
- witnessProgramHash :: ByteString
- witnessArchitecture :: Arch
- witnessCreationTime :: ZonedTime
- witnessNodes :: [WitnessNode]
- witnessEdges :: [WitnessEdge]
}
data WitnessNode = WitnessNode {
- nodeId :: Id
- nodeEntry :: Maybe Bool
- nodeSink :: Maybe Bool
- nodeViolation :: Maybe Bool
- nodeInvariant :: Maybe String
- nodeInvariantScope :: Maybe String
}
data WitnessEdge = WitnessEdge {
- edgeSource :: Id
- edgeTarget :: Id
- edgeAssumption :: Maybe Assumption
- edgeAssumptionScope :: Maybe String
- edgeAssumptionResultFunction :: Maybe String
- edgeControl :: Maybe Control
- edgeStartLine :: Maybe Int
- edgeEndLine :: Maybe Int
- edgeStartOffset :: Maybe Int
- edgeEndOffset :: Maybe Int
- edgeEnterLoopHead :: Maybe Bool
- edgeEnterFunction :: Maybe String
- edgeReturnFromFunction :: Maybe String
- edgeThreadId :: Maybe String
- edgeCreateThread :: Maybe String
- edgeStartColumn :: Maybe Int
}
data WitnessType
- = CorrectnessWitness
- | ViolationWitness
data SourceCodeLang
- = C
- | Java
data Control
- = ConditionTrue
- | ConditionFalse
data GraphMLAttrType
- = Boolean
- | Int
- | Long
- | Float
- | Double
- | String
mkNode :: Int -> WitnessNode
mkNodeId :: Int -> Id
mkEdge :: Int -> Int -> WitnessEdge
ppWitness :: Witness -> String

Documentation

data Witness Source #

A witness automaton. Adheres to the format specified in https://github.com/sosy-lab/sv-witnesses/tree/a592b52c4034423d42bed2059addbc6d8f1fa443#data-elements.

Constructors

Witness
Fields witnessType :: WitnessType witnessSourceCodeLang :: SourceCodeLang witnessProducer :: String witnessSpecification :: String witnessProgramFile :: FilePath witnessProgramHash :: ByteString witnessArchitecture :: Arch witnessCreationTime :: ZonedTime witnessNodes :: [WitnessNode] witnessEdges :: [WitnessEdge]

Instances

Instances details

Show Witness Source #
Instance details Defined in Crux.SVCOMP.Witness Methods showsPrec :: Int -> Witness -> ShowS # show :: Witness -> String # showList :: [Witness] -> ShowS #
Node Witness Source #
Instance details Defined in Crux.SVCOMP.Witness Methods node :: QName -> Witness -> Element #

data WitnessNode Source #

Constructors

WitnessNode
Fields nodeId :: Id nodeEntry :: Maybe Bool nodeSink :: Maybe Bool nodeViolation :: Maybe Bool nodeInvariant :: Maybe String nodeInvariantScope :: Maybe String

Instances

Instances details

Show WitnessNode Source #
Instance details Defined in Crux.SVCOMP.Witness Methods showsPrec :: Int -> WitnessNode -> ShowS # show :: WitnessNode -> String # showList :: [WitnessNode] -> ShowS #
Node WitnessNode Source #
Instance details Defined in Crux.SVCOMP.Witness Methods node :: QName -> WitnessNode -> Element #

data WitnessEdge Source #

Constructors

WitnessEdge

Fields

edgeSource :: Id
edgeTarget :: Id
edgeAssumption :: Maybe Assumption
edgeAssumptionScope :: Maybe String
edgeAssumptionResultFunction :: Maybe String
edgeControl :: Maybe Control
edgeStartLine :: Maybe Int
edgeEndLine :: Maybe Int
edgeStartOffset :: Maybe Int
edgeEndOffset :: Maybe Int
edgeEnterLoopHead :: Maybe Bool
edgeEnterFunction :: Maybe String
edgeReturnFromFunction :: Maybe String
edgeThreadId :: Maybe String
edgeCreateThread :: Maybe String
edgeStartColumn :: Maybe Int

Instances

Instances details

Show WitnessEdge Source #
Instance details Defined in Crux.SVCOMP.Witness Methods showsPrec :: Int -> WitnessEdge -> ShowS # show :: WitnessEdge -> String # showList :: [WitnessEdge] -> ShowS #
Node WitnessEdge Source #
Instance details Defined in Crux.SVCOMP.Witness Methods node :: QName -> WitnessEdge -> Element #

data WitnessType Source #

Constructors

CorrectnessWitness
ViolationWitness

Instances

Instances details

Show WitnessType Source #
Instance details Defined in Crux.SVCOMP.Witness Methods showsPrec :: Int -> WitnessType -> ShowS # show :: WitnessType -> String # showList :: [WitnessType] -> ShowS #

data SourceCodeLang Source #

Constructors

C
Java

Instances

Instances details

Show SourceCodeLang Source #
Instance details Defined in Crux.SVCOMP.Witness Methods showsPrec :: Int -> SourceCodeLang -> ShowS # show :: SourceCodeLang -> String # showList :: [SourceCodeLang] -> ShowS #

data Control Source #

Constructors

ConditionTrue
ConditionFalse

Instances

Instances details

Show Control Source #
Instance details Defined in Crux.SVCOMP.Witness Methods showsPrec :: Int -> Control -> ShowS # show :: Control -> String # showList :: [Control] -> ShowS #

data GraphMLAttrType Source #

Constructors

Boolean
Int
Long
Float
Double
String

Instances

Instances details

Show GraphMLAttrType Source #
Instance details Defined in Crux.SVCOMP.Witness Methods showsPrec :: Int -> GraphMLAttrType -> ShowS # show :: GraphMLAttrType -> String # showList :: [GraphMLAttrType] -> ShowS #

mkNode :: Int -> WitnessNode Source #

mkNodeId :: Int -> Id Source #

mkEdge :: Int -> Int -> WitnessEdge Source #

ppWitness :: Witness -> String Source #