Fix aggregate handling for raw pointer to str

We were handling aggregate of string as we handle thin slices due to a missing match arm. Added the new handling.
model-checking · Aug 17, 2024 · 409f4a9 · 409f4a9
1 parent e6f8a62
commit 409f4a9
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -694,6 +694,15 @@ impl<'tcx> GotocCtx<'tcx> {
                         let meta = self.codegen_operand_stable(&operands[1]);
                         slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
                     }
+                    TyKind::RigidTy(RigidTy::Str) => {
+                        let pointee_goto_typ = Type::unsigned_int(8);
+                        // cast data to pointer with specified type
+                        let data_cast =
+                            data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ.clone()) });
+                        debug!(?res_ty, ?typ, ?pointee_goto_typ, "** AGG **");
+                        let meta = self.codegen_operand_stable(&operands[1]);
+                        slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
+                    }
                     TyKind::RigidTy(RigidTy::Adt(..)) => {
                         let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
                         let data_cast =