Skip to content

Commit

Permalink
vargo fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
mmcloughlin committed Jun 29, 2024
1 parent edabef8 commit 90a396d
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 25 deletions.
11 changes: 6 additions & 5 deletions source/rust_verify_test/tests/common/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -541,9 +541,10 @@ pub fn assert_rust_error_msg_all(err: TestErr, expected_msg: &str) {

#[allow(dead_code)]
pub fn assert_spans_contain(err: &Diagnostic, needle: &str) {
assert!(err
.spans
.iter()
.find(|s| s.label.is_some() && s.label.as_ref().unwrap().contains(needle))
.is_some());
assert!(
err.spans
.iter()
.find(|s| s.label.is_some() && s.label.as_ref().unwrap().contains(needle))
.is_some()
);
}
24 changes: 4 additions & 20 deletions source/vir/src/sst_to_air.rs
Original file line number Diff line number Diff line change
Expand Up @@ -184,11 +184,7 @@ fn decoration_str(d: TypDecoration) -> &'static str {
pub fn monotyp_to_id(typ: &MonoTyp) -> Vec<Expr> {
let mk_id = |t: Expr| -> Vec<Expr> {
let ds = str_var(crate::def::DECORATE_NIL);
if crate::context::DECORATE {
vec![ds, t]
} else {
vec![t]
}
if crate::context::DECORATE { vec![ds, t] } else { vec![t] }
};
match &**typ {
MonoTypX::Bool => mk_id(str_var(crate::def::TYPE_ID_BOOL)),
Expand Down Expand Up @@ -221,11 +217,7 @@ pub fn monotyp_to_id(typ: &MonoTyp) -> Vec<Expr> {

fn big_int_to_expr(i: &BigInt) -> Expr {
use num_traits::Zero;
if i >= &BigInt::zero() {
mk_nat(i)
} else {
air::ast_util::mk_neg(&mk_nat(-i))
}
if i >= &BigInt::zero() { mk_nat(i) } else { air::ast_util::mk_neg(&mk_nat(-i)) }
}

// SMT-level type identifiers.
Expand All @@ -249,11 +241,7 @@ fn big_int_to_expr(i: &BigInt) -> Expr {
pub fn typ_to_ids(typ: &Typ) -> Vec<Expr> {
let mk_id = |t: Expr| -> Vec<Expr> {
let ds = str_var(crate::def::DECORATE_NIL);
if crate::context::DECORATE {
vec![ds, t]
} else {
vec![t]
}
if crate::context::DECORATE { vec![ds, t] } else { vec![t] }
};
match &**typ {
TypX::Bool => mk_id(str_var(crate::def::TYPE_ID_BOOL)),
Expand Down Expand Up @@ -1259,11 +1247,7 @@ pub(crate) fn assume_var(span: &Span, x: &UniqueIdent, exp: &Exp) -> Stm {
}

fn one_stmt(stmts: Vec<Stmt>) -> Stmt {
if stmts.len() == 1 {
stmts[0].clone()
} else {
Arc::new(StmtX::Block(Arc::new(stmts)))
}
if stmts.len() == 1 { stmts[0].clone() } else { Arc::new(StmtX::Block(Arc::new(stmts))) }
}

#[derive(Debug)]
Expand Down

0 comments on commit 90a396d

Please sign in to comment.