CN: add test for null for int to pointer

rems-project · Aug 16, 2024 · dfd550c · dfd550c
1 parent a80cb6b
commit dfd550c
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/backend/cn/lib/solver.ml b/backend/cn/lib/solver.ml
@@ -933,9 +933,12 @@ let rec translate_term s iterm =
     let smt_term = translate_term s t in
     (match (IT.bt t, cbt) with
      | Bits _, Loc ->
-       CN_Pointer.con
-         (CN_AllocId.to_sexp Z.zero)
-         (bv_cast Memory.uintptr_bt (IT.bt t) smt_term)
+       SMT.ite
+         (SMT.eq smt_term (SMT.bv_k CN_Pointer.width Z.zero))
+         CN_Pointer.con_null
+         (CN_Pointer.con
+            (CN_AllocId.to_sexp Z.zero)
+            (bv_cast Memory.uintptr_bt (IT.bt t) smt_term))
      | Loc, Bits _ ->
        let addr = CN_Pointer.get_addr smt_term ~default:(default Memory.uintptr_bt) in
        bv_cast cbt Memory.uintptr_bt addr