Fix some FPs based on verus-cheat-examples from Chenyuan.

utils/lynette/source/lynette/Cargo.toml

@@ -5,6 +5,9 @@ edition = "2018"
 publish = false
 rust-version = "1.62"
 
+[dev-dependencies]
+gag = "1.0"
+
 [dependencies]
 serde_json = "1.0"
 colored = "1.7"

utils/lynette/source/lynette/src/deghost.rs

@@ -336,14 +336,14 @@ pub fn remove_ghost_sig(
                 .requires
                 .clone()
                 .map(|mut new_req| {
-                    if !new_req.exprs.exprs.trailing_punct() {
+                    if !new_req.exprs.exprs.empty_or_trailing() {
                         new_req.exprs.exprs.push_punct(Default::default());
                     }
                     new_req
                 })
                 .filter(|_| mode.requires), // Removed
             recommends: sig.spec.recommends.clone().map(|mut new_rec| {
-                if !new_rec.exprs.exprs.trailing_punct() {
+                if !new_rec.exprs.exprs.empty_or_trailing() {
                     new_rec.exprs.exprs.push_punct(Default::default());
                 }
                 new_rec
@@ -353,7 +353,7 @@ pub fn remove_ghost_sig(
                 .ensures
                 .clone()
                 .map(|mut new_ens| {
-                    if !new_ens.exprs.exprs.trailing_punct() {
+                    if !new_ens.exprs.exprs.empty_or_trailing() {
                         new_ens.exprs.exprs.push_punct(Default::default());
                     }
                     new_ens
@@ -364,7 +364,7 @@ pub fn remove_ghost_sig(
                 .decreases
                 .clone()
                 .map(|mut new_dec| {
-                    if !new_dec.decreases.exprs.exprs.trailing_punct() {
+                    if !new_dec.decreases.exprs.exprs.empty_or_trailing() {
                         new_dec.decreases.exprs.exprs.push_punct(Default::default());
                     }
                     new_dec
@@ -376,7 +376,7 @@ pub fn remove_ghost_sig(
                 .default_ensures
                 .clone()
                 .map(|mut new_ens| {
-                    if !new_ens.exprs.exprs.trailing_punct() {
+                    if !new_ens.exprs.exprs.empty_or_trailing() {
                         new_ens.exprs.exprs.push_punct(Default::default());
                     }
                     new_ens

utils/lynette/source/lynette/src/lib.rs

@@ -0,0 +1,69 @@
+use clap::Args;
+
+pub mod additions;
+pub mod benchmark_gen;
+pub mod code;
+pub mod deghost;
+pub mod func;
+pub mod unimpl;
+pub mod utils;
+
+pub use additions::*;
+pub use benchmark_gen::*;
+pub use code::*;
+pub use deghost::*;
+pub use func::*;
+pub use unimpl::*;
+pub use utils::*;
+
+/// When a flag is set, the corresponding ghost code will not be removed by the
+/// deghost functions.
+#[derive(Clone)]
+#[derive(Args)]
+pub struct DeghostMode {
+    #[clap(long, help = "Compare requires")]
+    pub requires: bool,
+    #[clap(long, help = "Compare ensures")]
+    pub ensures: bool,
+    #[clap(long, help = "Compare invariants")]
+    pub invariants: bool,
+    #[clap(long, help = "Compare spec functions")]
+    pub spec: bool,
+    #[clap(long, help = "Compare asserts")]
+    pub asserts: bool,
+    #[clap(long, help = "Compare asserts with annotations(e.g. #[warn(llm_do_not_change)])")]
+    pub asserts_anno: bool,
+    #[clap(long, help = "Compare decreases")]
+    pub decreases: bool,
+    #[clap(long, help = "Compare assumes")]
+    pub assumes: bool,
+}
+
+impl DeghostMode {
+    pub fn replace_with(&mut self, other: &DeghostMode) {
+        self.requires = other.requires;
+        self.ensures = other.ensures;
+        self.invariants = other.invariants;
+        self.spec = other.spec;
+        self.asserts = other.asserts;
+        self.asserts_anno = other.asserts_anno;
+        self.decreases = other.decreases;
+        self.assumes = other.assumes;
+    }
+}
+
+/// By default, all flags are set to false so that all ghost code will be removed.
+impl Default for DeghostMode {
+    fn default() -> Self {
+        Self {
+            requires: false,
+            ensures: false,
+            invariants: false,
+            spec: false,
+            asserts: false,
+            asserts_anno: false,
+            decreases: false,
+            assumes: false,
+        }
+    }
+}

utils/lynette/source/lynette/src/main.rs

@@ -8,23 +8,7 @@ use std::path::PathBuf;
 use std::process;
 use syn_verus::{FnArg, FnArgKind, Type};
 
-mod additions;
-mod benchmark_gen;
-mod code;
-mod deghost;
-mod func;
-//mod merge;
-mod unimpl;
-mod utils;
-
-use crate::additions::*;
-use crate::benchmark_gen::*;
-use crate::code::*;
-use crate::deghost::*;
-use crate::func::*;
-//use crate::merge::*;
-use crate::unimpl::*;
-use crate::utils::*;
+use lynette::*;
 
 /// Parse a string of ranges in the format of a-b,c-d,e into a vector of ranges.
 fn parse_ranges(
@@ -162,62 +146,10 @@ struct DetectNLArgs {
     sig: bool,
 }
 
-/// When a flag is set, the corresponding ghost code will not be removed by the
-/// deghost functions.
-#[derive(Clone)]
-#[derive(Args)]
-pub struct DeghostMode {
-    #[clap(long, help = "Compare requires")]
-    requires: bool,
-    #[clap(long, help = "Compare ensures")]
-    ensures: bool,
-    #[clap(long, help = "Compare invariants")]
-    invariants: bool,
-    #[clap(long, help = "Compare spec functions")]
-    spec: bool,
-    #[clap(long, help = "Compare asserts")]
-    asserts: bool,
-    #[clap(long, help = "Compare asserts with annotations(e.g. #[warn(llm_do_not_change)])")]
-    asserts_anno: bool,
-    #[clap(long, help = "Compare decreases")]
-    decreases: bool,
-    #[clap(long, help = "Compare assumes")]
-    assumes: bool,
-}
-
-impl DeghostMode {
-    pub fn replace_with(&mut self, other: &DeghostMode) {
-        self.requires = other.requires;
-        self.ensures = other.ensures;
-        self.invariants = other.invariants;
-        self.spec = other.spec;
-        self.asserts = other.asserts;
-        self.asserts_anno = other.asserts_anno;
-        self.decreases = other.decreases;
-        self.assumes = other.assumes;
-    }
-}
-
 thread_local! {
     static DEGHOST_MODE_OPT: RefCell<DeghostMode> = RefCell::new(DeghostMode::default());
 }
 
-/// By default, all flags are set to false so that all ghost code will be removed.
-impl Default for DeghostMode {
-    fn default() -> Self {
-        Self {
-            requires: false,
-            ensures: false,
-            invariants: false,
-            spec: false,
-            asserts: false,
-            asserts_anno: false,
-            decreases: false,
-            assumes: false,
-        }
-    }
-}
-
 #[derive(Args)]
 struct AllowedAdditionsArgs {
     #[clap(help = "Path for original file")]