Merge pull request #163 from bjjwwang/master

Recur-mode -> Recur-handle

Author: yuleisui

CMakeLists.txt

@@ -327,8 +327,8 @@ foreach(filename ${ae_overflow_files})
           WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
   )
   add_test(
-          NAME ae_recursion_tests/${filename}-widen-top
-          COMMAND ae -overflow -recur-mode=widen-top -field-limit=1024 ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+          NAME ae_recursion_tests/${filename}-widen-narrow
+          COMMAND ae -overflow -handle-recur=widen-narrow -field-limit=1024 ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
           WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
   )
 endforeach()
@@ -350,7 +350,7 @@ file(GLOB ae_recursion_files RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} "${CMAKE_CURRE
 foreach(filename ${ae_recursion_files})
   add_test(
           NAME ae_recursion_tests/${filename}-widen-narrow
-          COMMAND ae -overflow -recur-mode=widen-narrow -field-limit=1024 -widen-delay=10 ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+          COMMAND ae -overflow -handle-recur=widen-narrow -field-limit=1024 -widen-delay=10 ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
           WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin
   )
 endforeach()

src/ae_recursion_tests/demo.c

@@ -0,0 +1,19 @@
+#include "stdbool.h"
+extern void svf_assert(bool);
+extern void svf_print(int, char*);
+
+int demo(int a) {
+    if (a >= 10000)
+        return a;
+    demo(a+1);
+}
+
+int main() {
+    int result = demo(0);
+    svf_print(result, "result");
+    svf_assert(result == 10000);
+}
+
+// TOP: [-oo, +oo]
+// WIDEN_ONLY: [10000, +oo]
+// WIDEN_NARROW: [10000, 10000]