From 4d4c3946f273a47d37a6694a319d824b1a5a8cab Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 11 Jun 2024 21:21:24 +0000
Subject: [PATCH] Avoid sizeof

---
 .../src/codegen_cprover_gotoc/codegen/intrinsic.rs       | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 2f97fcb5ec53..942c39203083 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1880,12 +1880,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "`dst` must be properly aligned",
             loc,
         );
-        let deref = dst.dereference();
-        if deref.typ().sizeof(&self.symbol_table) == 0 {
+        if self.is_zst_stable(pointee_type_stable(dst_typ).unwrap()) {
             // do not attempt to dereference (and assign) a ZST
             align_check
         } else {
-            let expr = deref.assign(src, loc);
+            let expr = dst.dereference().assign(src, loc);
             Stmt::block(vec![align_check, expr], loc)
         }
     }
@@ -1991,8 +1990,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let x = fargs.remove(0);
         let y = fargs.remove(0);
 
-        let deref_y = y.clone().dereference();
-        if deref_y.typ().sizeof(&self.symbol_table) == 0 {
+        if self.is_zst_stable(pointee_type_stable(farg_types[0]).unwrap()) {
             // do not attempt to dereference (and assign) a ZST
             Stmt::skip(loc)
         } else {
@@ -2020,6 +2018,7 @@ impl<'tcx> GotocCtx<'tcx> {
             );
 
             // T t = *y; *y = *x; *x = t;
+            let deref_y = y.clone().dereference();
             let (temp_var, assign_to_t) =
                 self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc);
             let assign_to_y = y.dereference().assign(x.clone().dereference(), loc);