Fix verifier error

seahorn · Apr 11, 2024 · 6ec8437 · 6ec8437
1 parent 3b7e6c0
commit 6ec8437
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 8 deletions.
diff --git a/src/rust-jobs/mock-test1/lib.rs b/src/rust-jobs/mock-test1/lib.rs
@@ -20,16 +20,16 @@ fn test<T: Test>(mock_test: &T, x: i32, y: bool) -> i32 {
 #[no_mangle]
 pub extern "C" fn entrypt() {
     let mut mock: MockTest = MockTest::new();
-	let mut x: i32 = verifier::any!();
-    let mut y: bool = verifier::any!();
+	let x: i32 = verifier::any!();
+    let y: bool = verifier::any!();
 
     verifier::assume!(x < 10);
 
     mock
         .times_a(2)
         .times_b(2)
         .times_c(1)
-        .returning_a(|x, y| x + 5)
+        .returning_a(|x, _y| x + 5)
         .returning_b(|| 4);
 
     verifier::vassert!(mock.a(x, y) < 15);

diff --git a/src/sea_cex_base.yaml b/src/sea_cex_base.yaml
@@ -45,7 +45,7 @@ verify_options:
   '-S': ''
 # keep intermediate results for debugging 
   keep-temps: ''
-  temp-dir: /tmp/c-rust-sid
+  temp-dir: /tmp/ajendo
 # time and result stats
   horn-stats: true
 # produce counterexample harness

diff --git a/src/seamock-lib/src/lib.rs b/src/seamock-lib/src/lib.rs
@@ -148,14 +148,12 @@ pub fn seamock(_args: TokenStream, input: TokenStream) -> TokenStream {
 
         let times_attr = Ident::new(&format!("times_{}", &method.sig.ident), method.sig.ident.span());
         let max_times_attr = Ident::new(&format!("max_times_{}", &method.sig.ident), method.sig.ident.span());
-        let val_attr = Ident::new(&format!("val_with_{}", &method.sig.ident), method.sig.ident.span());
         let ret_func = Ident::new(&format!("val_returning_{}", &method.sig.ident), method.sig.ident.span());
-        let method_name_string =  &method.sig.ident.to_string();
 
         Some (quote! {
             fn #method_name(#method_inputs) #method_output {
                 self.#times_attr.replace_with(|&mut old| old + 1);
-                // verifier::vassert!(*self.#times_attr.borrow() <= self.#max_times_attr)
+                verifier::vassert!(*self.#times_attr.borrow() <= self.#max_times_attr);
                 (self.#ret_func)(#(#params)*)
             }
         })
@@ -206,7 +204,6 @@ pub fn seamock(_args: TokenStream, input: TokenStream) -> TokenStream {
             #(#with_methods)*
             #(#times_methods)*
             #(#expect_times_methods)*
-            // #(#methods_impl)*
         }
     };