Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions source/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions source/rust_verify/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ regex = "1"
internals_interface = { path = "../tools/internals_interface" }
indicatif = "0.17.7"
console = { version = "0.15", default-features = false, features = ["ansi-parsing"] }
once_cell = { version = "1.19.0" }

[target.'cfg(windows)'.dependencies]
win32job = "1"
Expand Down
6 changes: 4 additions & 2 deletions source/rust_verify/src/verus_items.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
use air::ast::Ident;
use once_cell::sync::Lazy;
use regex::Regex;
use rustc_middle::ty::{TyCtxt, TyKind};
use rustc_span::def_id::DefId;
Expand Down Expand Up @@ -631,8 +632,9 @@ pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option<Ru
}

if let Some(rust_path) = rust_path {
let num_re = Regex::new(r"^([A-Za-z0-9_]+)::(MIN|MAX|BITS)").unwrap();
if let Some(captures) = num_re.captures(rust_path) {
static NUM_RE: Lazy<Regex> =
Lazy::new(|| Regex::new(r"^([A-Za-z0-9_]+)::(MIN|MAX|BITS)").unwrap());
if let Some(captures) = NUM_RE.captures(rust_path) {
let ty_name = captures.get(1).expect("invalid int intrinsic regex");
let const_name = captures.get(2).expect("invalid int intrinsic regex");
use RustIntType::*;
Expand Down