module Copilot.Compile.SBV.Makefile
( makefile
, makefileName
) where
import Copilot.Compile.SBV.Driver (driverName)
import Copilot.Compile.SBV.Params
import Text.PrettyPrint.HughesPJ
import qualified System.IO as I
import System.Directory
makefileName :: Params -> String
makefileName params = withPrefix (prefix params) "copilot" ++ ".mk"
makefile :: Params -> String -> String -> IO ()
makefile params dir sbvName = do
let filePath = dir ++ '/' : (makefileName params)
fileName = "copilot"
let wr doc = I.appendFile filePath ((mkStyle doc) ++ "\n")
wr (text "a")
removeFile filePath
wr (text "# Makefile rules for the Copilot driver.")
wr (text "\nCCFLAGS=-fnone \nCC=ccomp\nSHELL := /bin/bash")
wr (text "")
wr $ text "driver" <> colon
<+> text (driverName params) <+> text (withPre fileName) <> text ".h"
<+> archive
wr $ text "\t"
<> (hsep [ text "$" <> braces (text "CC")
, text "$" <> braces (text "CCFLAGS")
, text "$<"
, text "-o"
, text "$@"
, archive])
wr $ text "\nfval" <> colon
<+> text ("\n\tframa-c -val -main testing -slevel 10000000 *.h *.c | tee logval")
wr $ text "\nfwp" <> colon
<+> text ("\n\tparallel frama-c -wp -wp-out . -wp-timeout 20 -wp-prover CVC4 -wp-split {} ::: *.c | tee >logfwp >(grep 'Proved\\|Unknown\\|Timeout\\|Failed\\|Qed:\\s\\|CVC4:\\s\\|Parsing .*\\.c' > logfwpcompact) >(grep 'Proved\\|Qed:\\s\\|CVC4:\\s\\|Unknown\\|Timeout\\|Failed\\|Parsing .*\\.c')")
wr $ text "\nsplint" <> colon
<+> text ("\n\tsplint -comment-char % *.h *.c | tee logsplint")
where
archive = text sbvName <> text ".a"
withPre nm = withPrefix (prefix params) nm
mkStyle :: Doc -> String
mkStyle = renderStyle (style {lineLength = 80})