Skip to content

Commit dc98763

Browse files
parnoparno
committed
Cargo fmt
1 parent e60e318 commit dc98763

File tree

4 files changed

+22
-71
lines changed

4 files changed

+22
-71
lines changed

‎verify/rust_verify/src/rust_to_vir.rs

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -142,19 +142,11 @@ fn check_item<'tcx>(
142142
TyKind::Path(QPath::Resolved(_, _path)) => {
143143
for impl_item in impll.items {
144144
// TODO once we have references
145-
unsupported_err!(
146-
item.span,
147-
"unsupported method in impl",
148-
impl_item
149-
);
145+
unsupported_err!(item.span, "unsupported method in impl", impl_item);
150146
}
151147
}
152148
_ => {
153-
unsupported_err!(
154-
item.span,
155-
"unsupported impl of non-path type",
156-
item
157-
);
149+
unsupported_err!(item.span, "unsupported impl of non-path type", item);
158150
}
159151
}
160152
}

‎verify/rust_verify/src/rust_to_vir_base.rs

Lines changed: 6 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -95,17 +95,13 @@ fn get_trigger_arg(span: Span, token_tree: TokenTree) -> Result<u64, VirErr> {
9595
};
9696
match i {
9797
Some(i) => Ok(i),
98-
None => err_span_string(
99-
span,
100-
format!("expected integer constant, found {:?}", &token_tree),
101-
),
98+
None => {
99+
err_span_string(span, format!("expected integer constant, found {:?}", &token_tree))
100+
}
102101
}
103102
}
104103

105-
pub(crate) fn get_trigger(
106-
span: Span,
107-
attrs: &[Attribute],
108-
) -> Result<Vec<Option<u64>>, VirErr> {
104+
pub(crate) fn get_trigger(span: Span, attrs: &[Attribute]) -> Result<Vec<Option<u64>>, VirErr> {
109105
let mut groups: Vec<Option<u64>> = Vec::new();
110106
for attr in attrs {
111107
match &attr.kind {
@@ -313,9 +309,7 @@ pub(crate) fn is_smt_arith<'tcx>(bctx: &BodyCtxt<'tcx>, id1: &HirId, id2: &HirId
313309
}
314310
}
315311

316-
pub(crate) fn check_generics<'tcx>(
317-
generics: &'tcx Generics<'tcx>,
318-
) -> Result<Idents, VirErr> {
312+
pub(crate) fn check_generics<'tcx>(generics: &'tcx Generics<'tcx>) -> Result<Idents, VirErr> {
319313
let Generics { params, where_clause, span: _ } = generics;
320314
let mut typ_params: Vec<vir::ast::Ident> = Vec::new();
321315
for param in params.iter() {
@@ -329,10 +323,6 @@ pub(crate) fn check_generics<'tcx>(
329323
_ => unsupported_err!(generics.span, "complex generics"),
330324
}
331325
}
332-
unsupported_err_unless!(
333-
where_clause.predicates.len() == 0,
334-
generics.span,
335-
"where clause"
336-
);
326+
unsupported_err_unless!(where_clause.predicates.len() == 0, generics.span, "where clause");
337327
Ok(Rc::new(typ_params))
338328
}

‎verify/rust_verify/src/rust_to_vir_expr.rs

