{-# LANGUAGE NoImplicitPrelude #-}

-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @BwShiftR@
-- operation should only accept second arguments as large as C's @>>@ operation does.
module Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge where

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

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = do
  Spec
spec' <- Spec' () -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec' ()
spec
  VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
sideCondVerifierOptions{verbosity = verb}
    CSettings
mkDefaultCSettings
    []
    String
"shiftRTooLargePass" Spec
spec'