From 6ec84376ee70d50fc0f190056ba67e52b4def6b0 Mon Sep 17 00:00:00 2001
From: Adrian Jendo <ajendo@uwaterloo.ca>
Date: Thu, 11 Apr 2024 11:09:27 -0400
Subject: [PATCH] Fix verifier error

---
 src/rust-jobs/mock-test1/lib.rs | 6 +++---
 src/sea_cex_base.yaml           | 2 +-
 src/seamock-lib/src/lib.rs      | 5 +----
 3 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/rust-jobs/mock-test1/lib.rs b/src/rust-jobs/mock-test1/lib.rs
index 983f2da..0a5d5c5 100644
--- a/src/rust-jobs/mock-test1/lib.rs
+++ b/src/rust-jobs/mock-test1/lib.rs
@@ -20,8 +20,8 @@ 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);
 
@@ -29,7 +29,7 @@ pub extern "C" fn entrypt() {
         .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
index 92fd0e5..e3dc12d 100644
--- 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
index 3f09ed1..112b05c 100644
--- 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)*
         }
     };