Crux.Report

Documentation

generateReport :: CruxOptions -> CruxSimulationResult -> IO ()

maybeGenerateSource :: CruxOptions -> [FilePath] -> IO ()

provedGoalLocs :: ProvedGoals -> [ProgramLoc]

Return a list of all program locations referenced in a set of proved goals.

provedGoalTraces :: ProvedGoals -> Seq (Seq ProgramLoc)

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 Branches, which mirror the branching structure of the program execution that led to each individual ProvedGoal or NotProvedGoal.

provedGoalFiles :: ProvedGoals -> Set FilePath

Return a list of all files referenced in a set of proved goals.

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]