Fixed bug related main function without return

Signed-off-by: Herbert Rocha <[email protected]>
hbgit · Oct 25, 2017 · 1810a3d · 1810a3d
1 parent d1095b9
commit 1810a3d
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
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;
- }
+ } 
 
 }