copilot 3.17 → 3.18
raw patch · 6 files changed
+33/−25 lines, 6 filesdep ~copilot-c99dep ~copilot-coredep ~copilot-language
Dependency ranges changed: copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-prettyprinter, copilot-theorem, optparse-applicative
Files
- CHANGELOG +8/−0
- copilot.cabal +8/−8
- examples/WCV.hs +2/−2
- examples/what4/Arithmetic.hs +6/−6
- examples/what4/Propositional.hs +7/−7
- examples/what4/Structs.hs +2/−2
CHANGELOG view
@@ -1,3 +1,11 @@+2024-01-07+ * Version bump (3.18). (#487)+ * Enable tests for copilot-theorem in CI script. (#474)+ * Enable tests for copilot-libraries in CI script. (#475)+ * Replace uses of forall with forAll. (#470)+ * Update CI job to check for MISRA compliance with cppcheck. (#472)+ * Relax version constraint on optparse-applicative. (#488)+ 2023-11-07 * Version bump (3.17). (#466) * Replace uses of deprecated functions. (#457)
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 3.17+version: 3.18 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -48,16 +48,16 @@ -fno-warn-orphans build-depends: base >= 4.9 && < 5- , optparse-applicative >= 0.14 && < 0.18+ , optparse-applicative >= 0.14 && < 0.19 , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.5 - , copilot-core >= 3.17 && < 3.18- , copilot-theorem >= 3.17 && < 3.18- , copilot-language >= 3.17 && < 3.18- , copilot-libraries >= 3.17 && < 3.18- , copilot-c99 >= 3.17 && < 3.18- , copilot-prettyprinter >= 3.17 && < 3.18+ , copilot-core >= 3.18 && < 3.19+ , copilot-theorem >= 3.18 && < 3.19+ , copilot-language >= 3.18 && < 3.19+ , copilot-libraries >= 3.18 && < 3.19+ , copilot-c99 >= 3.18 && < 3.19+ , copilot-prettyprinter >= 3.18 && < 3.19 exposed-modules: Language.Copilot, Language.Copilot.Main
examples/WCV.hs view
@@ -151,8 +151,8 @@ (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr)) spec = do- Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v)))- -- Monad.void $ prop "3d" (forall $ (wcv tep s sz v vz) == (wcv tep (neg s) (-sz) (neg v) (-vz)))+ Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))+ -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz) == (wcv tep (neg s) (-sz) (neg v) (-vz))) main :: IO () main = do
examples/what4/Arithmetic.hs view
@@ -21,22 +21,22 @@ efloat = extern "efloat" Nothing -- The simplest example involving numbers: equality on constant values.- void $ prop "Example 1" (forall ((constant (1 :: Int8)) == (constant 1)))+ void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1))) -- Testing "a < a + 1". This should fail, because it isn't true.- void $ prop "Example 2" (forall (eint8 < (eint8 + 1)))+ void $ prop "Example 2" (forAll (eint8 < (eint8 + 1))) -- Adding another condition to the above property to make it true.- void $ prop "Example 3" (forall ((eint8 < (eint8 + 1)) || (eint8 == 127)))+ void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127))) -- Just like the previous example, but with words.- void $ prop "Example 4" (forall ((eword8 < (eword8 + 1)) || (eword8 == 255)))+ void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255))) -- An example with floats.- void $ prop "Example 5" (forall ((2 * efloat) == (efloat + efloat)))+ void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat))) -- Another example with floats. This fails, because it isn't true.- void $ prop "Example 6" (forall ((efloat + 1) /= efloat))+ void $ prop "Example 6" (forAll ((efloat + 1) /= efloat)) main :: IO () main = do
examples/what4/Propositional.hs view
@@ -13,38 +13,38 @@ spec = do -- The constant value true, which is translated as the corresponding SMT -- boolean literal.- void $ prop "Example 1" (forall true)+ void $ prop "Example 1" (forAll true) -- The constant value false, which is translated as the corresponding SMT -- boolean literal.- void $ prop "Example 2" (forall false)+ void $ prop "Example 2" (forAll false) -- An inductively defined flavor of true, which requires induction to prove, -- and hence is found to be invalid by the SMT solver (since no inductive -- hypothesis is made). let a = [True] ++ a- void $ prop "Example 3" (forall a)+ void $ prop "Example 3" (forAll a) -- An inductively defined "a or not a" proposition, which is unprovable by -- the SMT solver. let a = [False] ++ b b = [True] ++ a- void $ prop "Example 4" (forall (a || b))+ void $ prop "Example 4" (forAll (a || b)) -- A version of "a or not a" proposition which does not require any sort of -- inductive argument, and hence is provable. let a = [False] ++ b b = not a- void $ prop "Example 5" (forall (a || b))+ void $ prop "Example 5" (forAll (a || b)) -- A bit more convoluted version of Example 5, which is provable. let a = [True, False] ++ b b = [False] ++ not (drop 1 a)- void $ prop "Example 6" (forall (a || b))+ void $ prop "Example 6" (forAll (a || b)) -- An example using external streams. let a = extern "a" Nothing- void $ prop "Example 7" (forall (a || not a))+ void $ prop "Example 7" (forAll (a || not a)) main :: IO () main = do
examples/what4/Structs.hs view
@@ -56,12 +56,12 @@ -- Check equality, indexing into nested structs and arrays. Note that this is -- trivial by equality.- void $ prop "Example 1" $ forall $+ void $ prop "Example 1" $ forAll $ (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts) -- Same as previous example, but get a different array index (so should be -- false).- void $ prop "Example 2" $ forall $+ void $ prop "Example 2" $ forAll $ (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4) main :: IO ()