Merge branch 'master' into saw-core/typechecking-debugging

Author: Eddy Westbrook

crux-mir-comp/test/Test.hs

@@ -77,12 +77,15 @@ runCrux rustFile outHandle mode = Mir.withMirLogging $ do
     -- verification runs close to the timeout, causing flaky results
     -- (especially in CI).
     let quiet = True
-    let options = (defaultCruxOptions { Crux.inputFiles = [rustFile],
-                                        Crux.simVerbose = 0,
+    let outOpts = (Crux.outputOptions defaultCruxOptions)
+                    { Crux.simVerbose = 0
+                    , Crux.quietMode = quiet
+                    }
+    let options = (defaultCruxOptions { Crux.outputOptions = outOpts,
+                                        Crux.inputFiles = [rustFile],
                                         Crux.globalTimeout = Just 180,
                                         Crux.goalTimeout = Just 180,
                                         Crux.solver = "z3",
-                                        Crux.quietMode = quiet,
                                         Crux.checkPathSat = (mode == RcmCoverage),
                                         Crux.outDir = case mode of
                                             RcmCoverage -> getOutputDir rustFile
@@ -91,7 +94,7 @@ runCrux rustFile outHandle mode = Mir.withMirLogging $ do
                    Mir.defaultMirOptions { Mir.printResultOnly = (mode == RcmConcrete),
                                            Mir.defaultRlibsDir = "../deps/crucible/crux-mir/rlibs" })
     let ?outputConfig = Crux.mkOutputConfig (outHandle, False) (outHandle, False)
-            Mir.mirLoggingToSayWhat (Just $ fst options)
+            Mir.mirLoggingToSayWhat (Just $ Crux.outputOptions $ fst options)
     setEnv "CRYPTOLPATH" "."
     _exitCode <- Mir.runTestsWithExtraOverrides overrides options
     return ()

deps/crucible

@@ -908,21 +908,15 @@ evaluateExpr sym st sc cache = f []
         B.FloatToSBV{} -> floatFail
         B.FloatToReal{} -> floatFail
         B.FloatToBinary{} -> floatFail
+        B.FloatSpecialFunction{} -> floatFail
 
         B.RoundReal{} -> realFail
         B.RoundEvenReal{} -> realFail
         B.FloorReal{} -> realFail
         B.CeilReal{} -> realFail
         B.RealDiv{} -> realFail
         B.RealSqrt{} -> realFail
-        B.Pi{} -> realFail
-        B.RealSin{} -> realFail
-        B.RealCos{} -> realFail
-        B.RealSinh{} -> realFail
-        B.RealCosh{} -> realFail
-        B.RealExp{} -> realFail
-        B.RealLog{} -> realFail
-        B.RealATan2{} -> realFail
+        B.RealSpecialFunction{} -> realFail
 
         B.Cplx{}     -> cplxFail
         B.RealPart{} -> cplxFail

deps/what4

@@ -258,7 +258,8 @@ loadLLVMModule file halloc =
        Left err -> return (Left err)
        Right llvm_mod ->
          do memVar <- CL.mkMemVar (Text.pack "saw:llvm_memory") halloc
-            Some mtrans <- CL.translateModule halloc memVar llvm_mod
+            -- FIXME: do something with the translation warnings
+            (Some mtrans, _warnings) <- CL.translateModule halloc memVar llvm_mod
             return (Right (Some (LLVMModule file llvm_mod mtrans)))
 
 instance TestEquality LLVMModule where