Skip to content

Commit

Permalink
Hyper Hyper
Browse files Browse the repository at this point in the history
  • Loading branch information
JonasAlaif committed May 13, 2022
1 parent 0ec831a commit 8f07f74
Show file tree
Hide file tree
Showing 12 changed files with 200 additions and 446 deletions.
611 changes: 184 additions & 427 deletions Cargo.lock

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion prusti-common/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ config = "0.13"
itertools = "0.10.3"
serde = { version = "1.0", features = ["derive"] }
lazy_static = "1.4.0"
uuid = { version = "0.8", features = ["v4"] }
uuid = { version = "1.0", features = ["v4"] }
regex = "1.5"
prusti-utils = { path = "../prusti-utils" }
fxhash = "0.2.1"
2 changes: 1 addition & 1 deletion prusti-launch/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ toml = "0.5"
ctrlc = "3.1"

[target.'cfg(unix)'.dependencies]
nix = "0.23"
nix = "0.24"

[dev-dependencies]
glob = "0.3"
7 changes: 3 additions & 4 deletions prusti-server/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -28,10 +28,9 @@ num_cpus = "1.8.0"
serde = { version = "1.0", features = ["derive"] }
# More recent verions of reqwest and warp fail to compile
# due to https://github.com/rust-lang/rust/issues/82151
reqwest = { version = "0.10", features = ["json"] }
warp = "0.2"
# warp 0.2.x only works with tokio 0.2.x
tokio = "0.2"
reqwest = { version = "0.11", features = ["json"] }
warp = "0.3"
tokio = "1.18"

[dev-dependencies]
lazy_static = "1.4.0"
3 changes: 1 addition & 2 deletions prusti-server/src/server.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,7 @@ where
// Here we use a single thread because
// 1. Viper is not thread safe yet (Silicon issue #578), and
// 2. By default Silicon already uses as many cores as possible.
let mut runtime = Builder::new()
.basic_scheduler()
let runtime = Builder::new_current_thread()
.thread_name("prusti-server")
.enable_all()
.build()
Expand Down
2 changes: 1 addition & 1 deletion prusti-specs/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ doctest = false # we have no doc tests
syn = { version = "1.0", features = ["full", "extra-traits", "visit-mut", "parsing", "printing"] }
quote = "1.0"
proc-macro2 = "1.0"
uuid = { version = "0.8", features = ["v4", "serde"] }
uuid = { version = "1.0", features = ["v4", "serde"] }
serde_json = "1.0"
serde = { version = "1.0", features = ["derive"] }
prusti-utils = { path = "../prusti-utils" }
2 changes: 1 addition & 1 deletion prusti-specs/src/common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -407,7 +407,7 @@ pub(crate) fn add_phantom_data_for_generic_params(item_struct: &mut syn::ItemStr

let generate_field_ident = |span: proc_macro2::Span| {
if need_named_fields {
let uuid = Uuid::new_v4().to_simple();
let uuid = Uuid::new_v4().simple();
let field_name = format!("prusti_injected_phantom_field_{}", uuid);
return Some(syn::Ident::new(field_name.as_str(), span));
}
Expand Down
8 changes: 4 additions & 4 deletions prusti-specs/src/specifications/common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ impl Display for SpecificationId {
write!(
f,
"{}",
self.0.to_simple().encode_lower(&mut Uuid::encode_buffer()),
self.0.simple().encode_lower(&mut Uuid::encode_buffer()),
)
}
}
Expand Down Expand Up @@ -97,18 +97,18 @@ impl SpecificationIdGenerator {
}

pub(crate) fn generate_struct_name(item: &syn::ItemImpl) -> String {
let uuid = Uuid::new_v4().to_simple();
let uuid = Uuid::new_v4().simple();
let name_ty = generate_name_for_type(&*item.self_ty).unwrap_or_default();
format!("PrustiStruct{}_{}", name_ty, uuid)
}

pub(crate) fn generate_struct_name_for_trait(item: &syn::ItemTrait) -> String {
let uuid = Uuid::new_v4().to_simple();
let uuid = Uuid::new_v4().simple();
format!("PrustiTrait{}_{}", item.ident, uuid)
}

pub(crate) fn generate_mod_name(ident: &syn::Ident) -> String {
let uuid = Uuid::new_v4().to_simple();
let uuid = Uuid::new_v4().simple();
format!("{}_{}", ident, uuid)
}

Expand Down
2 changes: 1 addition & 1 deletion prusti-specs/src/type_model/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -216,7 +216,7 @@ impl GeneratedIdents {
}
}

let uuid = Uuid::new_v4().to_simple();
let uuid = Uuid::new_v4().simple();

GeneratedIdents {
model_struct_ident: Ident::new(
Expand Down
3 changes: 1 addition & 2 deletions prusti-viper/src/verifier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -397,8 +397,7 @@ fn verify_programs(env: &Environment, programs: Vec<Program>)
// Here we construct a Tokio runtime to block until completion of the futures returned by
// `client.verify`. However, to report verification errors as early as possible,
// `verify_programs` should return an asynchronous stream of verification results.
let mut runtime = Builder::new()
.basic_scheduler()
let runtime = Builder::new_current_thread()
.thread_name("prusti-viper")
.enable_all()
.build()
Expand Down
2 changes: 1 addition & 1 deletion viper/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ log = { version = "0.4", features = ["release_max_level_info"] }
error-chain = "0.12"
viper-sys = { path = "../viper-sys" }
jni = { version = "0.19", features = ["invocation"] }
uuid = { version = "0.8", features = ["v4"] }
uuid = { version = "1.0", features = ["v4"] }
serde = { version = "1.0", features = ["derive"] }
bincode = "1.3.3"
rustc-hash = "1.1.0"
Expand Down
2 changes: 1 addition & 1 deletion vir/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ regex = "1.5"
syn = { version = "1.0", features = ["full", "fold", "parsing", "derive"] }
quote = "1.0"
proc-macro2 = { version = "1.0", features = ["span-locations"] }
uuid = { version = "0.8", features = ["v4"] }
uuid = { version = "1.0", features = ["v4"] }
log = { version = "0.4", features = ["release_max_level_info"] }
lazy_static = "1.4.0"
itertools = "0.10.3"
Expand Down

0 comments on commit 8f07f74

Please sign in to comment.