diff --git a/.stainless-version b/.stainless-version index 70bca09b..6d90a817 100644 --- a/.stainless-version +++ b/.stainless-version @@ -1 +1 @@ -noxt-0.8.1 +noxt-0.8.1-1-g3c34688 diff --git a/demo/examples/generic_result.rs b/demo/examples/generic_result.rs deleted file mode 100644 index b807bf07..00000000 --- a/demo/examples/generic_result.rs +++ /dev/null @@ -1,31 +0,0 @@ -extern crate stainless; -use stainless::*; - -// These are just here, because the bug was triggered more easily with more -// stuff to extract. -trait Clone { - fn clone(&self) -> Self; -} -trait Default { - fn default() -> Self; -} -pub trait Equals { - fn eq(&self, other: &Self) -> bool; -} - -pub enum Result { - Ok(T), - Err(E), -} - -impl Result { - #[post(self.is_ok() == ret)] - pub fn is_ok(&self) -> bool { - match self { - Result::Ok(_) => true, - _ => false, - } - } -} - -pub fn main() {} diff --git a/stainless_backend/src/lib.rs b/stainless_backend/src/lib.rs index d25d7c45..d9253599 100644 --- a/stainless_backend/src/lib.rs +++ b/stainless_backend/src/lib.rs @@ -56,7 +56,9 @@ impl Backend { .arg("--interactive") .arg("--batched") .arg("--vc-cache=false") - .arg("--type-checker=false") + // FIXME: https://github.com/epfl-lara/rust-stainless/issues/86 + .arg("--check-measures=false") + .arg("--infer-measures=false") .arg(format!("--timeout={}", config.timeout)) .arg(format!("--print-ids={}", config.print_ids)) .arg(format!("--print-types={}", config.print_types)) diff --git a/stainless_frontend/tests/pass/generic_result.rs b/stainless_frontend/tests/pass/generic_result.rs index b807bf07..fb83a016 100644 --- a/stainless_frontend/tests/pass/generic_result.rs +++ b/stainless_frontend/tests/pass/generic_result.rs @@ -19,7 +19,7 @@ pub enum Result { } impl Result { - #[post(self.is_ok() == ret)] + #[post(matches!(self, Result::Ok(_)) == ret)] pub fn is_ok(&self) -> bool { match self { Result::Ok(_) => true,