Add an example that modifies an existing C program for symbolic testing

examples/CMakeLists.txt

@@ -23,3 +23,7 @@ target_link_libraries(Lists deepstate)
 
 add_executable(StreamingAndFormatting StreamingAndFormatting.cpp)
 target_link_libraries(StreamingAndFormatting deepstate)
+
+add_executable(Squares Squares.c)
+target_link_libraries(Squares deepstate)
+set_target_properties(Squares PROPERTIES COMPILE_DEFINITIONS "DEEPSTATE_TEST")

examples/Squares.c

@@ -0,0 +1,42 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+int square(int x) {
+    return x*x;
+}
+
+#ifdef DEEPSTATE_TEST
+#include <deepstate/DeepState.h>
+DeepState_EntryPoint(test_main) {
+    const char *new_args[2];
+    new_args[0] = "deepstate";
+    new_args[1] = DeepState_CStr(8);
+
+    DeepState_Assert(0 == old_main(2, new_args));
+}
+
+int main(int argc, const char *argv[]) {
+    return 0 == DeepState_Run();
+}
+// yes this is awful but avoids another ifdef
+#define main old_main
+
+#endif
+
+int main(int argc, const char *argv[]) {
+
+    if(argc != 2) {
+        printf("Usage: %s <integer>\n", argv[0]);
+        return -1;
+    }
+    int x = atoi(argv[1]);
+    int y = square(x);
+
+    if(y + 4 == 29) {
+        printf("You found the secret number\n");
+        return 0;
+    } else {
+        printf("Secret NOT found\n");
+        return -1;
+    }
+}