feat(crab): use macro to avoid crab infer 0 size allocation

seahorn · May 10, 2022 · fee0b78 · fee0b78
1 parent 78ea93e
commit fee0b78
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 4 deletions.
diff --git a/seahorn/lib/proof_allocators.c b/seahorn/lib/proof_allocators.c
@@ -13,16 +13,16 @@
 
 void *realloc(void *ptr, size_t new_size) { return sea_realloc(ptr, new_size); }
 
-void *bounded_malloc(size_t size) {
+void *bounded_malloc_havoc(size_t size) {
   #ifdef __CRAB__
-  assume(size > 1);
+  assume(size > 0);
   #endif
   return size == 0 ? NULL : sea_malloc_havoc_safe(size);
 }
 
-void *can_fail_malloc(size_t size) {
+void *can_fail_malloc_havoc(size_t size) {
   #ifdef __CRAB__
-  assume(size > 1);
+  assume(size > 0);
   #endif
   return size == 0 ? NULL : sea_malloc_havoc(size);
 }

diff --git a/seahorn/lib/sea_allocators.c b/seahorn/lib/sea_allocators.c
@@ -8,6 +8,9 @@ extern void memhavoc(void *, size_t);
 
 extern NONDET_FN_ATTR bool nd_malloc_is_fail(void);
 INLINE void *sea_malloc(size_t sz) {
+  #ifdef __CRAB__
+  assume(sz > 0);
+  #endif
   return nd_malloc_is_fail() ? NULL : malloc(sz);
 }