Merge pull request diffblue#192 from diffblue/smowton/feature/split_frontend_final_stage

SEC-58: Split the entry-point-generation phase into two parts

Author: smowton

regression/cbmc/mixed-c-library-goto-main/lib.c

@@ -0,0 +1,4 @@
+
+int getone() {
+  return 1;
+}

regression/cbmc/mixed-c-library-goto-main/main.c

@@ -0,0 +1,12 @@
+
+extern int getone();
+
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  assert(getone()==1);
+}
+
+int altmain() {
+  assert(getone()==0);
+}

regression/cbmc/mixed-c-library-goto-main/main.gb

@@ -0,0 +1,8 @@
+CORE
+main.gb
+lib.c --function altmain
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/mixed-c-library-goto-main/with_function.desc

@@ -0,0 +1,8 @@
+CORE
+main.gb
+lib.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/mixed-c-library-goto-main/without_function.desc

@@ -0,0 +1,4 @@
+
+int getone() {
+  return 1;
+}

regression/cbmc/mixed-goto-library-c-main/lib.c

@@ -0,0 +1,12 @@
+
+extern int getone();
+
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  assert(getone()==1);
+}
+
+int altmain() {
+  assert(getone()==0);
+}

regression/cbmc/mixed-goto-library-c-main/lib.gb

@@ -0,0 +1,8 @@
+CORE
+main.c
+lib.gb --function altmain
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/mixed-goto-library-c-main/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+lib.gb
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring