copilot 3.20 → 4.0

raw patch · 5 files changed

+35/−12 lines, 5 filesdep ~copilot-c99dep ~copilot-coredep ~copilot-languagePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-prettyprinter, copilot-theorem

API changes (from Hackage documentation)

Files

• CHANGELOG +5/−0
• copilot.cabal +7/−7
• examples/Array.hs +15/−1
• examples/Structs.hs +2/−2
• examples/what4/Structs.hs +6/−2

@@ -1,3 +1,8 @@+2024-09-07+        * Version bump (4.0). (#532)+        * Update example to demonstrate struct update support. (#524)+        * Update example to demonstrate array update support. (#36)+ 2024-07-07         * Version bump (3.20). (#522)         * Update README to reflect support for GHC 9.8. (#518)

@@ -1,5 +1,5 @@ name:                copilot-version:             3.20+version:             4.0 cabal-version:       >= 1.10 license:             BSD3 license-file:        LICENSE@@ -52,12 +52,12 @@                      , directory             >= 1.3  && < 1.4                      , filepath              >= 1.4  && < 1.5 -                     , copilot-core          >= 3.20 && < 3.21-                     , copilot-theorem       >= 3.20 && < 3.21-                     , copilot-language      >= 3.20 && < 3.21-                     , copilot-libraries     >= 3.20 && < 3.21-                     , copilot-c99           >= 3.20 && < 3.21-                     , copilot-prettyprinter >= 3.20 && < 3.21+                     , copilot-core          >= 4.0 && < 4.1+                     , copilot-theorem       >= 4.0 && < 4.1+                     , copilot-language      >= 4.0 && < 4.1+                     , copilot-libraries     >= 4.0 && < 4.1+                     , copilot-c99           >= 4.0 && < 4.1+                     , copilot-prettyprinter >= 4.0 && < 4.1       exposed-modules: Language.Copilot, Language.Copilot.Main

@@ -26,7 +26,21 @@   -- It passes the current value of arr as an argument.   -- The prototype of 'func' would be:   -- void func (int8_t arg[3]);-  trigger "func" (arr .!! 0) [arg arr]+  trigger "func" (arr ! 0) [arg arr]++  -- A trigger that fires 'func2' every time.+  -- It passes the current value of arr as an argument, but updating the first+  -- element of the array to always be True.+  -- The prototype of 'func2' would be:+  -- void func2 (int8_t arg[3]);+  trigger "func2" true [arg (arr !! 0 =: true)]++  -- A trigger that fires 'func2' every time.+  -- It passes the current value of arr as an argument, but negating the second+  -- element of the array.+  -- The prototype of 'func3' would be:+  -- void func3 (int8_t arg[3]);+  trigger "func3" true [arg (arr !! 1 =$ not)]  -- Compile the spec main :: IO ()

@@ -56,13 +56,13 @@   -- Check equality, indexing into nested structs and arrays. Note that this is   -- trivial by equality.   trigger "equalitySameIndex"-    ((((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts))+    ((((battery#volts) ! 0)#numVolts) == (((battery#volts) ! 0)#numVolts))     [arg battery]    -- Same as previous example, but get a different array index (so should be   -- false).   trigger "equalityDifferentIndices"-    ((((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4))+    ((((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4))     [arg battery]  main :: IO ()

@@ -57,12 +57,16 @@   -- Check equality, indexing into nested structs and arrays. Note that this is   -- trivial by equality.   void $ prop "Example 1" $ forAll $-    (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts)+    (((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 $-    (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)+    (((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4)++  -- Update a struct field, then check it for equality.+  void $ prop "Example 3" $ forAll $+    ((battery ## temp =$ (+1))#temp == (battery#temp + 1))  main :: IO () main = do