Adapt saw-remote-api package to remove dependency on jvm-verifier.

GaloisInc · Jan 14, 2021 · ad4e48f · ad4e48f
1 parent bf46828
commit ad4e48f
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal
@@ -52,7 +52,6 @@ common deps
                  cryptonite-conduit,
                  directory,
                  jvm-parser,
-                 jvm-verifier,
                  lens,
                  llvm-pretty,
                  llvm-pretty-bc-parser,

diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs
@@ -37,7 +37,7 @@ import qualified Data.AIG as AIG
 import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator)
 import qualified Lang.Crucible.JVM as CJ
 import qualified Text.LLVM.AST as LLVM
-import qualified Verifier.Java.Codebase as JSS
+import qualified Lang.JVM.Codebase as JSS
 import qualified Verifier.SAW.CryptolEnv as CryptolEnv
 import Verifier.SAW.Module (emptyModule)
 import Verifier.SAW.SharedTerm (mkSharedContext, scLoadModule)
@@ -55,7 +55,6 @@ import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibl
 import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm)
 import Verifier.SAW.Rewriter (Simpset)
-import qualified Verifier.Java.SAWBackend as JavaSAW
 import qualified Cryptol.Utils.Ident as Cryptol
 
 import Argo
@@ -159,7 +158,6 @@ initialState readFileFn =
   silence $
   do sc <- mkSharedContext
      CryptolSAW.scLoadPreludeModule sc
-     JavaSAW.scLoadJavaModule sc
      CryptolSAW.scLoadCryptolModule sc
      let mn = mkModuleName ["SAWScript"]
      scLoadModule sc (emptyModule mn)