diff --git a/osek-verification.cabal b/osek-verification.cabal index 114370ca8dc06b69289fd0e733459ed480596f20..8935e78168c1650589a979e9095b166d72d0bc66 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -42,6 +42,7 @@ executable mockup_generator , text >= 1.2 && <1.3 , bytestring >= 0.10 && <0.11 , osek-verification + , optparse-applicative >= 0.12 && <0.13 hs-source-dirs: src/main default-language: Haskell2010 diff --git a/src/main/Main.hs b/src/main/Main.hs index bc78bc570a657c7e7ca703fe2b33268194e80088..0dc1e3c0676ac2a2a6a3510df719686238e6117b 100644 --- a/src/main/Main.hs +++ b/src/main/Main.hs @@ -4,7 +4,10 @@ module Main where import qualified Data.ByteString.Lazy as BS import qualified Data.Text.IO as T -import System.Environment +import qualified Data.Text as T +import Data.Text (Text) +import System.Environment +import Options.Applicative import qualified CFG.Parser as P import CFG.Graph @@ -14,17 +17,29 @@ import CFG.Sanitize import Search.States2Dot import Search.Search -main :: IO () -main = do - getArgs >>= \case - ["graph"] -> do - cntnt <- T.getContents - T.putStrLn $ states2Dot cntnt +data Command = Mockup | Search SearchOpts + +optParser :: Parser Command +optParser = subparser + ( command "mockup" (info (helper <*> pure Mockup) (progDesc "Generate mockup")) + <> command "search" (info (helper <*> (Search <$> searchOptParser)) + (progDesc "Extract CFG by running EXECUTABLE")) + ) - ["search", prog] -> do - driver prog +data SearchOpts = SearchOpts + { mockupExecutable :: FilePath + } - _ -> do +searchOptParser :: Parser SearchOpts +searchOptParser = SearchOpts <$> argument str (metavar "EXECUTABLE") + +main :: IO () +main = do + cmd <- execParser $ info (helper <*> optParser) + ( fullDesc <> progDesc "dOSEK verification tool" ) + case cmd of + (Search opts) -> driver (mockupExecutable opts) + Mockup -> do cntnt <- BS.getContents case P.parseFile cntnt of Left err -> putStrLn err