Trying to debug tests/expected/cover/cover-message/main.rs

model-checking · Apr 13, 2023 · 0064927 · 0064927
1 parent c5b895c
commit 0064927
Showing 1 changed file with 7 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
@@ -465,6 +465,8 @@ impl<'tcx> GotocCtx<'tcx> {
                         niche_variants,
                         niche_start,
                     );
+                    debug!(?layout, "LAYOUT");
+                    debug!(?variant_layout, "VARIANT LAYOUT");
                     let mut operands_base_offset = Size::from_bits(0);
                     if let FieldsShape::Arbitrary { offsets, .. } = &variant_layout.fields {
                         let mut indices = variant_layout.fields.index_by_increasing_offset();
@@ -475,6 +477,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     } else {
                         unreachable!();
                     }
+                    debug!(?operands_base_offset, "BASE OFFSET");
                     let niche_offset = layout.fields.offset(*tag_field);
                     let lvalue_niche = self.codegen_get_niche(
                         lvalue.clone(),
@@ -504,6 +507,10 @@ impl<'tcx> GotocCtx<'tcx> {
                                     <= operands_base_offset.bits()
                         );
                         // data update must be within bounds
+                        let target_size = target_component.typ().sizeof_in_bits(&self.symbol_table);
+                        debug!(?target_size, "TARGET SIZE");
+                        let lvalue_size = lvalue.typ().sizeof_in_bits(&self.symbol_table);
+                        debug!(?lvalue_size, "LVALUE SIZE");
                         assert!(
                             operands_base_offset.bits()
                                 + target_component.typ().sizeof_in_bits(&self.symbol_table)