Implement byte-to-char casts for crucible-mir.

GaloisInc · Mar 27, 2024 · 9fce599 · 9fce599
1 parent e03b20f
commit 9fce599
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs
@@ -789,12 +789,15 @@ evalCast' ck ty1 e ty2  = do
        -> baseSizeToNatCont bsz $ \w ->
            return $ MirExp (C.BVRepr w) (R.App $ E.BVIte e0 w (R.App $ eBVLit w 1) (R.App $ eBVLit w 0))
 
-      -- char to uint
+      -- char to usize
       (M.Misc, M.TyChar, M.TyUint  M.USize)
        | MirExp (C.BVRepr sz) e0 <- e
        -> return $ MirExp UsizeRepr (bvToUsize sz R.App e0)
+      -- char to other uint
       (M.Misc, M.TyChar, M.TyUint s) -> baseSizeToNatCont s $ extendUnsignedBV e
 
+      -- byte to char
+      (M.Misc, M.TyUint B8, M.TyChar) -> baseSizeToNatCont M.B32 $ extendUnsignedBV e