From 9ec6a917357342a4aae8ee4f7ca1d0bf7d2de4ba Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 25 Apr 2023 16:53:08 -0700 Subject: [PATCH] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- kani-compiler/src/kani_middle/attributes.rs | 2 +- kani-driver/src/args.rs | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 69e7fe756a40..abec9c4a8c77 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -171,7 +171,7 @@ pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: err.note(format!("see issue {link} for more information")); } err.help(format!( - "use `-Z {}` to enable use this API.", + "use `-Z {}` to enable using this API.", unstable_attr.feature )); err.emit(); diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index 171712e9de4c..431dbfbae875 100644 --- a/kani-driver/src/args.rs +++ b/kani-driver/src/args.rs @@ -350,10 +350,10 @@ pub enum ConcretePlaybackMode { #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)] #[strum(serialize_all = "kebab-case")] pub enum UnstableFeatures { - /// Allow replace certain items with stubs (mocks). - /// See (RFC-0002)[https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html] + /// Allow replacing certain items with stubs (mocks). + /// See [RFC-0002](https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html) Stubbing, - /// Generate a C-like file equivalent to inputted program used for debugging purpose. + /// Generate a C-like file equivalent to input program used for debugging purpose. GenC, }