sbv-8.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Levent Erkok
Safe HaskellNone




Test generation from symbolic programs


Test case generation

genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors Source #

Generate a set of concrete test values from a symbolic program. The output can be rendered as test vectors in different languages as necessary. Use the function output call to indicate what fields should be in the test result. (Also see constrain for filtering acceptable test values.)

data TestVectors Source #

Type of test vectors (abstract)

getTestValues :: TestVectors -> [([CV], [CV])] Source #

Retrieve the test vectors for further processing. This function is useful in cases where renderTest is not sufficient and custom output (or further preprocessing) is needed.

renderTest :: TestStyle -> TestVectors -> String Source #

Render the test as a Haskell value with the given name n.

data TestStyle Source #

Test output style


Haskell String

As a Haskell value with given name

C String

As a C array of structs with given name

Forte String Bool ([Int], [Int])

As a Forte/Verilog value with given name. If the boolean is True then vectors are blasted big-endian, otherwise little-endian The indices are the split points on bit-vectors for input and output values