feat: add suc mock function

seahorn · Oct 3, 2023 · dd9b13c · dd9b13c
1 parent c665a62
commit dd9b13c
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/src/include/seamock.hh b/src/include/seamock.hh
@@ -148,6 +148,19 @@ BOOST_HANA_CONSTEXPR_LAMBDA auto AND =
 #define LAZY_MOCK_FUNCTION(name, ret_type, args_tuple)                         \
   MOCK_FUNCTION(name, DefaultExpectationsMap, ret_type, args_tuple)
 
+// assumes return type is int
+// function can return [MIN_INT, 0]
+#define SUC_MOCK_FUNCTION(name, args_tuple)                                    \
+  extern int CREATE_ND_FUNC_NAME(name, _ret)(void);                            \
+  BOOST_HANA_CONSTEXPR_LAMBDA auto name##_ret_fn = []() {                      \
+    int ret = CREATE_ND_FUNC_NAME(name, _ret)();                               \
+    assume(ret == 0);                                                          \
+    return ret;                                                                \
+  };                                                                           \
+  constexpr auto name##_suc_map =                                              \
+      ReturnFn(name##_ret_fn, DefaultExpectationsMap);                         \
+  MOCK_FUNCTION(name, name##_suc_map, int, args_tuple)
+
 // assumes return type is int
 // function can return [MIN_INT, 0]
 #define ERR_SUC_MOCK_FUNCTION(name, args_tuple)                                \