Fixed bug related main function without return

hbgit · hbgit · commit 1810a3d91424 · 2017-10-25T17:36:46.000-04:00
Signed-off-by: Herbert Rocha &lt;herberthb12@gmail.com&gt;
diff --git a/map2check b/map2check
diff --git a/map2check-wrapper.py b/map2check-wrapper.py
@@ -66,7 +66,7 @@
   exit(1)
 
 if is_memsafety:
-  command_line += " --generate-witness "
+  command_line += " --assume-malloc-true --generate-witness "
 elif is_reachability:
   command_line += " --target-function __VERIFIER_error --generate-witness "
 elif is_overflow:
diff --git a/sample/over.c b/sample/over.c
@@ -1,13 +1,18 @@
+extern void __VERIFIER_error(void);
+extern int __VERIFIER_nondet_int(void);
+
 main()
 {
     int a = __VERIFIER_nondet_int();
+    __VERIFIER_assume(a>0);
     int b = __VERIFIER_nondet_int();
+    __VERIFIER_assume(b>0);
 
     if(a)
     {
         int c = a +b;
     }else{
         int c = b;
-    }
+    }   
 
 }

Original file line number	Diff line number	Diff line change
`@@ -1,13 +1,18 @@`
	`1`	`+extern void __VERIFIER_error(void);`
	`2`	`+extern int __VERIFIER_nondet_int(void);`
	`3`	`+`
`1`	`4`	`main()`
`2`	`5`	`{`
`3`	`6`	`int a = __VERIFIER_nondet_int();`
	`7`	`+ __VERIFIER_assume(a>0);`
`4`	`8`	`int b = __VERIFIER_nondet_int();`
	`9`	`+ __VERIFIER_assume(b>0);`
`5`	`10`
`6`	`11`	`if(a)`
`7`	`12`	`{`
`8`	`13`	`int c = a +b;`
`9`	`14`	`}else{`
`10`	`15`	`int c = b;`
`11`		`- }`
	`16`	`+ }`
`12`	`17`
`13`	`18`	`}`