Minor code cleanup, squash some warnings

src/SAWScript/AutoMatch/LLVM.hs

@@ -31,7 +31,7 @@ getDeclsLLVM ::
   SharedContext ->
   LLVMModule ->
   IO (Interaction (Maybe [Decl]))
-getDeclsLLVM proxy sc (LLVMModule file mdl _) = do
+getDeclsLLVM _proxy _sc (LLVMModule file mdl _) = do
     let symStr (Symbol s) = s
     return $ do
       let (untranslateable, translations) =

src/SAWScript/CrucibleMethodSpecIR.hs

@@ -62,10 +62,11 @@ import qualified Lang.Crucible.Simulator.Intrinsics as Crucible
 import qualified What4.ProgramLoc as W4 (plSourceLoc)
 
 import qualified SAWScript.CrucibleLLVM as CL
+import           SAWScript.Options
+import           SAWScript.Utils (bullets)
 
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.TypedTerm
-import           SAWScript.Options
 
 newtype AllocIndex = AllocIndex Int
   deriving (Eq, Ord, Show)
@@ -198,7 +199,7 @@ ppMethodSpec methodSpec =
   PP.text "Name: " <> PP.text (methodSpec ^. csName)
   PP.<$$> PP.text "Location: " <> PP.pretty (W4.plSourceLoc (methodSpec ^. csLoc))
   PP.<$$> PP.text "Argument types: "
-  PP.<$$> PP.indent 2 (PP.vcat (map (PP.text . show) (methodSpec ^. csArgs)))
+  PP.<$$> bullets '-' (map (PP.text . show) (methodSpec ^. csArgs))
   PP.<$$> PP.text "Return type: " <> case methodSpec ^. csRet of
                                        Nothing  -> PP.text "<void>"
                                        Just ret -> PP.text (show ret)

src/SAWScript/CrucibleOverride.hs

@@ -98,7 +98,7 @@ import           Verifier.SAW.TypedTerm
 import           SAWScript.CrucibleMethodSpecIR
 import           SAWScript.CrucibleResolveSetupValue
 import           SAWScript.Options
-import           SAWScript.Utils (handleException)
+import           SAWScript.Utils (bullets, handleException)
 
 -- | The 'OverrideMatcher' type provides the operations that are needed
 -- to match a specification's arguments with the arguments provided by
@@ -433,9 +433,6 @@ failure loc e = OM (lift (throwE (OF loc e)))
 
 ------------------------------------------------------------------------
 
-bullets :: Char -> [PP.Doc] -> PP.Doc
-bullets c = PP.vcat . map (PP.hang 2 . (PP.text [c] PP.<+>))
-
 -- | Partition into three groups:
 --   * Preconditions concretely succeed
 --   * Preconditions concretely fail
@@ -1270,7 +1267,7 @@ learnPointsTo opts sc cc spec prepost (PointsTo loc ptr val) =
            assertion_tree
          addAssert pred_ $ Crucible.SimError loc "Invalid memory load"
          pure Nothing <* matchArg opts sc cc spec prepost res_val memTy val
-       W4.Err err -> do
+       W4.Err _err -> do
          -- When we have a concrete failure, we do a little more computation to
          -- try and find out why.
          let (blk, _offset) = Crucible.llvmPointerView ptr1
@@ -1298,16 +1295,14 @@ learnPointsTo opts sc cc spec prepost (PointsTo loc ptr val) =
                     , "possibly matching allocation(s):"
                     ]
                   ])
-               PP.<$$> PP.nest 2 (bullets (map Crucible.ppSomeAlloc possibleAllocs))
+               PP.<$$> bullets '-' (map Crucible.ppSomeAlloc possibleAllocs)
                -- This information tends to be overwhelming, but might be useful?
                -- We should brainstorm about better ways of presenting it.
                -- PP.<$$> PP.text (unwords [ "Here are the details on why reading"
                --                          , "from each matching write failed"
                --                          ])
                -- PP.<$$> PP.text (show err)
 
-  where bullets xs = PP.vcat [ PP.text "-" PP.<+> d | d <- xs ]
-
 ------------------------------------------------------------------------
 
 stateCond :: PrePost -> String

src/SAWScript/Exceptions.hs

@@ -3,8 +3,7 @@ module SAWScript.Exceptions (TypeErrors(..), failTypecheck) where
 
 import Control.Exception
 
-import SAWScript.Position (Pos(..), Positioned(..))
-import SAWScript.Utils
+import SAWScript.Position (Pos(..))
 
 newtype TypeErrors = TypeErrors [(Pos, String)]
 

src/SAWScript/JVM/CrucibleResolveSetupValue.hs

@@ -38,10 +38,7 @@ import Verifier.SAW.SharedTerm
 import Verifier.SAW.TypedTerm
 
 -- crucible
-import qualified Lang.Crucible.Backend as Crucible (IsSymInterface)
-import qualified Lang.Crucible.CFG.Expr as Crucible (App(..))
-import qualified Lang.Crucible.Simulator as Crucible (RegValue, RegValue'(..), extensionEval)
-import qualified Lang.Crucible.Simulator.Evaluation as Crucible (evalApp)
+import qualified Lang.Crucible.Simulator as Crucible (RegValue)
 
 -- what4
 import qualified What4.Partial as W4

src/SAWScript/JavaMethodSpecIR.hs

@@ -79,7 +79,7 @@ import Verifier.SAW.TypedAST (ppTerm, defaultPPOpts)
 import qualified SAWScript.CongruenceClosure as CC
 import SAWScript.CongruenceClosure (CCSet)
 import SAWScript.JavaExpr
-import SAWScript.Position (Pos(..), Positioned(..))
+import SAWScript.Position (Pos(..))
 import SAWScript.Utils
 
 -- ExprActualTypeMap {{{1

src/SAWScript/Utils.hs

@@ -10,6 +10,7 @@ Stability   : provisional
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DeriveDataTypeable  #-}
+
 module SAWScript.Utils where
 
 #if !MIN_VERSION_base(4,8,0)
@@ -31,7 +32,7 @@ import System.Time(TimeDiff(..), getClockTime, diffClockTimes, normalizeTimeDiff
 import System.Locale(defaultTimeLocale)
 import qualified System.IO.Error as IOE
 import System.Exit
-import Text.PrettyPrint.ANSI.Leijen hiding ((</>), (<$>))
+import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>))
 import Text.Printf
 import Numeric(showFFloat)
 
@@ -40,6 +41,9 @@ import qualified Verifier.Java.Codebase as JSS
 import SAWScript.Options
 import SAWScript.Position
 
+bullets :: Char -> [PP.Doc] -> PP.Doc
+bullets c = PP.vcat . map (PP.hang 2 . (PP.text [c] PP.<+>))
+
 data SSMode = Verify | Blif | CBlif deriving (Eq, Show, Data, Typeable)
 
 -- | Convert a string to a paragraph formatted document.