Skip to content

Commit aed703b

Browse files
JakuJJakuJ
committed
Make clippy happy
1 parent f50838a commit aed703b

File tree

2 files changed

+41
-45
lines changed

2 files changed

+41
-45
lines changed

‎viper/src/native_backend/fol.rs

+13-16
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,13 @@
11
use std::collections::HashMap;
2-
use vir::{
3-
low::{
4-
ast::{expression::*, statement::*},
5-
*,
6-
},
2+
use vir::low::{
3+
ast::{expression::*, statement::*},
4+
*,
75
};
86

97
pub enum FolStatement {
108
Comment(String),
119
Assume(Expression),
1210
Assert(Expression),
13-
Choice(Box<FolStatement>, Box<FolStatement>),
1411
}
1512

1613
fn vir_statement_to_fol_statements(
@@ -35,22 +32,22 @@ fn vir_statement_to_fol_statements(
3532

3633
vec![FolStatement::Assume(eq)]
3734
}
38-
Statement::MethodCall(methodCall) => {
35+
Statement::MethodCall(method_call) => {
3936
let method_decl = known_methods
40-
.get(&methodCall.method_name)
37+
.get(&method_call.method_name)
4138
.expect("Method not found");
4239

4340
let mut params_to_args = method_decl
4441
.parameters
4542
.iter()
46-
.zip(methodCall.arguments.iter())
43+
.zip(method_call.arguments.iter())
4744
.map(|(target, arg)| (target.clone(), arg.clone()))
4845
.collect::<HashMap<_, _>>();
4946

5047
let returns_to_targets = method_decl
5148
.targets
5249
.iter()
53-
.zip(methodCall.targets.iter())
50+
.zip(method_call.targets.iter())
5451
.map(|(target, arg)| (target.clone(), arg.clone()))
5552
.collect::<HashMap<_, _>>();
5653

@@ -75,12 +72,12 @@ fn vir_statement_to_fol_statements(
7572
position: op.position,
7673
}),
7774
Expression::UnaryOp(op) => Expression::UnaryOp(UnaryOp {
78-
op_kind: op.op_kind,
75+
op_kind: op.op_kind.clone(), // TODO: Copy trait derivation
7976
argument: Box::new(substitute(&op.argument, mapping)),
8077
position: op.position,
8178
}),
8279
Expression::ContainerOp(op) => Expression::ContainerOp(ContainerOp {
83-
kind: op.kind,
80+
kind: op.kind.clone(), // TODO: Copy trait derivation
8481
container_type: op.container_type.clone(),
8582
operands: op
8683
.operands
@@ -102,10 +99,10 @@ fn vir_statement_to_fol_statements(
10299
return_type: func.return_type.clone(),
103100
position: func.position,
104101
}),
105-
Expression::MagicWand(magicWand) => Expression::MagicWand(MagicWand {
106-
left: Box::new(substitute(&magicWand.left, mapping)),
107-
right: Box::new(substitute(&magicWand.right, mapping)),
108-
position: magicWand.position,
102+
Expression::MagicWand(magic_wand) => Expression::MagicWand(MagicWand {
103+
left: Box::new(substitute(&magic_wand.left, mapping)),
104+
right: Box::new(substitute(&magic_wand.right, mapping)),
105+
position: magic_wand.position,
109106
}),
110107
_ => unimplemented!("substitute not implemented for {:?}", expr),
111108
}

‎viper/src/native_backend/smt_lib.rs

+28-29
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,6 @@ impl SMTLib {
9696
self.add_code("(check-sat)".to_string());
9797
self.add_code("(pop)".to_string());
9898
}
99-
FolStatement::Choice(_, _) => unimplemented!("Choice"),
10099
}
101100
}
102101

@@ -351,45 +350,45 @@ impl SMTTranslatable for Expression {
351350
fn to_smt(&self) -> String {
352351
match self {
353352
Expression::Local(local) => local.variable.name.clone(),
354-
Expression::Field(field) => unimplemented!(),
355-
Expression::LabelledOld(labelledOld) => unimplemented!(),
353+
Expression::Field(_) => unimplemented!(),
354+
Expression::LabelledOld(_) => unimplemented!(),
356355
Expression::Constant(constant) => match &constant.value {
357356
ConstantValue::Bool(bool) => bool.to_string(),
358357
ConstantValue::Int(i64) => i64.to_string(),
359358
ConstantValue::BigInt(s) => s.clone(),
360359
},
361-
Expression::MagicWand(magicWand) => format!(
360+
Expression::MagicWand(magic_wand) => format!(
362361
"(=> {} {})", // TODO: is this correct?
363-
magicWand.left.to_smt(),
364-
magicWand.right.to_smt()
362+
magic_wand.left.to_smt(),
363+
magic_wand.right.to_smt()
365364
),
366-
Expression::PredicateAccessPredicate(access) => {
365+
Expression::PredicateAccessPredicate(_access) => {
367366
// TODO: access predicates for predicates
368367
warn!("PredicateAccessPredicate not supported");
369368
"".to_string()
370369
}
371-
Expression::FieldAccessPredicate(fieldAccessPredicate) => unimplemented!(),
372-
Expression::Unfolding(unfolding) => unimplemented!(),
373-
Expression::UnaryOp(unaryOp) => {
370+
Expression::FieldAccessPredicate(_) => unimplemented!(),
371+
Expression::Unfolding(_) => unimplemented!(),
372+
Expression::UnaryOp(unary_op) => {
374373
format!(
375374
"({} {})",
376-
unaryOp.op_kind.to_smt(),
377-
unaryOp.argument.to_smt()
375+
unary_op.op_kind.to_smt(),
376+
unary_op.argument.to_smt()
378377
)
379378
}
380-
Expression::BinaryOp(binaryOp) => format!(
379+
Expression::BinaryOp(binary_op) => format!(
381380
"({} {} {})",
382-
binaryOp.op_kind.to_smt(),
383-
binaryOp.left.to_smt(),
384-
binaryOp.right.to_smt()
381+
binary_op.op_kind.to_smt(),
382+
binary_op.left.to_smt(),
383+
binary_op.right.to_smt()
385384
),
386-
Expression::PermBinaryOp(permBinaryOp) => format!(
385+
Expression::PermBinaryOp(perm_binary_op) => format!(
387386
"({} {} {})",
388-
permBinaryOp.op_kind.to_smt(),
389-
permBinaryOp.left.to_smt(),
390-
permBinaryOp.right.to_smt()
387+
perm_binary_op.op_kind.to_smt(),
388+
perm_binary_op.left.to_smt(),
389+
perm_binary_op.right.to_smt()
391390
),
392-
Expression::ContainerOp(containerOp) => containerOp.to_smt(),
391+
Expression::ContainerOp(container_op) => container_op.to_smt(),
393392
Expression::Conditional(conditional) => format!(
394393
"(ite {} {} {})",
395394
conditional.guard.to_smt(),
@@ -441,12 +440,12 @@ impl SMTTranslatable for Expression {
441440
}
442441
QuantifierKind::Exists => unimplemented!(),
443442
},
444-
Expression::LetExpr(letExpr) => unimplemented!(),
445-
Expression::FuncApp(funcApp) => unimplemented!(),
446-
Expression::DomainFuncApp(domainFuncApp) => {
447-
mk_app(&domainFuncApp.function_name, &domainFuncApp.arguments)
443+
Expression::LetExpr(_) => unimplemented!(),
444+
Expression::FuncApp(_) => unimplemented!(),
445+
Expression::DomainFuncApp(domain_func_app) => {
446+
mk_app(&domain_func_app.function_name, &domain_func_app.arguments)
448447
}
449-
Expression::InhaleExhale(inhaleExhale) => unimplemented!(),
448+
Expression::InhaleExhale(_) => unimplemented!(),
450449
}
451450
}
452451
}
@@ -497,7 +496,7 @@ impl SMTTranslatable for UnaryOpKind {
497496

498497
impl SMTTranslatable for ContainerOp {
499498
fn to_smt(&self) -> String {
500-
match self.kind {
499+
match &self.kind {
501500
ContainerOpKind::SetConstructor => {
502501
if self.operands.len() == 1 {
503502
return format!("(Set_singleton {})", self.operands[0].to_smt());
@@ -577,8 +576,8 @@ impl SMTTranslatable for Type {
577576
},
578577
Type::Seq(seq) => format!("Seq<{}>", seq.element_type.to_smt()),
579578
Type::Set(set) => format!("Set<{}>", set.element_type.to_smt()),
580-
Type::MultiSet(set) => unimplemented!("MultiSet"),
581-
Type::Map(map) => unimplemented!("Map"),
579+
Type::MultiSet(_) => unimplemented!("MultiSet"),
580+
Type::Map(_) => unimplemented!("Map"),
582581
Type::Ref => unimplemented!("Ref"),
583582
Type::Domain(domain) => domain.name.to_string(),
584583
}

0 commit comments

Comments
 (0)