diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index e618d8ec2163..ee0b8e769bc7 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -138,6 +138,7 @@ impl<'tcx> From<&Statement<'tcx>> for Key { | StatementKind::ConstEvalCounter | StatementKind::FakeRead(_) | StatementKind::Nop + | StatementKind::PlaceMention(_) | StatementKind::Retag(_, _) | StatementKind::StorageLive(_) | StatementKind::StorageDead(_) => Key("Ignored"), @@ -148,11 +149,9 @@ impl<'tcx> From<&Statement<'tcx>> for Key { impl<'tcx> From<&Terminator<'tcx>> for Key { fn from(value: &Terminator<'tcx>) -> Self { match value.kind { - TerminatorKind::Abort => Key("Abort"), TerminatorKind::Assert { .. } => Key("Assert"), TerminatorKind::Call { .. } => Key("Call"), TerminatorKind::Drop { .. } => Key("Drop"), - TerminatorKind::DropAndReplace { .. } => Key("DropAndReplace"), TerminatorKind::GeneratorDrop => Key("GeneratorDrop"), TerminatorKind::Goto { .. } => Key("Goto"), TerminatorKind::FalseEdge { .. } => Key("FalseEdge"), @@ -161,6 +160,7 @@ impl<'tcx> From<&Terminator<'tcx>> for Key { TerminatorKind::Resume => Key("Resume"), TerminatorKind::Return => Key("Return"), TerminatorKind::SwitchInt { .. } => Key("SwitchInt"), + TerminatorKind::Terminate => Key("Terminate"), TerminatorKind::Unreachable => Key("Unreachable"), TerminatorKind::Yield { .. } => Key("Yield"), } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 8bb298dbd810..8e0691182215 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -8,7 +8,7 @@ use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem}; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; -use rustc_middle::ty::{self, Instance, TyCtxt}; +use rustc_middle::ty::{self, Instance, TyCtxt, TyKind}; use rustc_span::Span; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; @@ -155,6 +155,11 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option