Skip to content

Commit b5b8484

Browse files
committed
Re-enable signum examples in {Int,FP}Ops
This bumps the `copilot` submodule to bring in GaloisInc/copilot-1#8, which fixes how `copilot-c99` and `copilot-theorem` handle `signum`. With these fixes, we can finally enable `signum` in the `IntOps` and `FPOps` examples. Fixes #14.
1 parent 6fe812b commit b5b8484

3 files changed

Lines changed: 3 additions & 5 deletions

File tree

copilot-verifier/examples/Copilot/Verifier/Examples/FPOps.hs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,7 @@ mkSpecFor _ nameSuffix = do
1919
stream = extern (mkName "stream") Nothing
2020

2121
triggerOp1 (mkName "abs") abs stream
22-
-- Currently fails due to https://github.com/GaloisInc/copilot-verifier/issues/14
23-
-- triggerOp1 (mkName "signum") signum stream
22+
triggerOp1 (mkName "signum") signum stream
2423
triggerOp1 (mkName "recip") recip stream
2524
triggerOp1 (mkName "exp") exp stream
2625
triggerOp1 (mkName "sqrt") sqrt stream

copilot-verifier/examples/Copilot/Verifier/Examples/IntOps.hs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,7 @@ spec = do
1818
_ <- prop "shiftByBits" (forall (0 <= shiftBy && shiftBy < 16))
1919

2020
triggerOp1 "abs" abs stream
21-
-- Currently fails due to https://github.com/GaloisInc/copilot-verifier/issues/14
22-
-- triggerOp1 "signum" signum stream
21+
triggerOp1 "signum" signum stream
2322
triggerOp1 "bwNot" complement stream
2423

2524
triggerOp2 "add" (+) stream stream

0 commit comments

Comments
 (0)