Merge pull request #83 from Copilot-Language/T82-release-4.3

Require building with Copilot 4.3. Refs #82.

Author: RyanGlScott

copilot-verifier/CHANGELOG

@@ -1,4 +1,5 @@
-2025-02-03
+2025-03-10
+        * Version bump (4.3). (#82)
         * Add `smtSolver` option to `VerifierOptions`. (#78)
         * Add `smtFloatMode` option to `VerifierOptions`. (#79)
 

copilot-verifier/copilot-verifier.cabal

@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          copilot-verifier
-Version:       4.2
+Version:       4.3
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com
 Copyright:     (c) Galois, Inc 2021-2024
@@ -45,9 +45,9 @@ common bldflags
     bv-sized >= 1.0.0 && < 1.1,
     bytestring,
     containers >= 0.5.9.0,
-    copilot-c99 >= 4.2 && < 4.3,
-    copilot-core >= 4.2 && < 4.3,
-    copilot-theorem >= 4.2 && < 4.3,
+    copilot-c99 >= 4.3 && < 4.4,
+    copilot-core >= 4.3 && < 4.4,
+    copilot-theorem >= 4.3 && < 4.4,
     crucible >= 0.7.1 && < 0.8,
     crucible-llvm >= 0.7 && < 0.8,
     crux >= 0.7.1 && < 0.8,
@@ -80,10 +80,10 @@ library copilot-verifier-examples
   hs-source-dirs: examples
   build-depends:
     case-insensitive,
-    copilot >= 4.2 && < 4.3,
-    copilot-language >= 4.2 && < 4.3,
-    copilot-libraries >= 4.2 && < 4.3,
-    copilot-prettyprinter >= 4.2 && < 4.3,
+    copilot >= 4.3 && < 4.4,
+    copilot-language >= 4.3 && < 4.4,
+    copilot-libraries >= 4.3 && < 4.4,
+    copilot-prettyprinter >= 4.3 && < 4.4,
     copilot-verifier
   exposed-modules:
     Copilot.Verifier.Examples

copilot-verifier/src/Copilot/Verifier.hs

@@ -1014,7 +1014,7 @@ copilotExprToRegValue sym = loop
     loop (CW4.XFloat x)  (FloatRepr SingleFloatRepr) = return x
     loop (CW4.XDouble x) (FloatRepr DoubleFloatRepr) = return x
 
-    loop CW4.XEmptyArray (VectorRepr _tpr) =
+    loop (CW4.XEmptyArray _ctp) (VectorRepr _tpr) =
       pure V.empty
     loop (CW4.XArray xs) (VectorRepr tpr) =
       V.generateM (PVec.lengthInt xs) (\i -> loop (PVec.elemAtUnsafe i xs) tpr)
@@ -1075,7 +1075,7 @@ computeEqualVals bak clRefs mem = loop
     loop Float (CW4.XFloat x)  (FloatRepr SingleFloatRepr) v = iFloatEq @_ @SingleFloat sym x v
     loop Double (CW4.XDouble x) (FloatRepr DoubleFloatRepr) v = iFloatEq @_ @DoubleFloat sym x v
 
-    loop (Array _ctp) CW4.XEmptyArray (VectorRepr _tpr) vs =
+    loop (Array _ctp) (CW4.XEmptyArray _ctp2) (VectorRepr _tpr) vs =
       pure $ backendPred sym $ V.null vs
     loop (Array ctp) (CW4.XArray xs) (VectorRepr tpr) vs
       | PVec.lengthInt xs == V.length vs

copilot-verifier/src/Copilot/Verifier/Log.hs

@@ -799,7 +799,7 @@ ppCopilotValue val =
     CW4.XWord64 w -> WI.printSymExpr w
     CW4.XFloat  f -> WI.printSymExpr f
     CW4.XDouble d -> WI.printSymExpr d
-    CW4.XEmptyArray -> "[]"
+    CW4.XEmptyArray {} -> "[]"
     CW4.XArray  a   -> ppBracesWith ppCopilotValue (PV.toList a)
     CW4.XStruct s   -> ppBracketsWith ppCopilotValue s