Pate.TraceConstraint: support parsing constraints for symbolic integers

these occur when pointers have symbolic regions
GaloisInc · Aug 13, 2024 · 995e16d · 995e16d
1 parent dcda670
commit 995e16d
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/Pate/TraceConstraint.hs b/src/Pate/TraceConstraint.hs
@@ -81,6 +81,10 @@ instance forall sym. W4S.W4Deserializable sym (TraceConstraint sym) where
         case (BVS.mkBVUnsigned w c) of
           Just bv -> return $ TraceConstraint var op (W4.ConcreteBV w bv)
           Nothing -> fail "Unexpected integer size"
+      W4.BaseIntegerRepr -> do
+        (cS :: String) <- o .: "const"
+        ((c :: Integer),""):_ <- return $ Num.readDec cS
+        return $ TraceConstraint var op (W4.ConcreteInteger c)
       _ -> fail ("Unsupported expression type:" ++ show (W4.exprType var))
 
 constraintToPred ::