Demo: Assertion loses info unless in a block

adpaco-aws · Feb 8, 2024 · 8f86333 · 8f86333
1 parent 55a7f3e
commit 8f86333
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 2 deletions.
diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs
@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! GOTO binary serializer.
 
+use tracing::debug;
+
 use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
 use crate::{InternString, InternedString};
 use std::collections::HashMap;
@@ -23,6 +25,8 @@ pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::Sym
     let mut writer = BufWriter::new(out_file);
     let mut serializer = GotoBinarySerializer::new(&mut writer);
     let irep_symbol_table = &source.to_irep();
+    debug!("SYMTAB: {irep_symbol_table:?}");
+    // debug!("SYMTAB: {source:?}");
     serializer.write_file(irep_symbol_table);
 }
 

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -93,13 +93,18 @@ impl<'tcx> GotocCtx<'tcx> {
                     "assumption failed",
                     location,
                 )
-            }
+            },
+            StatementKind::Coverage(opaque) => {
+            debug!(?opaque, "StatementKind::Coverage Opaque");
+            self.codegen_coverage(stmt.span)
+            // let coverage_stmt = self.codegen_coverage(stmt.span);
+            // Stmt::block(vec![coverage_stmt], location)
+            },
             StatementKind::PlaceMention(_) => todo!(),
             StatementKind::FakeRead(..)
             | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType { .. }
             | StatementKind::Nop
-            | StatementKind::Coverage { .. }
             | StatementKind::ConstEvalCounter => Stmt::skip(location),
         }
         .with_location(location)

diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
@@ -116,6 +116,10 @@ impl KaniSession {
         // We only use panic abort strategy for verification since we cannot handle unwind logic.
         flags.extend_from_slice(
             &[
+                "-C",
+                "instrument-coverage",
+                "-Z",
+                "no-profiler-runtime",
                 "-C",
                 "panic=abort",
                 "-C",