Make test binary translate and check Float.cry and Array.cry.

This is another step toward addressing #25.
GaloisInc · Jul 30, 2020 · a48cce3 · a48cce3
1 parent 0410199
commit a48cce3
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/test/CryptolVerifierTC.hs b/test/CryptolVerifierTC.hs
@@ -21,9 +21,13 @@ main =
      C.scLoadCryptolModule sc
      putStrLn "Loaded Cryptol.sawcore!"
      let ?fileReader = BS.readFile
-     cenv <- CEnv.initCryptolEnv sc
+     cenv0 <- CEnv.initCryptolEnv sc
      putStrLn "Translated Cryptol.cry!"
-     mapM_ (checkTranslation sc) $ Map.assocs (CEnv.eTermEnv cenv)
+     cenv1 <- CEnv.importModule sc cenv0 (Right N.floatName) Nothing Nothing
+     putStrLn "Translated Float.cry!"
+     cenv2 <- CEnv.importModule sc cenv1 (Right N.arrayName) Nothing Nothing
+     putStrLn "Translated Array.cry!"
+     mapM_ (checkTranslation sc) $ Map.assocs (CEnv.eTermEnv cenv2)
      putStrLn "Checked all terms!"
 
 checkTranslation :: SharedContext -> (N.Name, Term) -> IO ()