Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- generateReport :: CruxOptions -> CruxSimulationResult -> IO ()
- maybeGenerateSource :: CruxOptions -> [FilePath] -> IO ()
- provedGoalLocs :: ProvedGoals -> [ProgramLoc]
- provedGoalTraces :: ProvedGoals -> Seq (Seq ProgramLoc)
- provedGoalFiles :: ProvedGoals -> Set FilePath
- renderSideConds :: CruxOptions -> [ProvedGoals] -> IO [JS]
- removeRepeats :: Eq a => [a] -> [a]
- removeRepeatsBy :: (a -> a -> Bool) -> [a] -> [a]
- jsPath :: [ProgramLoc] -> IO [JS]
- jsProvedGoal :: [ProgramLoc] -> [CrucibleAssumption (Const ())] -> SimError -> Bool -> IO [JS]
- jsNotProvedGoal :: [ProgramLoc] -> [CrucibleAssumption (Const ())] -> SimError -> Doc Void -> Maybe (ModelView, [CrucibleEvent GroundValueWrapper]) -> IO [JS]
Documentation
generateReport :: CruxOptions -> CruxSimulationResult -> IO () Source #
maybeGenerateSource :: CruxOptions -> [FilePath] -> IO () Source #
provedGoalLocs :: ProvedGoals -> [ProgramLoc] Source #
Return a list of all program locations referenced in a set of proved goals.
provedGoalTraces :: ProvedGoals -> Seq (Seq ProgramLoc) Source #
Return a list of all of the traces referenced in a set of proved goals.
This returns a sequence-of-sequences because a single ProvedGoals
can
involve many Branch
es, which mirror the branching structure of the program
execution that led to each individual ProvedGoal
or NotProvedGoal
.
provedGoalFiles :: ProvedGoals -> Set FilePath Source #
Return a list of all files referenced in a set of proved goals.
renderSideConds :: CruxOptions -> [ProvedGoals] -> IO [JS] Source #
removeRepeats :: Eq a => [a] -> [a] Source #
removeRepeatsBy :: (a -> a -> Bool) -> [a] -> [a] Source #
jsProvedGoal :: [ProgramLoc] -> [CrucibleAssumption (Const ())] -> SimError -> Bool -> IO [JS] Source #
jsNotProvedGoal :: [ProgramLoc] -> [CrucibleAssumption (Const ())] -> SimError -> Doc Void -> Maybe (ModelView, [CrucibleEvent GroundValueWrapper]) -> IO [JS] Source #