Merge pull request #2669 from diffblue/spurious-cover-test

use assertion in test regenerate-entry-function

Author: Daniel Kroening

regression/goto-cc-cbmc/regenerate-entry-function/main.c

@@ -1,23 +1,11 @@
+#include <assert.h>
+
 int fun(int x)
 {
-	if(x > 0)
-	{
-		return x * x;
-	}
-	else
-	{
-		return x;
-	}
+  assert(0);
 }
 
 int main(int argc, char** argv)
 {
-	if(argc>4)
-	{
-		return 0;
-	}
-	else
-	{
-		return 1;
-	}
+  return 0;
 }

regression/goto-cc-cbmc/regenerate-entry-function/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
-'--function fun --cover branch'
-^EXIT=0$
+'--function fun'
+^EXIT=10$
 ^SIGNAL=0$
-^x=
+^VERIFICATION FAILED$
 --
 ^warning: ignoring