Fix code actions

model-checking · Aug 26, 2024 · dc332a7 · dc332a7
1 parent 3376a93
commit dc332a7
Showing 1 changed file with 9 additions and 10 deletions.
diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs
@@ -120,16 +120,15 @@ impl<'locals> CollectActions<'locals> {
                 return;
             }
         };
-        match place.ty(self.locals).unwrap().kind() {
-            TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => {
-                self.actions.push(Action::StackUpdateReference { place: place.local, ty });
-                self.actions.push(Action::StackCheck);
-            }
-            TyKind::RigidTy(RigidTy::RawPtr(ty, _)) => {
-                self.actions.push(Action::StackUpdatePointer { place: place.local, ty });
-                self.actions.push(Action::StackCheck);
-            }
-            _ => {}
+        if self.locals[place.local].ty.kind().is_ref() {
+            let ty = place.ty(self.locals).unwrap();
+            self.actions.push(Action::StackUpdateReference { place: place.local, ty });
+            self.actions.push(Action::StackCheck);
+        }
+        if self.locals[place.local].ty.kind().is_raw_ptr() {
+            let ty = place.ty(self.locals).unwrap();
+            self.actions.push(Action::StackUpdatePointer { place: place.local, ty });
+            self.actions.push(Action::StackCheck);
         }
     }