www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

bv-tests.rkt (1102B)

      1 #lang s-exp "../../rosette/bv.rkt"
      2 (require "../rackunit-typechecking.rkt")
      3 
      4 (check-type current-bvpred : (CParamof CBVPred))
      5 (check-type (current-bvpred) : BVPred -> (bitvector 4))
      6 (check-type (current-bvpred (bitvector 5)) : CUnit -> (void))
      7 (check-type (current-bvpred) : BVPred -> (bitvector 5))
      8 (check-type (current-bvpred (bitvector 4)) : CUnit -> (void))
      9 
     10 (check-type (bv 1) : BV)
     11 (check-type ((bitvector 4) (bv 1)) : Bool -> #t)
     12 (check-type ((bitvector 1) (bv 1)) : Bool -> #f)
     13 (check-type (bv 2 (bitvector 3)) : BV)
     14 (check-type ((bitvector 3) (bv 2 (bitvector 3))) : Bool -> #t)
     15 
     16 (check-type (bv*) : BV)
     17 
     18 (check-type (if 1 (bv 1) (bv 0)) : BV -> (bv 1))
     19 (check-type (if #f (bv 1) (bv 0)) : BV -> (bv 0))
     20 (define-symbolic i integer? : Int)
     21 (define-symbolic b boolean? : Bool)
     22 (check-type (if i (bv 1) (bv 0)) : BV -> (bv 1))
     23 (check-type (if b (bv 1) (bv 0)) : BV -> (if b (bv 1) (bv 0)))
     24 
     25 (check-type (bvredor (bv 1)) : BV)
     26 (check-type (bvredand (bv 1)) : BV)
     27 
     28 (check-type bveq : (→ BV BV BV))
     29 (check-type (bveq (bv 1) (bv 1)) : BV -> (bv 1))
     30 (check-type (bveq (bv 1) (bv 0)) : BV -> (bv 0))