copilot-verifier-0.1: examples/Copilot/Verifier/Examples/ShouldPass/Partial/MulSignedWrap.hs

{-# LANGUAGE NoImplicitPrelude #-}

-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Mul@
-- operation should wrap on signed integers precisely when C multiplication does.
module Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap where

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , sideCondVerifierOptions, verifyWithOptions )
import Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap (spec)

verifySpec :: Verbosity -> IO ()
verifySpec verb = do
  spec' <- reify spec
  verifyWithOptions sideCondVerifierOptions{verbosity = verb}
    mkDefaultCSettings
    []
    "mulSignedWrapPass" spec'