Lines changed: 13 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -130,10 +130,7 @@ fn extract_quant<'tcx>(
130130
.collect();
131131
let expr = &body.value;
132132
if !matches!(bctx.types.node_type(expr.hir_id).kind(), TyKind::Bool) {
133-
return err_span_str(
134-
expr.span,
135-
"forall/ensures needs a bool expression",
136-
);
133+
return err_span_str(expr.span, "forall/ensures needs a bool expression");
137134
}
138135
let vir_expr = expr_to_vir(bctx, expr)?;
139136
Ok(spanned_new(span, ExprX::Quant(quant, Rc::new(binders), vir_expr)))
@@ -159,8 +156,7 @@ pub(crate) fn expr_to_vir<'tcx>(
159156
) -> Result<vir::ast::Expr, VirErr> {
160157
let mut vir_expr = expr_to_vir_inner(bctx, expr)?;
161158
for group in get_trigger(expr.span, bctx.ctxt.tcx.hir().attrs(expr.hir_id))? {
162-
vir_expr =
163-
spanned_new(expr.span, ExprX::Unary(UnaryOp::Trigger(group), vir_expr));
159+
vir_expr = spanned_new(expr.span, ExprX::Unary(UnaryOp::Trigger(group), vir_expr));
164160
}
165161
Ok(vir_expr)
166162
}
@@ -310,11 +306,7 @@ fn fn_call_to_vir<'tcx>(
310306
let fun_ty = bctx.types.node_type(fun.hir_id);
311307
let (param_typs, ret_typ) = match fun_ty.kind() {
312308
TyKind::FnDef(def_id, _substs) => match tcx.fn_sig(*def_id).no_bound_vars() {
313-
None => unsupported_err!(
314-
expr.span,
315-
format!("found bound vars in function"),
316-
expr
317-
),
309+
None => unsupported_err!(expr.span, format!("found bound vars in function"), expr),
318310
Some(f) => {
319311
let params: Vec<Typ> =
320312
f.inputs().iter().map(|t| mid_ty_to_vir(tcx, *t)).collect();
@@ -348,11 +340,7 @@ fn fn_call_to_vir<'tcx>(
348340
GenericArgKind::Type(ty) => {
349341
typ_args.push(mid_ty_to_vir(tcx, ty));
350342
}
351-
_ => unsupported_err!(
352-
expr.span,
353-
format!("lifetime/const type arguments"),
354-
expr
355-
),
343+
_ => unsupported_err!(expr.span, format!("lifetime/const type arguments"), expr),
356344
}
357345
}
358346
// make call
@@ -479,10 +467,9 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
479467
IntRange::Int | IntRange::Nat | IntRange::U(_) | IntRange::USize => {
480468
Ok(spanned_new(expr.span, ExprX::Const(c)))
481469
}
482-
IntRange::I(_) | IntRange::ISize => Ok(mk_clip(
483-
&range,
484-
&spanned_new(expr.span, ExprX::Const(c)),
485-
)),
470+
IntRange::I(_) | IntRange::ISize => {
471+
Ok(mk_clip(&range, &spanned_new(expr.span, ExprX::Const(c))))
472+
}
486473
}
487474
} else {
488475
panic!("unexpected constant: {:?} {:?}", lit, typ)
@@ -567,10 +554,7 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
567554
expr_tuple_datatype_ctor_to_vir(bctx, expr, &path.res, &[])
568555
}
569556
_ => {
570-
unsupported_err!(
571-
expr.span,
572-
format!("Path {:?} kind {:?}", id, def_kind)
573-
)
557+
unsupported_err!(expr.span, format!("Path {:?} kind {:?}", id, def_kind))
574558
}
575559
}
576560
}
@@ -609,10 +593,8 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
609593
} else {
610594
unsupported_err!(expr.span, "field_of_non_adt", expr)
611595
};
612-
let mut vir = spanned_new(
613-
expr.span,
614-
ExprX::Field { lhs: vir_lhs, datatype_name, field_name },
615-
);
596+
let mut vir =
597+
spanned_new(expr.span, ExprX::Field { lhs: vir_lhs, datatype_name, field_name });
616598
if let Some(target_typ) = unbox {
617599
vir = Spanned::new(
618600
vir.span.clone(),
@@ -754,21 +736,14 @@ pub(crate) fn let_stmt_to_vir<'tcx>(
754736
attrs: &[Attribute],
755737
) -> Result<Vec<vir::ast::Stmt>, VirErr> {
756738
let Pat { hir_id, kind, span: _, default_binding_modes } = pattern;
757-
unsupported_err_unless!(
758-
default_binding_modes,
759-
pattern.span,
760-
"default_binding_modes"
761-
);
739+
unsupported_err_unless!(default_binding_modes, pattern.span, "default_binding_modes");
762740
match pattern.kind {
763741
PatKind::Binding(annotation, _id, ident, pat) => {
764742
let mutable = match annotation {
765743
BindingAnnotation::Unannotated => false,
766744
BindingAnnotation::Mutable => true,
767745
_ => {
768-
unsupported_err!(
769-
pattern.span,
770-
format!("binding annotation {:?}", annotation)
771-
)
746+
unsupported_err!(pattern.span, format!("binding annotation {:?}", annotation))
772747
}
773748
};
774749
match pat {
@@ -784,10 +759,7 @@ pub(crate) fn let_stmt_to_vir<'tcx>(
784759
Ok(vec![spanned_new(
785760
pattern.span,
786761
StmtX::Decl {
787-
param: spanned_new(
788-
pattern.span,
789-
ParamX { name: name.clone(), typ, mode },
790-
),
762+
param: spanned_new(pattern.span, ParamX { name: name.clone(), typ, mode }),
791763
mutable,
792764
init: initializer.map(|e| expr_to_vir(bctx, e)).transpose()?,
793765
},

‎verify/rust_verify/src/util.rs

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,10 +17,7 @@ pub(crate) fn err_span_string<A>(span: Span, msg: String) -> Result<A, VirErr> {
1717
Err(spanned_new(span, VirErrX::Str(msg)))
1818
}
1919

20-
pub(crate) fn unsupported_err_span<A>(
21-
span: Span,
22-
msg: String,
23-
) -> Result<A, VirErr> {
20+
pub(crate) fn unsupported_err_span<A>(span: Span, msg: String) -> Result<A, VirErr> {
2421
err_span_string(
2522
span,
2623
format!("The verifier does not yet support the following Rust feature: {}", msg),

0 commit comments

Comments
 (0)