diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index 3ede2988f143..1fe9e9bd24db 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs @@ -32,6 +32,8 @@ pub struct InstrumentationVisitor<'a, 'tcx> { tcx: TyCtxt<'tcx>, } +/// This enum differentiates between different reasons to visit a place, yielding different +/// instrumentation injected. enum PlaceOperation { Read, Write,