Copyright | (c) 2013-2015 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell98 |
- data BitVector = BV {}
- bitMask :: Int -> Integer
- bv :: Int -> Integer -> BitVector
- sbv :: Bool -> Int -> Integer -> BitVector
- unsigned :: Int -> Integer -> Integer
- signed :: Int -> Integer -> Integer
- same :: Int -> Int -> Int
- type SWord = SBV BitVector
- extract :: Int -> Int -> SWord -> SWord
- cat :: SWord -> SWord -> SWord
- literalSWord :: Int -> Integer -> SWord
- randomSBVBitVector :: Int -> IO (SBV BitVector)
- mkSymBitVector :: Maybe Quantifier -> Maybe String -> Int -> Symbolic (SBV BitVector)
- forallBV :: String -> Int -> Symbolic (SBV BitVector)
- forallBV_ :: Int -> Symbolic (SBV BitVector)
- existsBV :: String -> Int -> Symbolic (SBV BitVector)
- existsBV_ :: Int -> Symbolic (SBV BitVector)
Documentation
Invariant: BV w x requires that 0 <= w and 0 <= x < 2^w.
literalSWord :: Int -> Integer -> SWord Source
mkSymBitVector :: Maybe Quantifier -> Maybe String -> Int -> Symbolic (SBV BitVector) Source