content: {-# LANGUAGE NoImplicitPrelude #-}
  
  -- | This will fail to verify since the verification does not assume the
  -- @lessThanBitWidth@ property, which is needed to prevent shifting by too
  -- large of a value.
  module Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge where
  
  import Language.Copilot
  import Copilot.Compile.C99
  import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                          , defaultVerifierOptions, verifyWithOptions )
  
  spec :: Spec
  spec = do
    let stream1 :: Stream Int32
        stream1 = extern "stream1" Nothing
  
        stream2 :: Stream Int64
        stream2 = extern "stream2" Nothing
  
    _ <- prop "lessThanBitWidth" (forAll
           (constI64 0 <= stream2 && stream2 < constI64 32))
    trigger "streamShiftR" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]
  
  verifySpec :: Verbosity -> IO ()
  verifySpec verb = do
    spec' <- reify spec
    verifyWithOptions defaultVerifierOptions{verbosity = verb}
      mkDefaultCSettings
      -- ["lessThanBitWidth"]
      []
      "shiftRTooLargeFail" spec'
  