Add error message

seahorn · Apr 12, 2024 · c40c7a0 · c40c7a0
1 parent 0801d67
commit c40c7a0
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/src/rust-jobs/mock-test1/lib.rs b/src/rust-jobs/mock-test1/lib.rs
@@ -1,6 +1,7 @@
 #![cfg_attr(not(kani), no_std)]
 
 use verifier;
+use sea;
 use seamock::seamock;
 
 #[seamock]

diff --git a/src/seamock-lib/src/lib.rs b/src/seamock-lib/src/lib.rs
@@ -149,11 +149,15 @@ 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 ret_func = Ident::new(&format!("val_returning_{}", &method.sig.ident), method.sig.ident.span());
+        let error = format!("Hit times limit for {}", &method.sig.ident);
 
         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);
+                if (*self.#times_attr.borrow() > self.#max_times_attr) {
+                    sea::sea_printf!(#error, self.#max_times_attr);
+                    verifier::vassert!(false);
+                }
                 (self.#ret_func)(#(#params)*)
             }
         })