From 494ffd0aa343a5fc086b88f1882c9d42c8475ea7 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Tue, 30 Apr 2024 01:26:24 +0200
Subject: [PATCH] clippy: Fix if_not_else
---
rr_frontend/.cargo/config.toml | 1 -
rr_frontend/radium/src/code.rs | 6 +++---
rr_frontend/radium/src/specs.rs | 6 +++++-
.../src/bin/refinedrust-rustc.rs | 17 ++++++++-------
rr_frontend/translation/src/function_body.rs | 9 +++++---
.../translation/src/spec_parsers/mod.rs | 21 +++++++++++--------
6 files changed, 35 insertions(+), 25 deletions(-)
diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index b4202e24..aa262952 100644
--- a/rr_frontend/.cargo/config.toml
+++ b/rr_frontend/.cargo/config.toml
@@ -32,7 +32,6 @@ rustflags = [
"-Aclippy::string_lit_as_bytes",
# clippy::pedantic
- "-Aclippy::if_not_else",
"-Aclippy::inefficient_to_string",
"-Aclippy::items_after_statements",
"-Aclippy::manual_let_else",
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index c4caa2ba..6f76d699 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -1097,10 +1097,10 @@ impl<'def> Function<'def> {
if !self.spec.coq_params.is_empty() {
write!(f, "intros")?;
for param in &self.spec.coq_params {
- if !param.implicit {
- write!(f, " {}", param.name)?;
- } else {
+ if param.implicit {
write!(f, " ?")?;
+ } else {
+ write!(f, " {}", param.name)?;
}
}
writeln!(f, ";")?;
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 37d6cac5..58dd499d 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -2852,7 +2852,11 @@ impl<'def> FunctionSpecBuilder<'def> {
}
fn ensure_coq_bound(&self, name: &str) -> Result<(), String> {
- if !self.coq_names.contains(name) { Err(format!("Unbound Coq name {} ", name)) } else { Ok(()) }
+ if !self.coq_names.contains(name) {
+ return Err(format!("Unbound Coq name {} ", name));
+ }
+
+ Ok(())
}
fn ensure_coq_not_bound(&self, name: &CoqName) -> Result<(), String> {
diff --git a/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs b/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
index b2052170..7dfaa212 100644
--- a/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
+++ b/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
@@ -128,17 +128,18 @@ impl rustc_driver::Callbacks for RRCompilerCalls {
_: &rustc_interface::interface::Compiler,
queries: &'tcx rustc_interface::Queries<'tcx>,
) -> Compilation {
- if !rrconfig::no_verify() {
- // Analyze the crate and inspect the types under the cursor.
- queries.global_ctxt().unwrap().enter(|tcx| {
- analyze(tcx);
- });
- Compilation::Stop
- } else {
+ if rrconfig::no_verify() {
// TODO: We also need this to properly compile deps.
// However, for deps I'd ideally anyways have be_rustc??
- Compilation::Continue
+ return Compilation::Continue;
}
+
+ // Analyze the crate and inspect the types under the cursor.
+ queries.global_ctxt().unwrap().enter(|tcx| {
+ analyze(tcx);
+ });
+
+ Compilation::Stop
}
}
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index f03dcf04..8f97df8f 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -2456,13 +2456,16 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// before executing the assignment, first enforce dynamic inclusions
info!("Generating dynamic inclusions {:?}", incls);
let mut stmt_annots = Vec::new();
+
for (r1, r2, p) in &incls {
- if !incls.contains(&(*r2, *r1, *p)) {
- self.generate_dyn_inclusion(&mut stmt_annots, *r1, *r2, *p);
- } else {
+ if incls.contains(&(*r2, *r1, *p)) {
warn!("Skipping impossible dynamic inclusion {:?} ⊑ {:?} at {:?}", r1, r2, p);
+ continue;
}
+
+ self.generate_dyn_inclusion(&mut stmt_annots, *r1, *r2, *p);
}
+
stmt_annots
}
diff --git a/rr_frontend/translation/src/spec_parsers/mod.rs b/rr_frontend/translation/src/spec_parsers/mod.rs
index 44ac305c..34562aa9 100644
--- a/rr_frontend/translation/src/spec_parsers/mod.rs
+++ b/rr_frontend/translation/src/spec_parsers/mod.rs
@@ -57,17 +57,20 @@ where
let pos = input.pos().unwrap();
let args: parse::Punctuated<parse::LitStr, MToken![,]> =
parse::Punctuated::<_, _>::parse_terminated(input, meta)?;
+
if args.len() != 2 {
- Err(parse::ParseError::OtherErr(pos, "Expected exactly two arguments to rr::shim".to_string()))
- } else {
- let args: Vec<_> = args.into_iter().collect();
- let x = args[0].value();
- let y = args[1].value();
- Ok(Self {
- code_name: x,
- spec_name: y,
- })
+ return Err(parse::ParseError::OtherErr(
+ pos,
+ "Expected exactly two arguments to rr::shim".to_string(),
+ ));
}
+
+ let args: Vec<_> = args.into_iter().collect();
+
+ Ok(Self {
+ code_name: args[0].value(),
+ spec_name: args[1].value(),
+ })
}
}
--
GitLab