Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 7e0a0bff20
Fetching contributors…

Cannot retrieve contributors at this time

file 154 lines (131 sloc) 4.371 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | A test suite to check for basic functionality.

module Main where

import System.Directory ( removeDirectoryRecursive
                        , doesDirectoryExist
                        , doesFileExist
                        , removeFile )
import qualified Copilot.Compile.C99 as C99
import qualified Copilot.Compile.SBV as SBV
import qualified Copilot.Tools.CBMC as M
import Control.Monad (when, unless)
import Data.Maybe (catMaybes)

import AddMult
import Array
--import BadExtVars
import Cast
import ClockExamples
import EngineExample
import Examples
import Examples2
import ExtFuns
import Local
import LTLExamples
import PTLTLExamples
import Random
import RegExpExamples
import StackExamples
import StatExamples
import VotingExamples


--------------------------------------------------------------------------------

main :: IO ()
main = do
  ls <- checkExists
  when (null ls) runTests
  unless (null ls) $ do putStrLn "*** Warning! ***"
                        putStrLn "Cannot run tests in this directory. You have the following files or directories that would be deleted: "
                        mapM_ putStrLn ls
                                
runTests :: IO ()
runTests = do
  cleanup
  putStrLn "Testing addMult ..."
  addMult >> cleanup
  putStrLn ""
  putStrLn "Testing array ..."
  array >> cleanup
  putStrLn ""
-- putStrLn "Testing badExtVars ..."
-- badExtVars >> cleanup
  putStrLn ""
  putStrLn "Testing castEx ..."
  castEx >> cleanup
  putStrLn ""
  putStrLn "Testing clockExamples ..."
  clockExamples >> cleanup
  putStrLn ""
  putStrLn "Testing engineExample ..."
  engineExample >> cleanup
  putStrLn ""
  putStrLn "Testing examples ..."
  examples >> cleanup
  putStrLn ""
  putStrLn "Testing examples2 ..."
  examples2 >> cleanup
  putStrLn ""
  putStrLn "Testing extFuns ..."
  extFuns >> cleanup
  putStrLn ""
  putStrLn "Testing localEx ..."
  localEx >> cleanup
  putStrLn ""
  putStrLn "Testing ltlExamples ..."
  ltlExamples >> cleanup
  putStrLn ""
  putStrLn "Testing ptltlExamples ..."
  ptltlExamples >> cleanup
  putStrLn ""
  putStrLn "Testing randomEx ..."
  randomEx >> cleanup
  putStrLn ""
  putStrLn "Testing regExpExamples ..."
  regExpExamples >> cleanup
  putStrLn ""
  putStrLn "Testing stackExamples ..."
  stackExamples >> cleanup
  putStrLn ""
  putStrLn "Testing statExamples ..."
  statExamples >> cleanup
  putStrLn ""
  putStrLn "Testing votingExamples ..."
  votingExamples >> cleanup
  putStrLn ""
  putStrLn ""
  putStrLn "************************************"
  putStrLn " Ok, the basic tests passed. Enjoy!"
  putStrLn "************************************"

--------------------------------------------------------------------------------

cbmcName :: String
cbmcName = "cbmc_driver.c"

atomCBMC :: String
atomCBMC = M.appendPrefix M.atomPrefix C99.c99DirName

sbvCBMC :: String
sbvCBMC = M.appendPrefix M.sbvPrefix SBV.sbvDirName

--------------------------------------------------------------------------------

checkExists :: IO [String]
checkExists = do
  b0 <- nmBool doesDirectoryExist SBV.sbvDirName
  b1 <- nmBool doesDirectoryExist C99.c99DirName
  b2 <- nmBool doesFileExist cbmcName
  b3 <- nmBool doesDirectoryExist atomCBMC
  b4 <- nmBool doesDirectoryExist sbvCBMC
  return $ catMaybes $ map getName [b0, b1, b2, b3, b4]

  where
  getName (nm, bool) = if bool then Just nm else Nothing
  nmBool f nm = do b <- f nm
                   return (nm, b)

--------------------------------------------------------------------------------

cleanup :: IO ()
cleanup = do

  b0 <- doesDirectoryExist SBV.sbvDirName
  when b0 (removeDirectoryRecursive SBV.sbvDirName)

  b1 <- doesDirectoryExist C99.c99DirName
  when b1 (removeDirectoryRecursive C99.c99DirName)

  b2 <- doesFileExist cbmcName
  when b2 (removeFile cbmcName)

  b3 <- doesDirectoryExist atomCBMC
  when b3 (removeDirectoryRecursive atomCBMC)

  b4 <- doesDirectoryExist sbvCBMC
  when b4 (removeDirectoryRecursive sbvCBMC)

--------------------------------------------------------------------------------
Something went wrong with that request. Please try again.