diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index 504e2b54482020ed625554ef89f423d5c940cb5d..47cdbc7cbe1d1458ee3ae3e93af667656fb5896d 100644
--- a/rr_frontend/.cargo/config.toml
+++ b/rr_frontend/.cargo/config.toml
@@ -34,7 +34,6 @@ rustflags = [
# clippy::restriction
"-Aclippy::non_ascii_literal",
"-Aclippy::panic_in_result_fn",
- "-Aclippy::str_to_string",
"-Aclippy::string_to_string",
"-Aclippy::tests_outside_test_module",
"-Aclippy::unneeded_field_pattern",
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index aec86351ea8bb00586e2dfba0be11a6470fe7953..60a882333b510ba25dea9e085797798072016270 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -113,13 +113,13 @@ impl RustType {
let typarams: Vec<_> = as_use.ty_params.iter().map(|ty| Self::of_type(ty, env)).collect();
let ty_name = if is_raw { def.plain_ty_name() } else { def.public_type_name() };
- Self::Lit(vec![ty_name.to_string()], typarams)
+ Self::Lit(vec![ty_name.to_owned()], typarams)
},
Type::Enum(ae_use) => {
let typarams: Vec<_> = ae_use.ty_params.iter().map(|ty| Self::of_type(ty, env)).collect();
- Self::Lit(vec![ae_use.def.public_type_name().to_string()], typarams)
+ Self::Lit(vec![ae_use.def.public_type_name().to_owned()], typarams)
},
Type::LiteralParam(lit) => Self::TyVar(lit.rust_name.clone()),
@@ -139,7 +139,7 @@ impl RustType {
panic!("RustType::of_type: cannot translate Never type");
},
- Type::RawPtr => Self::Lit(vec!["alias_ptr_t".to_string()], vec![]),
+ Type::RawPtr => Self::Lit(vec!["alias_ptr_t".to_owned()], vec![]),
}
}
}
@@ -737,11 +737,11 @@ impl FunctionCodeBuilder {
}
pub fn add_argument(&mut self, name: &str, st: SynType) {
- self.stack_layout.insert_arg(name.to_string(), st);
+ self.stack_layout.insert_arg(name.to_owned(), st);
}
pub fn add_local(&mut self, name: &str, st: SynType) {
- self.stack_layout.insert_local(name.to_string(), st);
+ self.stack_layout.insert_local(name.to_owned(), st);
}
pub fn add_basic_block(&mut self, index: usize, bb: Stmt) {
@@ -1113,8 +1113,8 @@ impl<'def> FunctionBuilder<'def> {
let code_builder = FunctionCodeBuilder::new();
let spec_builder = FunctionSpecBuilder::new();
FunctionBuilder {
- function_name: name.to_string(),
- spec_name: spec_name.to_string(),
+ function_name: name.to_owned(),
+ spec_name: spec_name.to_owned(),
other_functions: Vec::new(),
generic_types: Vec::new(),
generic_lifetimes: Vec::new(),
@@ -1161,7 +1161,7 @@ impl<'def> FunctionBuilder<'def> {
/// Add a manual tactic used for a sidecondition proof.
pub fn add_manual_tactic(&mut self, tac: &str) {
- self.tactics.push(tac.to_string());
+ self.tactics.push(tac.to_owned());
}
/// Add a generic type used by this function.
diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index 42476ff37d68153abfe713612b87692147fe7cae..6890e5e6f6a523f2d23885a8ab1c0fb013cf4dbb 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -26,7 +26,7 @@ pub struct Path(String);
impl Path {
#[must_use]
pub fn new(path: &str) -> Self {
- Self(path.to_string())
+ Self(path.to_owned())
}
#[must_use]
@@ -46,7 +46,7 @@ impl Module {
#[must_use]
pub fn new(name: &str) -> Self {
Self {
- name: name.to_string(),
+ name: name.to_owned(),
path: None,
}
}
@@ -54,7 +54,7 @@ impl Module {
#[must_use]
pub fn new_with_path(name: &str, path: Path) -> Self {
Self {
- name: name.to_string(),
+ name: name.to_owned(),
path: Some(path),
}
}
@@ -212,7 +212,7 @@ pub type Pattern = String;
fn fmt_prod(v: &Vec<Type>) -> String {
match v.as_slice() {
- [] => "unit".to_string(),
+ [] => "unit".to_owned(),
[t] => t.to_string(),
_ => format!("({})%type", display_list!(v, " * ")),
}
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index bd0ead242111bb33ae35320c32733f2540f76c63..21300078fd5674176c00d574af29a20ba1bf3532 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -32,7 +32,7 @@ impl<'def> TypeWithRef<'def> {
#[must_use]
pub fn make_unit() -> Self {
- TypeWithRef(Type::Unit, "()".to_string())
+ TypeWithRef(Type::Unit, "()".to_owned())
}
#[must_use]
@@ -238,7 +238,7 @@ impl SynType {
Self::Literal(ca) => {
let rhs = format!("{}", ca);
- Layout::Literal(coq::AppTerm::new("use_layout_alg'".to_string(), vec![rhs]))
+ Layout::Literal(coq::AppTerm::new("use_layout_alg'".to_owned(), vec![rhs]))
},
Self::Var(i) => {
@@ -273,12 +273,12 @@ impl SynType {
Self::Ptr | Self::FnPtr => OpType::PtrOp,
Self::Untyped(ly) => OpType::UntypedOp(ly.clone()),
- Self::Unit => OpType::StructOp(coq::AppTerm::new_lhs("unit_sl".to_string()), Vec::new()),
+ Self::Unit => OpType::StructOp(coq::AppTerm::new_lhs("unit_sl".to_owned()), Vec::new()),
Self::Never => OpType::UntypedOp(Layout::UnitLayout),
Self::Literal(ca) => {
let rhs = format!("{}", ca);
- OpType::Literal(coq::AppTerm::new("use_op_alg'".to_string(), vec![rhs]))
+ OpType::Literal(coq::AppTerm::new("use_op_alg'".to_owned(), vec![rhs]))
},
Self::Var(i) => {
@@ -667,7 +667,7 @@ impl<'def> Type<'def> {
},
Self::Var(_i) => {
- s.insert("RAW".to_string());
+ s.insert("RAW".to_owned());
},
}
}
@@ -696,7 +696,7 @@ impl<'def> Type<'def> {
},
Self::Var(_) => {
- s.insert("RAW".to_string());
+ s.insert("RAW".to_owned());
},
}
}
@@ -1542,7 +1542,7 @@ impl<'def> AbstractStruct<'def> {
pub fn public_rt_def_name(&self) -> String {
match &self.invariant {
Some(inv) => inv.rt_def_name(),
- None => self.plain_rt_def_name().to_string(),
+ None => self.plain_rt_def_name().to_owned(),
}
}
@@ -1580,10 +1580,10 @@ impl<'def> AbstractStruct<'def> {
#[must_use]
pub fn make_literal_type(&self) -> LiteralType {
LiteralType {
- rust_name: Some(self.name().to_string()),
- type_term: self.public_type_name().to_string(),
+ rust_name: Some(self.name().to_owned()),
+ type_term: self.public_type_name().to_owned(),
refinement_type: coq::Type::Literal(self.public_rt_def_name()),
- syn_type: SynType::Literal(self.sls_def_name().to_string()),
+ syn_type: SynType::Literal(self.sls_def_name().to_owned()),
}
}
}
@@ -1621,7 +1621,7 @@ impl<'def> VariantBuilder<'def> {
.collect();
let rfn_type = coq::Type::PList(
- "place_rfn".to_string(),
+ "place_rfn".to_owned(),
subst_fields.iter().map(|(_, t)| t.get_rfn_type(&[])).collect(),
);
@@ -1662,7 +1662,7 @@ impl<'def> VariantBuilder<'def> {
/// Append a field to the struct def.
pub fn add_field(&mut self, name: &str, ty: Type<'def>) {
- self.fields.push((name.to_string(), ty));
+ self.fields.push((name.to_owned(), ty));
}
}
@@ -1768,7 +1768,7 @@ impl<'def> AbstractStructUse<'def> {
let inv = &def.invariant;
if self.is_raw() || inv.is_none() {
- let rfn_type = def.plain_rt_def_name().to_string();
+ let rfn_type = def.plain_rt_def_name().to_owned();
let applied = coq::AppTerm::new(rfn_type, rfn_instantiations);
applied.to_string()
} else {
@@ -1794,7 +1794,7 @@ impl<'def> AbstractStructUse<'def> {
// use_struct_layout_alg' ([my_spec] [params])
let specialized_spec = format!("({})", coq::AppTerm::new(def.sls_def_name(), param_sts));
- coq::AppTerm::new("use_struct_layout_alg'".to_string(), vec![specialized_spec]).to_string()
+ coq::AppTerm::new("use_struct_layout_alg'".to_owned(), vec![specialized_spec]).to_string()
}
#[must_use]
@@ -1830,7 +1830,7 @@ impl<'def> AbstractStructUse<'def> {
}
// TODO generates too many apps
- let specialized_spec = coq::AppTerm::new(def.st_def_name().to_string(), param_sts);
+ let specialized_spec = coq::AppTerm::new(def.st_def_name().to_owned(), param_sts);
SynType::Literal(format!("{}", specialized_spec))
}
@@ -2070,14 +2070,14 @@ impl<'def> AbstractEnum<'def> {
// TODO: probably should build this up modularly over the fields
let mut v: Vec<_> = self.ty_params.iter().map(|p| format!("(ty_lfts {})", p.type_term)).collect();
- v.push("[]".to_string());
+ v.push("[]".to_owned());
format!("{}", v.join(" ++ "))
}
fn generate_wf_elctx(&self) -> String {
// TODO: probably should build this up modularly over the fields
let mut v: Vec<_> = self.ty_params.iter().map(|p| format!("(ty_wf_E {})", p.type_term)).collect();
- v.push("[]".to_string());
+ v.push("[]".to_owned());
format!("{}", v.join(" ++ "))
}
@@ -2258,10 +2258,10 @@ impl<'def> AbstractEnum<'def> {
#[must_use]
pub fn make_literal_type(&self) -> LiteralType {
LiteralType {
- rust_name: Some(self.name().to_string()),
- type_term: self.public_type_name().to_string(),
- refinement_type: coq::Type::Literal(self.public_rt_def_name().to_string()),
- syn_type: SynType::Literal(self.els_def_name().to_string()),
+ rust_name: Some(self.name().to_owned()),
+ type_term: self.public_type_name().to_owned(),
+ refinement_type: coq::Type::Literal(self.public_rt_def_name().to_owned()),
+ syn_type: SynType::Literal(self.els_def_name().to_owned()),
}
}
}
@@ -2337,7 +2337,7 @@ impl<'def> EnumBuilder<'def> {
variant: Option<&'def AbstractStruct<'def>>,
discriminant: i128,
) {
- self.variants.push((name.to_string(), variant, discriminant));
+ self.variants.push((name.to_owned(), variant, discriminant));
}
}
@@ -2399,7 +2399,7 @@ impl<'def> AbstractEnumUse<'def> {
// use_struct_layout_alg' ([my_spec] [params])
let specialized_spec = format!("({})", coq::AppTerm::new(self.def.els_def_name.clone(), param_sts));
- coq::AppTerm::new("use_enum_layout_alg'".to_string(), vec![specialized_spec]).to_string()
+ coq::AppTerm::new("use_enum_layout_alg'".to_owned(), vec![specialized_spec]).to_string()
}
/// Generate a term for the enum layout spec (of type `enum_layout_spec`).
@@ -2693,7 +2693,7 @@ impl<'def> FunctionSpec<'def> {
let mut v = v.into_iter().peekable();
if v.peek().is_none() {
- return ("_".to_string(), coq::Type::Literal("unit".to_string()));
+ return ("_".to_owned(), coq::Type::Literal("unit".to_owned()));
}
let mut pattern = String::with_capacity(100);
@@ -2816,7 +2816,7 @@ impl<'def> FunctionSpecBuilder<'def> {
fn push_coq_name(&mut self, name: &coq::Name) {
if let coq::Name::Named(name) = &name {
- self.coq_names.insert(name.to_string());
+ self.coq_names.insert(name.to_owned());
}
}
@@ -2856,7 +2856,7 @@ impl<'def> FunctionSpecBuilder<'def> {
return Ok(());
}
}
- Err("could not find name".to_string())
+ Err("could not find name".to_owned())
}
fn ensure_coq_bound(&self, name: &str) -> Result<(), String> {
@@ -2966,7 +2966,7 @@ impl<'def> FunctionSpecBuilder<'def> {
/// Set the return type of the function
pub fn set_ret_type(&mut self, ret: TypeWithRef<'def>) -> Result<(), String> {
if self.ret.is_some() {
- return Err("Re-definition of return type".to_string());
+ return Err("Re-definition of return type".to_owned());
}
self.ret = Some(ret);
Ok(())
@@ -2995,8 +2995,8 @@ impl<'def> FunctionSpecBuilder<'def> {
FunctionSpec {
extra_link_assum: self.extra_link_assum,
- function_name: name.to_string(),
- spec_name: spec_name.to_string(),
+ function_name: name.to_owned(),
+ spec_name: spec_name.to_owned(),
coq_params: self.coq_params,
lifetimes: self.lifetimes,
params: self.params,
diff --git a/rr_frontend/refinedrust_frontend/src/bin/cargo-refinedrust.rs b/rr_frontend/refinedrust_frontend/src/bin/cargo-refinedrust.rs
index dddd126e709a212046800abe49bd16c238662479..2a0fd6081198eb1975e4b49ccc04d94c9860e503 100644
--- a/rr_frontend/refinedrust_frontend/src/bin/cargo-refinedrust.rs
+++ b/rr_frontend/refinedrust_frontend/src/bin/cargo-refinedrust.rs
@@ -40,7 +40,7 @@ where
let command = rrconfig::cargo_command();
// TODO: If we're using workspaces, we should figure out the right dir for the workspace
- let cargo_target_path = env::var("CARGO_TARGET_DIR").unwrap_or_else(|_| "target".to_string());
+ let cargo_target_path = env::var("CARGO_TARGET_DIR").unwrap_or_else(|_| "target".to_owned());
let cargo_target = PathBuf::from(cargo_target_path.to_string());
let maybe_output_dir = rrconfig::output_dir();
@@ -48,7 +48,7 @@ where
if let Some(old_output_dir) = maybe_output_dir {
output_dir = old_output_dir;
} else {
- output_dir = [cargo_target_path, "verify".to_string()].into_iter().collect();
+ output_dir = [cargo_target_path, "verify".to_owned()].into_iter().collect();
}
let exit_status = Command::new(cargo_path)
diff --git a/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs b/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
index a87e66e9b04c284d600842e1685445fbdbb52454..1d3c3bdbbd0596c2de4ef076b3210caa3f46d9e1 100644
--- a/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
+++ b/rr_frontend/refinedrust_frontend/src/bin/refinedrust-rustc.rs
@@ -198,7 +198,7 @@ fn main() {
debug!("rustc arguments: {:?}", rustc_args);
let exit_code = rustc_driver::catch_with_exit_code(move || {
- if rustc_args.get(1) == Some(&"-vV".to_string()) {
+ if rustc_args.get(1) == Some(&"-vV".to_owned()) {
// When cargo queries the verbose rustc version,
// also print the RR version to stdout.
// This ensures that the cargo build cache is
@@ -232,7 +232,7 @@ fn main() {
rustc_args.push("-Zidentify-regions=yes".to_owned());
}
if rrconfig::dump_borrowck_info() {
- rustc_args.push("-Znll-facts=yes".to_string());
+ rustc_args.push("-Znll-facts=yes".to_owned());
rustc_args.push(format!(
"-Znll-facts-dir={}",
rrconfig::log_dir()
diff --git a/rr_frontend/translation/src/environment/borrowck/regions.rs b/rr_frontend/translation/src/environment/borrowck/regions.rs
index cc1743623bae31a61e2ffff5f9c2ddb6a3d01fa9..b4ae8059a8790b9ad9b48101f4b7bc483424351e 100644
--- a/rr_frontend/translation/src/environment/borrowck/regions.rs
+++ b/rr_frontend/translation/src/environment/borrowck/regions.rs
@@ -59,32 +59,32 @@ impl PlaceRegions {
mir::ProjectionElem::Deref => Err(PlaceRegionsError::Unsupported(
"determining the region of a dereferentiation is \
not supported"
- .to_string(),
+ .to_owned(),
)),
mir::ProjectionElem::Index(_) => Err(PlaceRegionsError::Unsupported(
"determining the region of array indexing is \
not supported"
- .to_string(),
+ .to_owned(),
)),
mir::ProjectionElem::ConstantIndex { .. } => Err(PlaceRegionsError::Unsupported(
"determining the region of constant indexing is \
not supported"
- .to_string(),
+ .to_owned(),
)),
mir::ProjectionElem::Subslice { .. } => Err(PlaceRegionsError::Unsupported(
"determining the region of a subslice is \
not supported"
- .to_string(),
+ .to_owned(),
)),
mir::ProjectionElem::Downcast(_, _) => Err(PlaceRegionsError::Unsupported(
"determining the region of a downcast is \
not supported"
- .to_string(),
+ .to_owned(),
)),
mir::ProjectionElem::OpaqueCast(_) => Err(PlaceRegionsError::Unsupported(
"determining the region of an opaque cast is \
not supported"
- .to_string(),
+ .to_owned(),
)),
})
.collect::<Result<_, _>>()?;
diff --git a/rr_frontend/translation/src/environment/polonius_info.rs b/rr_frontend/translation/src/environment/polonius_info.rs
index 177d04eb28eaa72052e110166dc2ab7a0a4d0b38..1db667ce2e74000f8cd714de1021c35a64f5ea65 100644
--- a/rr_frontend/translation/src/environment/polonius_info.rs
+++ b/rr_frontend/translation/src/environment/polonius_info.rs
@@ -403,7 +403,7 @@ fn get_borrowed_places<'a, 'tcx: 'a>(
mir::Rvalue::Cast(..) => {
// all other loan-casts are unsupported
Err(PoloniusInfoError::LoanInUnsupportedStatement(
- "cast statements that create loans are not supported".to_string(),
+ "cast statements that create loans are not supported".to_owned(),
*location,
))
},
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index 16cd3981cb5bbf0bb96a2c206bd3b0ec980b7b17..c1617c511ab252463dc0b6a998467c9a8456d5f5 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -861,7 +861,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
used_names.insert(mir_name);
name
} else {
- let mut name = "__".to_string();
+ let mut name = "__".to_owned();
name.push_str(&local.index().to_string());
name
}
@@ -889,7 +889,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
// used already
// TODO: find better solution
if !used_names.contains(name.as_str()) {
- return Some(name.as_str().to_string());
+ return Some(name.as_str().to_owned());
}
}
}
@@ -943,7 +943,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
let mut return_synty = radium::SynType::Unit; // default
let mut fn_locals = Vec::new();
let mut opt_return_name =
- Err(TranslationError::UnknownError("could not find local for return value".to_string()));
+ Err(TranslationError::UnknownError("could not find local for return value".to_owned()));
let mut used_names = HashSet::new();
let mut arg_tys = Vec::new();
@@ -1178,7 +1178,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
self.format_atomic_region(r2),
),
s: Box::new(translated_bb),
- why: Some("initialization".to_string()),
+ why: Some("initialization".to_owned()),
};
}
self.translated_fn.code.add_basic_block(initial_bb_idx.as_usize(), translated_bb);
@@ -1308,7 +1308,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
},
ty::GenericArgKind::Const(_c) => {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does not support const generics".to_string(),
+ description: "RefinedRust does not support const generics".to_owned(),
});
},
}
@@ -1345,7 +1345,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
.lookup_function_spec_name(did)
.ok_or_else(|| TranslationError::UnknownProcedure(format!("{:?}", did)))?;
- let mut mangled_name = name.to_string();
+ let mut mangled_name = name.to_owned();
let mut translated_params = Vec::new();
// TODO: maybe come up with some better way to generate names
@@ -1422,7 +1422,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
);
self.collected_procedures
- .insert(tup, (loc_name.clone(), spec_name.to_string(), translated_params, syntypes));
+ .insert(tup, (loc_name.clone(), spec_name.to_owned(), translated_params, syntypes));
trace!("leave register_use_procedure");
Ok(loc_name)
@@ -1625,7 +1625,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
},
// TODO handle FnPtr, closure
_ => Err(TranslationError::Unimplemented {
- description: "implement function pointers".to_string(),
+ description: "implement function pointers".to_owned(),
}),
}
},
@@ -1645,12 +1645,12 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
},
// TODO handle FnPtr, closure
_ => Err(TranslationError::Unimplemented {
- description: "implement function pointers".to_string(),
+ description: "implement function pointers".to_owned(),
}),
}
},
ConstantKind::Unevaluated(_, _) => Err(TranslationError::Unimplemented {
- description: "implement ConstantKind::Unevaluated".to_string(),
+ description: "implement ConstantKind::Unevaluated".to_owned(),
}),
}
}
@@ -2008,7 +2008,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
let cont_stmt = radium::Stmt::with_annotations(
cont_stmt,
post_stmt_annots,
- &Some("post_function_call".to_string()),
+ &Some("post_function_call".to_owned()),
);
// assign stmt with call; then jump to bb
@@ -2021,7 +2021,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
let annotated_rhs = radium::Expr::with_optional_annotation(
call_expr,
rhs_annots,
- Some("function_call".to_string()),
+ Some("function_call".to_owned()),
);
let assign_stmt = radium::Stmt::Assign {
ot,
@@ -2032,7 +2032,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
radium::Stmt::with_annotations(
assign_stmt,
pre_stmt_annots,
- &Some("function_call".to_string()),
+ &Some("function_call".to_owned()),
)
},
None => {
@@ -2060,7 +2060,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
0 => {
return Err(TranslationError::UnsupportedFeature {
description: "RefinedRust does currently not support unconstrained lifetime"
- .to_string(),
+ .to_owned(),
});
},
1 => {
@@ -2080,7 +2080,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
}
}
- let stmt = radium::Stmt::with_annotations(stmt, stmt_annots, &Some("function_call".to_string()));
+ let stmt = radium::Stmt::with_annotations(stmt, stmt_annots, &Some("function_call".to_owned()));
Ok(stmt)
}
@@ -2180,7 +2180,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
let translated_ty = self.ty_translator.translate_type(ty)?;
let radium::Type::Int(it) = translated_ty else {
return Err(TranslationError::UnknownError(
- "SwitchInt switching on non-integer type".to_string(),
+ "SwitchInt switching on non-integer type".to_owned(),
));
};
@@ -2244,11 +2244,11 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
TerminatorKind::Unreachable => Ok(radium::Stmt::Stuck),
TerminatorKind::UnwindResume => Err(TranslationError::Unimplemented {
- description: "implement UnwindResume".to_string(),
+ description: "implement UnwindResume".to_owned(),
}),
TerminatorKind::UnwindTerminate(_) => Err(TranslationError::Unimplemented {
- description: "implement UnwindTerminate".to_string(),
+ description: "implement UnwindTerminate".to_owned(),
}),
TerminatorKind::GeneratorDrop
@@ -2275,7 +2275,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
cont_stmt = radium::Stmt::Annot {
a: radium::Annotation::EndLft(self.format_atomic_region(&lft)),
s: Box::new(cont_stmt),
- why: Some("endlft".to_string()),
+ why: Some("endlft".to_owned()),
};
}
}
@@ -2751,13 +2751,13 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
cont_stmt = radium::Stmt::with_annotations(
cont_stmt,
post_stmt_annots,
- &Some("post-assignment".to_string()),
+ &Some("post-assignment".to_owned()),
);
let translated_val = radium::Expr::with_optional_annotation(
self.translate_rvalue(loc, val)?,
expr_annot,
- Some("assignment".to_string()),
+ Some("assignment".to_owned()),
);
let translated_place = self.translate_place(plc)?;
let synty = self.ty_translator.translate_type_to_syn_type(plc_ty.ty)?;
@@ -2771,17 +2771,17 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
cont_stmt = radium::Stmt::with_annotations(
cont_stmt,
pre_stmt_annots,
- &Some("assignment".to_string()),
+ &Some("assignment".to_owned()),
);
cont_stmt = radium::Stmt::with_annotations(
cont_stmt,
borrow_annots,
- &Some("borrow".to_string()),
+ &Some("borrow".to_owned()),
);
cont_stmt = radium::Stmt::with_annotations(
cont_stmt,
composite_annots,
- &Some("composite".to_string()),
+ &Some("composite".to_owned()),
);
}
},
@@ -2789,7 +2789,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
StatementKind::Deinit(_) => {
// TODO: find out where this is emitted
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support Deinit".to_string(),
+ description: "RefinedRust does currently not support Deinit".to_owned(),
});
},
@@ -2800,7 +2800,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
StatementKind::Intrinsic(_intrinsic) => {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support Intrinsic".to_string(),
+ description: "RefinedRust does currently not support Intrinsic".to_owned(),
});
},
@@ -2815,7 +2815,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
} => {
// TODO
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support SetDiscriminant".to_string(),
+ description: "RefinedRust does currently not support SetDiscriminant".to_owned(),
});
},
@@ -2849,7 +2849,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// TODO: figure out what to do with this
// arises in match lowering
Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support shallow borrows".to_string(),
+ description: "RefinedRust does currently not support shallow borrows".to_owned(),
})
},
BorrowKind::Mut { .. } => {
@@ -2925,13 +2925,13 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
BinOp::Sub => Ok(radium::Binop::CheckedSubOp),
BinOp::Mul => Ok(radium::Binop::CheckedMulOp),
BinOp::Shl => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support checked Shl".to_string(),
+ description: "RefinedRust does currently not support checked Shl".to_owned(),
}),
BinOp::Shr => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support checked Shr".to_string(),
+ description: "RefinedRust does currently not support checked Shr".to_owned(),
}),
_ => Err(TranslationError::UnknownError(
- "unexpected checked binop that is not Add, Sub, Mul, Shl, or Shr".to_string(),
+ "unexpected checked binop that is not Add, Sub, Mul, Shl, or Shr".to_owned(),
)),
}
}
@@ -2943,7 +2943,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
ty::TyKind::Bool => Ok(radium::Unop::NotBoolOp),
ty::TyKind::Int(_) | ty::TyKind::Uint(_) => Ok(radium::Unop::NotIntOp),
_ => Err(TranslationError::UnknownError(
- "application of UnOp::Not to non-{Int, Bool}".to_string(),
+ "application of UnOp::Not to non-{Int, Bool}".to_owned(),
)),
},
UnOp::Neg => Ok(radium::Unop::NegOp),
@@ -3085,7 +3085,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// TODO: SizeOf
Err(TranslationError::UnsupportedFeature {
description: "RefinedRust does currently not support nullary ops (AlignOf, Sizeof)"
- .to_string(),
+ .to_owned(),
})
},
@@ -3290,26 +3290,26 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
},
mir::CastKind::DynStar => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support dyn* cast".to_string(),
+ description: "RefinedRust does currently not support dyn* cast".to_owned(),
}),
mir::CastKind::IntToInt => {
// TODO
Err(TranslationError::Unimplemented {
- description: "RefinedRust does currently not support int-to-int cast".to_string(),
+ description: "RefinedRust does currently not support int-to-int cast".to_owned(),
})
},
mir::CastKind::IntToFloat => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support int-to-float cast".to_string(),
+ description: "RefinedRust does currently not support int-to-float cast".to_owned(),
}),
mir::CastKind::FloatToInt => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support float-to-int cast".to_string(),
+ description: "RefinedRust does currently not support float-to-int cast".to_owned(),
}),
mir::CastKind::FloatToFloat => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support float-to-float cast".to_string(),
+ description: "RefinedRust does currently not support float-to-float cast".to_owned(),
}),
mir::CastKind::PtrToPtr => {
@@ -3435,7 +3435,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
fn translate_fn_def_use(&mut self, ty: Ty<'tcx>) -> Result<radium::Expr, TranslationError> {
let TyKind::FnDef(defid, params) = ty.kind() else {
- return Err(TranslationError::UnknownError("not a FnDef type".to_string()));
+ return Err(TranslationError::UnknownError("not a FnDef type".to_owned()));
};
let key: ty::ParamEnv<'tcx> = self.env.tcx().param_env(self.proc.get_id());
@@ -3591,7 +3591,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
}
},
_ => Err(TranslationError::UnsupportedFeature {
- description: "Unsupported ConstKind".to_string(),
+ description: "Unsupported ConstKind".to_owned(),
}),
}
},
@@ -3668,18 +3668,18 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
ProjectionElem::Index(_v) => {
//TODO
return Err(TranslationError::UnsupportedFeature {
- description: "places: implement index access".to_string(),
+ description: "places: implement index access".to_owned(),
});
},
ProjectionElem::ConstantIndex { .. } => {
//TODO
return Err(TranslationError::UnsupportedFeature {
- description: "places: implement const index access".to_string(),
+ description: "places: implement const index access".to_owned(),
});
},
ProjectionElem::Subslice { .. } => {
return Err(TranslationError::UnsupportedFeature {
- description: "places: implement subslicing".to_string(),
+ description: "places: implement subslicing".to_owned(),
});
},
ProjectionElem::Downcast(_, variant_idx) => {
@@ -3698,18 +3698,18 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
}
} else {
return Err(TranslationError::UnknownError(
- "places: ADT downcasting on non-enum type".to_string(),
+ "places: ADT downcasting on non-enum type".to_owned(),
));
}
} else {
return Err(TranslationError::UnknownError(
- "places: ADT downcasting on non-enum type".to_string(),
+ "places: ADT downcasting on non-enum type".to_owned(),
));
}
},
ProjectionElem::OpaqueCast(_) => {
return Err(TranslationError::UnsupportedFeature {
- description: "places: implement opaque casts".to_string(),
+ description: "places: implement opaque casts".to_owned(),
});
},
};
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 3f8f94d4d48605fc991ce595682d4ef18e40648d..ea63eadb83b0207f890428147407dedf914dc74d 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -131,27 +131,24 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
return None;
}
- match self.env.tcx().visibility(did) {
- // only export public items
- ty::Visibility::Public => {
- let is_method = self.env.tcx().impl_of_method(did).is_some();
- let interned_path = self.get_path_for_shim(did);
+ if self.env.tcx().visibility(did) != ty::Visibility::Public {
+ // don't export
+ return None;
+ }
- let name = type_translator::strip_coq_ident(&self.env.get_item_name(did));
- info!("Found function path {:?} for did {:?} with name {:?}", interned_path, did, name);
+ // only export public items
+ let is_method = self.env.tcx().impl_of_method(did).is_some();
+ let interned_path = self.get_path_for_shim(did);
- Some(shim_registry::FunctionShim {
- path: interned_path,
- is_method,
- name,
- spec_name: spec_name.to_string(),
- })
- },
- ty::Visibility::Restricted(_) => {
- // don't export
- None
- },
- }
+ let name = type_translator::strip_coq_ident(&self.env.get_item_name(did));
+ info!("Found function path {:?} for did {:?} with name {:?}", interned_path, did, name);
+
+ Some(shim_registry::FunctionShim {
+ path: interned_path,
+ is_method,
+ name,
+ spec_name: spec_name.to_owned(),
+ })
}
fn make_shim_trait_method_entry(
@@ -211,7 +208,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
return None;
};
- let method_ident = ident.as_str().to_string();
+ let method_ident = ident.as_str().to_owned();
let name = type_translator::strip_coq_ident(&self.env.get_item_name(did));
trace!("leave make_shim_trait_method_entry (success)");
@@ -220,7 +217,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
method_ident,
for_type,
name,
- spec_name: spec_name.to_string(),
+ spec_name: spec_name.to_owned(),
})
},
ty::Visibility::Restricted(_) => {
@@ -703,8 +700,9 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let (project_name, dune_project_package) = if let Some(dune_package) = &self.dune_package {
(dune_package.to_string(), format!("(package (name {dune_package}))\n"))
} else {
- (stem.to_string(), format!(""))
+ (stem.to_owned(), format!(""))
};
+
write!(
dune_project_file,
"\
@@ -1064,7 +1062,7 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
&vcx.procedure_registry,
&vcx.const_registry,
),
- _ => Err(base::TranslationError::UnknownError("unknown function kind".to_string())),
+ _ => Err(base::TranslationError::UnknownError("unknown function kind".to_owned())),
};
if mode.is_only_spec() {
@@ -1269,7 +1267,7 @@ where
let mut crate_parser = crate_parser::VerboseCrateAttrParser::new();
let crate_spec = crate_parser.parse_crate_attrs(&crate_attrs)?;
- let path_prefix = crate_spec.prefix.unwrap_or_else(|| "refinedrust.examples".to_string());
+ let path_prefix = crate_spec.prefix.unwrap_or_else(|| "refinedrust.examples".to_owned());
info!("Setting Coq path prefix: {:?}", path_prefix);
let package = crate_spec.package;
diff --git a/rr_frontend/translation/src/shim_registry.rs b/rr_frontend/translation/src/shim_registry.rs
index 02696b10fe30965022d9bf9bb1250c8a3c7440dd..f95d03715acd7aafd16bb2e283a9476a33f727f8 100644
--- a/rr_frontend/translation/src/shim_registry.rs
+++ b/rr_frontend/translation/src/shim_registry.rs
@@ -84,8 +84,8 @@ pub struct FunctionShim<'a> {
impl<'a> From<FunctionShim<'a>> for ShimFunctionEntry {
fn from(shim: FunctionShim<'a>) -> Self {
Self {
- path: shim.path.iter().map(|x| (*x).to_string()).collect(),
- kind: if shim.is_method { "method".to_string() } else { "function".to_string() },
+ path: shim.path.iter().map(|x| (*x).to_owned()).collect(),
+ kind: if shim.is_method { "method".to_owned() } else { "function".to_owned() },
name: shim.name,
spec: shim.spec_name,
}
@@ -107,7 +107,7 @@ impl From<TraitMethodImplShim> for ShimTraitMethodImplEntry {
trait_path: shim.trait_path,
method_ident: shim.method_ident,
for_type: shim.for_type,
- kind: "trait_method".to_string(),
+ kind: "trait_method".to_owned(),
name: shim.name,
spec: shim.spec_name,
}
@@ -125,8 +125,8 @@ pub struct AdtShim<'a> {
impl<'a> From<AdtShim<'a>> for ShimAdtEntry {
fn from(shim: AdtShim<'a>) -> Self {
Self {
- path: shim.path.iter().map(|x| (*x).to_string()).collect(),
- kind: "adt".to_string(),
+ path: shim.path.iter().map(|x| (*x).to_owned()).collect(),
+ kind: "adt".to_owned(),
syntype: shim.syn_type,
semtype: shim.sem_type,
rtype: shim.refinement_type,
@@ -261,7 +261,7 @@ impl<'a> ShimRegistry<'a> {
serde_json::Value::Array(arr) => arr,
- _ => return Err("invalid Json format".to_string()),
+ _ => return Err("invalid Json format".to_owned()),
};
for i in v {
@@ -393,7 +393,7 @@ pub fn is_valid_refinedrust_module(f: File) -> Option<String> {
let name = obj.get("refinedrust_name")?;
let name = name.as_str()?;
- Some(name.to_string())
+ Some(name.to_owned())
},
_ => None,
}
diff --git a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
index 4c757f0d582a79c266d283de1a5d2ee810c6052b..59c284917943a5d8516129008f407c08e8c9f9f1 100644
--- a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
@@ -135,7 +135,7 @@ impl EnumSpecParser for VerboseEnumSpecParser {
}
}
if let Some(pattern) = pattern {
- let refinement = refinement.unwrap_or_else(|| "-[]".to_string());
+ let refinement = refinement.unwrap_or_else(|| "-[]".to_owned());
variant_patterns.push((pattern.pat, pattern.args, refinement));
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/mod.rs b/rr_frontend/translation/src/spec_parsers/mod.rs
index eb182e4ad413d9833bc53f740b44c2009fdc5897..b320f99f191cc46fc41b57ce6e769b7d4713874c 100644
--- a/rr_frontend/translation/src/spec_parsers/mod.rs
+++ b/rr_frontend/translation/src/spec_parsers/mod.rs
@@ -40,7 +40,7 @@ pub fn get_export_as_attr(attrs: &[&AttrItem]) -> Result<Vec<String>, String> {
}
}
}
- Err("Did not find export_as annotation".to_string())
+ Err("Did not find export_as annotation".to_owned())
}
/// Parser for getting shim attributes
@@ -62,7 +62,7 @@ where
if args.len() != 2 {
return Err(parse::ParseError::OtherErr(
pos,
- "Expected exactly two arguments to rr::shim".to_string(),
+ "Expected exactly two arguments to rr::shim".to_owned(),
));
}
@@ -92,5 +92,5 @@ pub fn get_shim_attrs(attrs: &[&AttrItem]) -> Result<ShimAnnot, String> {
}
}
}
- Err("Did not find shim annotation".to_string())
+ Err("Did not find shim annotation".to_owned())
}
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 3f32566742659dbbb6bfd28b1157b7682bde52e2..46033b1debc83ed32697bf2a63509e9e2d7b51da 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -65,7 +65,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for LiteralTypeWithRef {
"raw" => {
raw = specs::TypeIsRaw::Yes;
},
- _ => return Err(parse::ParseError::OtherErr(loc.unwrap(), "Unsupported flag".to_string())),
+ _ => return Err(parse::ParseError::OtherErr(loc.unwrap(), "Unsupported flag".to_owned())),
}
}
@@ -323,7 +323,7 @@ pub fn process_coq_literal(s: &str, meta: ParseMeta<'_>) -> (String, specs::Type
literal_tyvars.insert(param.clone());
format!("{}(ty_syn_type {})", &c[1], ¶m.type_term)
},
- None => "ERR".to_string(),
+ None => "ERR".to_owned(),
}
});
let cs = RE_LY_OF.replace_all(&cs, |c: &Captures<'_>| {
@@ -334,7 +334,7 @@ pub fn process_coq_literal(s: &str, meta: ParseMeta<'_>) -> (String, specs::Type
literal_tyvars.insert(param.clone());
format!("{}(use_layout_alg' (ty_syn_type {}))", &c[1], ¶m.type_term)
},
- None => "ERR".to_string(),
+ None => "ERR".to_owned(),
}
});
let cs = RE_TY_OF.replace_all(&cs, |c: &Captures<'_>| {
@@ -356,7 +356,7 @@ pub fn process_coq_literal(s: &str, meta: ParseMeta<'_>) -> (String, specs::Type
literal_lfts.insert(lft.clone());
format!("{}{}", &c[1], lft)
},
- None => "ERR".to_string(),
+ None => "ERR".to_owned(),
}
});
let cs = RE_LIT.replace_all(&cs, |c: &Captures<'_>| format!("{}", &c[1]));
diff --git a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
index 2f20b0de6487f1470847c5d71afbb45115fdd021..0bfa1874c5aee5f2e8705b12ff3d55b93813b4d3 100644
--- a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
@@ -161,7 +161,7 @@ impl<U> parse::Parse<U> for InvariantSpecFlags {
"plain" => Ok(Self(specs::InvariantSpecFlags::Plain)),
"na" => Ok(Self(specs::InvariantSpecFlags::NonAtomic)),
"atomic" => Ok(Self(specs::InvariantSpecFlags::Atomic)),
- _ => Err(parse::ParseError::OtherErr(input.pos().unwrap(), "invalid ADT mode".to_string())),
+ _ => Err(parse::ParseError::OtherErr(input.pos().unwrap(), "invalid ADT mode".to_owned())),
}
}
}
@@ -192,7 +192,7 @@ impl InvariantSpecParser for VerboseInvariantSpecParser {
let mut type_invariants: Vec<specs::TyOwnSpec> = Vec::new();
let mut abstracted_refinement = None;
- let mut rfn_pat = "placeholder_pat".to_string();
+ let mut rfn_pat = "placeholder_pat".to_owned();
let mut rfn_type = coq::Type::Infer;
let mut existentials: Vec<RRParam> = Vec::new();
@@ -255,7 +255,7 @@ impl InvariantSpecParser for VerboseInvariantSpecParser {
let term = IdentOrTerm::parse(&buffer, &meta).map_err(str_err)?;
if abstracted_refinement.is_some() {
- return Err("multiple refines specifications given".to_string());
+ return Err("multiple refines specifications given".to_owned());
}
abstracted_refinement = Some(term.to_string());
},
@@ -278,9 +278,9 @@ impl InvariantSpecParser for VerboseInvariantSpecParser {
let refinement_included = abstracted_refinement.is_some();
let spec = specs::InvariantSpec::new(
- ty_name.to_string(),
+ ty_name.to_owned(),
inv_flags,
- "κ".to_string(),
+ "κ".to_owned(),
rfn_type,
rfn_pat,
existentials.into_iter().map(|a| (a.name, a.ty)).collect(),
diff --git a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
index 52d46912679bc473ee69b17bb8224a67fe80185b..c47b8a2f657b28e3f84d5f210cd5cac00e3f481c 100644
--- a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
@@ -541,7 +541,7 @@ where
ty::ClosureKind::FnMut => {
// wrap the argument in a mutable reference
let post_name = "__γclos";
- builder.spec.add_param(coq::Name::Named(post_name.to_string()), coq::Type::Gname).unwrap();
+ builder.spec.add_param(coq::Name::Named(post_name.to_owned()), coq::Type::Gname).unwrap();
let lft = meta.closure_lifetime.unwrap();
let ref_ty = specs::Type::MutRef(Box::new(tuple), lft);
@@ -561,9 +561,7 @@ where
});
post_term.push(']');
- builder
- .spec
- .add_postcondition(MetaIProp::Observe(post_name.to_string(), post_term).into());
+ builder.spec.add_postcondition(MetaIProp::Observe(post_name.to_owned(), post_term).into());
},
}
Ok(())
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 476d17ef984fbeed2c50127cf5e1066c4b9c7868..42a21451cb37ac4aef66957f778a1071e54b9039 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -118,7 +118,7 @@ impl<'def> TypeTranslationScope<'def> {
let st_term = st_name;
let lit_ty = radium::LiteralTyParam {
- rust_name: p.name.as_str().to_string(),
+ rust_name: p.name.as_str().to_owned(),
type_term: ty_term,
refinement_type: rt_name,
syn_type: st_term,
@@ -129,7 +129,7 @@ impl<'def> TypeTranslationScope<'def> {
_ => {
return Err(TranslationError::UnsupportedFeature {
description: "RefinedRust does currently not support non-type generic arguments"
- .to_string(),
+ .to_owned(),
});
},
},
@@ -155,7 +155,7 @@ impl<'def> TypeTranslationScope<'def> {
ty::GenericArgKind::Const(_c) => {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support const generics".to_string(),
+ description: "RefinedRust does currently not support const generics".to_owned(),
});
},
}
@@ -341,19 +341,19 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
if repr.simd() {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support the SIMD flag".to_string(),
+ description: "RefinedRust does currently not support the SIMD flag".to_owned(),
});
}
if repr.packed() {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support the repr(packed) flag".to_string(),
+ description: "RefinedRust does currently not support the repr(packed) flag".to_owned(),
});
}
if repr.linear() {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support the linear flag".to_string(),
+ description: "RefinedRust does currently not support the linear flag".to_owned(),
});
}
@@ -372,19 +372,19 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
if repr.simd() {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support the SIMD flag".to_string(),
+ description: "RefinedRust does currently not support the SIMD flag".to_owned(),
});
}
if repr.packed() {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support the repr(packed) flag".to_string(),
+ description: "RefinedRust does currently not support the repr(packed) flag".to_owned(),
});
}
if repr.linear() {
return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support the linear flag".to_string(),
+ description: "RefinedRust does currently not support the linear flag".to_owned(),
});
}
@@ -414,8 +414,8 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
None
},
- ty::RegionKind::ReStatic => Some("static".to_string()),
- ty::RegionKind::ReErased => Some("erased".to_string()),
+ ty::RegionKind::ReStatic => Some("static".to_owned()),
+ ty::RegionKind::ReErased => Some("erased".to_owned()),
ty::RegionKind::ReVar(v) => match &translation_state {
TranslationStateInner::InFunction(scope) => {
@@ -512,7 +512,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
if adt.is_box() {
// TODO: for now, Box gets a special treatment and is not accurately
// translated. Reconsider this later on
- return Err(TranslationError::UnknownError("Box is not a proper structlike".to_string()));
+ return Err(TranslationError::UnknownError("Box is not a proper structlike".to_owned()));
}
if adt.is_struct() {
@@ -528,7 +528,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
if adt.is_enum() {
let Some(variant) = variant else {
return Err(TranslationError::UnknownError(
- "a non-downcast enum is not a structlike".to_string(),
+ "a non-downcast enum is not a structlike".to_owned(),
));
};
@@ -540,13 +540,13 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
}
Err(TranslationError::UnsupportedType {
- description: "non-{enum, struct, tuple} ADTs are not supported".to_string(),
+ description: "non-{enum, struct, tuple} ADTs are not supported".to_owned(),
})
},
TyKind::Tuple(args) => self.generate_tuple_use(*args, adt_deps).map(radium::Type::Literal),
- _ => Err(TranslationError::UnknownError("not a structlike".to_string())),
+ _ => Err(TranslationError::UnknownError("not a structlike".to_owned())),
}
}
@@ -609,7 +609,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
let Some(arg_ty) = arg.as_type() else {
return Err(TranslationError::UnsupportedFeature {
description: "RefinedRust does currently not support ADTs with lifetime parameters"
- .to_string(),
+ .to_owned(),
});
};
@@ -764,7 +764,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
if def.is_union() {
Err(TranslationError::Unimplemented {
- description: "union ADTs are not yet supported".to_string(),
+ description: "union ADTs are not yet supported".to_owned(),
})
} else if self.is_struct_definitely_zero_sized(def.did()) == Some(true) {
Ok(())
@@ -883,7 +883,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
// check for representation flags
let repr = Self::get_struct_representation(&adt.repr())?;
- let mut builder = radium::VariantBuilder::new(struct_name.to_string(), repr);
+ let mut builder = radium::VariantBuilder::new(struct_name.to_owned(), repr);
// parse attributes
let outer_attrs = self.env.get_attributes(ty.def_id);
@@ -1057,18 +1057,18 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
/// Get the spec for a built-in enum like `std::option::Option`.
fn get_builtin_enum_spec(&self, did: DefId) -> Option<radium::EnumSpec> {
let option_spec = radium::EnumSpec {
- rfn_type: coq::Type::Literal("_".to_string()),
+ rfn_type: coq::Type::Literal("_".to_owned()),
variant_patterns: vec![
- ("None".to_string(), vec![], "-[]".to_string()),
- ("Some".to_string(), vec!["x".to_string()], "-[x]".to_string()),
+ ("None".to_owned(), vec![], "-[]".to_owned()),
+ ("Some".to_owned(), vec!["x".to_owned()], "-[x]".to_owned()),
],
};
let enum_spec = radium::EnumSpec {
- rfn_type: coq::Type::Literal("_".to_string()),
+ rfn_type: coq::Type::Literal("_".to_owned()),
variant_patterns: vec![
- ("inl".to_string(), vec!["x".to_string()], "-[x]".to_string()),
- ("inr".to_string(), vec!["x".to_string()], "-[x]".to_string()),
+ ("inl".to_owned(), vec!["x".to_owned()], "-[x]".to_owned()),
+ ("inr".to_owned(), vec!["x".to_owned()], "-[x]".to_owned()),
],
};
@@ -1104,16 +1104,16 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
let registry = self.variant_registry.borrow();
let (variant_name, coq_def, variant_def, _, _) = registry.get(&v.def_id).unwrap();
let coq_def = coq_def.get().unwrap();
- let refinement_type = coq_def.plain_rt_def_name().to_string();
+ let refinement_type = coq_def.plain_rt_def_name().to_owned();
// simple optimization: if the variant has no fields, also this constructor gets no arguments
let (variant_args, variant_arg_binders, variant_rfn) = if variant_def.fields.is_empty() {
- (vec![], vec![], "-[]".to_string())
+ (vec![], vec![], "-[]".to_owned())
} else {
let args =
vec![coq::Param::new(coq::Name::Unnamed, coq::Type::Literal(refinement_type), false)];
- (args, vec!["x".to_string()], "x".to_string())
+ (args, vec!["x".to_owned()], "x".to_owned())
};
let variant_def = coq::Variant {
@@ -1127,13 +1127,13 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
// We assume the generated Inductive def is placed in a context where the generic types are in scope.
let inductive = coq::Inductive {
- name: enum_name.to_string(),
+ name: enum_name.to_owned(),
parameters: coq::ParamList::new(vec![]),
variants,
};
let enum_spec = radium::EnumSpec {
- rfn_type: coq::Type::Literal(enum_name.to_string()),
+ rfn_type: coq::Type::Literal(enum_name.to_owned()),
variant_patterns,
};
@@ -1477,60 +1477,60 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
},
TyKind::Float(_) => Err(TranslationError::UnsupportedType {
- description: "RefinedRust does not support floats".to_string(),
+ description: "RefinedRust does not support floats".to_owned(),
}),
TyKind::Array(_, _) => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does not support arrays".to_string(),
+ description: "RefinedRust does not support arrays".to_owned(),
}),
TyKind::Slice(_) => {
// TODO this should really be a fat ptr?
Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does not support slices".to_string(),
+ description: "RefinedRust does not support slices".to_owned(),
})
},
TyKind::Foreign(_) => Err(TranslationError::UnsupportedType {
- description: "RefinedRust does not support extern types".to_string(),
+ description: "RefinedRust does not support extern types".to_owned(),
}),
TyKind::Str => Err(TranslationError::UnsupportedType {
- description: "RefinedRust does not support str".to_string(),
+ description: "RefinedRust does not support str".to_owned(),
}),
TyKind::FnDef(_, _) => Err(TranslationError::Unimplemented {
- description: "RefinedRust does not support FnDef".to_string(),
+ description: "RefinedRust does not support FnDef".to_owned(),
}),
TyKind::FnPtr(_) => Err(TranslationError::Unimplemented {
- description: "RefinedRust does not support FnPtr".to_string(),
+ description: "RefinedRust does not support FnPtr".to_owned(),
}),
TyKind::Dynamic(_, _, _) => Err(TranslationError::UnsupportedType {
- description: "RefinedRust does not support trait objects".to_string(),
+ description: "RefinedRust does not support trait objects".to_owned(),
}),
TyKind::Generator(_, _, _) | TyKind::GeneratorWitness(_) | TyKind::GeneratorWitnessMIR(_, _) => {
Err(TranslationError::UnsupportedType {
- description: "RefinedRust does currently not support generators".to_string(),
+ description: "RefinedRust does currently not support generators".to_owned(),
})
},
TyKind::Alias(_, _) => {
// TODO: probably need this when translating trait definitions
Err(TranslationError::UnsupportedType {
- description: "RefinedRust does not support Alias types".to_string(),
+ description: "RefinedRust does not support Alias types".to_owned(),
})
},
TyKind::Infer(_) => Err(TranslationError::UnsupportedType {
- description: "RefinedRust does not support infer types".to_string(),
+ description: "RefinedRust does not support infer types".to_owned(),
}),
TyKind::Bound(_, _) | TyKind::Placeholder(_) | TyKind::Error(_) => {
Err(TranslationError::UnsupportedType {
- description: "RefinedRust does not support higher-ranked types".to_string(),
+ description: "RefinedRust does not support higher-ranked types".to_owned(),
})
},
}
@@ -1702,12 +1702,12 @@ impl<'def, 'tcx> TypeTranslator<'def, 'tcx> {
self.generate_enum_variant_use(v.def_id, args.iter(), scope).map(Some)
} else {
Err(TranslationError::UnknownError(
- "a non-downcast enum is not a structlike".to_string(),
+ "a non-downcast enum is not a structlike".to_owned(),
))
}
} else {
Err(TranslationError::UnsupportedType {
- description: "non-{enum, struct, tuple} ADTs are not supported".to_string(),
+ description: "non-{enum, struct, tuple} ADTs are not supported".to_owned(),
})
}
},
@@ -1720,7 +1720,7 @@ impl<'def, 'tcx> TypeTranslator<'def, 'tcx> {
let upvars = closure_args.upvar_tys();
self.generate_tuple_use(upvars, &mut TranslationStateInner::InFunction(scope)).map(Some)
},
- _ => Err(TranslationError::UnknownError("not a structlike".to_string())),
+ _ => Err(TranslationError::UnknownError("not a structlike".to_owned())),
}
}
diff --git a/rr_frontend/translation/src/utils.rs b/rr_frontend/translation/src/utils.rs
index 6c1038bfd2e11a82999b2fe6fb6369063cee698a..4b4b0dc9fa54a7480611d4da4f5bc66b03b7a206 100644
--- a/rr_frontend/translation/src/utils.rs
+++ b/rr_frontend/translation/src/utils.rs
@@ -149,7 +149,7 @@ pub fn get_cleaned_def_path(tcx: TyCtxt<'_>, did: DefId) -> Vec<String> {
// this is a generic specialization, skip
continue;
}
- components.push(i.to_string());
+ components.push(i.to_owned());
}
info!("split def path {:?} to {:?}", def_path, components);
@@ -162,7 +162,7 @@ fn extract_def_path(path: &rustc_hir::definitions::DefPath) -> Vec<String> {
let mut components = Vec::new();
for p in &path.data {
if let Some(name) = p.data.get_opt_name() {
- components.push(name.as_str().to_string());
+ components.push(name.as_str().to_owned());
}
}
components
@@ -243,13 +243,13 @@ where
// if the first component is "std", try if we can replace it with "alloc" or "core"
if path[0].as_ref() == "std" {
- let mut components: Vec<_> = path.iter().map(|x| x.as_ref().to_string()).collect();
- components[0] = "core".to_string();
+ let mut components: Vec<_> = path.iter().map(|x| x.as_ref().to_owned()).collect();
+ components[0] = "core".to_owned();
if let Some(did) = try_resolve_did_direct(tcx, &components) {
return Some(did);
}
// try "alloc"
- components[0] = "alloc".to_string();
+ components[0] = "alloc".to_owned();
try_resolve_did_direct(tcx, &components)
} else {
None
@@ -437,13 +437,13 @@ where
// if the first component is "std", try if we can replace it with "alloc" or "core"
if path[0].as_ref() == "std" {
- let mut components: Vec<_> = path.iter().map(|x| x.as_ref().to_string()).collect();
- components[0] = "core".to_string();
+ let mut components: Vec<_> = path.iter().map(|x| x.as_ref().to_owned()).collect();
+ components[0] = "core".to_owned();
if let Some(did) = try_resolve_method_did_direct(tcx, &components) {
return Some(did);
}
// try "alloc"
- components[0] = "alloc".to_string();
+ components[0] = "alloc".to_owned();
try_resolve_method_did_direct(tcx, &components)
} else {
None