Simplify file

src/libc/include/owi.h

@@ -1,25 +1,36 @@
 #ifndef _OWI_H
 #define _OWI_H
 
-void *owi_malloc(void *base, unsigned int size) __attribute__((import_module("summaries"))) __attribute__((import_name("malloc")));
-
-void owi_free(void *) __attribute__((import_module("summaries"))) __attribute__((import_name("free")));
-
-char owi_i8(void) __attribute__((import_module("symbolic"))) __attribute__((import_name("i8_symbol")));
-
-int owi_i32(void) __attribute__((import_module("symbolic"))) __attribute__((import_name("i32_symbol")));
-
-long long owi_i64(void) __attribute__((import_module("symbolic"))) __attribute__((import_name("i64_symbol")));
-
-float owi_f32(void) __attribute__((import_module("symbolic"))) __attribute__((import_name("f32_symbol")));
-
-double owi_f64(void) __attribute__((import_module("symbolic"))) __attribute__((import_name("f64_symbol")));
-
-
-void owi_assume(int c) __attribute__((import_module("symbolic"))) __attribute__((import_name("assume")));
-void owi_assert(int c) __attribute__((import_module("symbolic"))) __attribute__((import_name("assert")));
+__attribute__((import_module("summaries"), import_name("alloc"))) void *
+owi_malloc(void *, unsigned int);
+__attribute__((import_module("summaries"), import_name("dealloc"))) void
+owi_free(void *);
+
+__attribute__((import_module("symbolic"), import_name("i8_symbol"))) char
+owi_i8(void);
+__attribute__((import_module("symbolic"), import_name("i32_symbol"))) int
+owi_i32(void);
+__attribute__((import_module("symbolic"), import_name("i64_symbol"))) long long
+owi_i64(void);
+__attribute__((import_module("symbolic"), import_name("f32_symbol"))) float
+owi_f32(void);
+__attribute__((import_module("symbolic"), import_name("f64_symbol"))) double
+owi_f64(void);
+__attribute__((import_module("symbolic"), import_name("bool_symbol"))) _Bool
+owi_bool(void);
+
+__attribute__((import_module("symbolic"), import_name("assume"))) void
+owi_assume(int);
+__attribute__((import_module("symbolic"), import_name("assert"))) void
+owi_assert(int);
+
+__attribute__((import_module("summaries"))) __attribute__((import_name("abort"))) void
+owi_abort(void);
+__attribute__((import_module("summaries"))) __attribute__((import_name("exit"))) void
+owi_exit(int);
 
 int and_(int, int);
+
 int or_(int, int);
 
 #endif

src/libc/src/owi.c

@@ -1,40 +1,5 @@
 #include <owi.h>
 
-__attribute__((import_module("summaries"), import_name("alloc"))) void *
-__owi_alloc(void *, unsigned int);
-__attribute__((import_module("summaries"), import_name("dealloc"))) void
-__owi_dealloc(void *);
-
-__attribute__((import_module("symbolic"), import_name("i8_symbol"))) char __i8(void);
-__attribute__((import_module("symbolic"), import_name("i32_symbol"))) int
-__i32(void);
-__attribute__((import_module("symbolic"), import_name("i64_symbol"))) long long
-__i64(void);
-__attribute__((import_module("symbolic"), import_name("f32_symbol"))) float
-__f32(void);
-__attribute__((import_module("symbolic"), import_name("f64_symbol"))) double
-__f64(void);
-
-__attribute__((import_module("symbolic"), import_name("assume"))) void
-__owi_assume(int);
-__attribute__((import_module("symbolic"), import_name("assert"))) void
-__owi_assert(int);
-
-void *owi_malloc(void *base, unsigned int size) { return __owi_alloc(base, size); }
-void owi_free(void *base) { __owi_dealloc(base); }
-
-char owi_i8(void) { return __i8(); };
-int owi_i32(void) { return __i32(); }
-long long owi_i64(void) { return __i64(); }
-float owi_f32(void) { return __f32(); }
-double owi_f64(void) { return __f64(); }
-
-
-void owi_assume(int c) { __owi_assume(c); }
-void owi_assert(int c) { __owi_assert(c); }
-
-void assume(int) __attribute__((weak, alias("owi_assume")));
-
 int and_(int a, int b) {
   __asm__ __volatile__("local.get 0;"
                        "i32.const 0;"

src/libc/src/stdlib.c

@@ -12,12 +12,12 @@
 #define ldbltype double
 #endif
 
-void owi_abort(void) __attribute__((import_module("summaries"))) __attribute__((import_name("abort")));
-void owi_exit(int)  __attribute__((import_module("summaries"))) __attribute__((import_name("exit")));
-
 void abort(void) { owi_abort(); }
 void exit(int status) { owi_exit(status); }
 
+__attribute__((weak, import_module("symbolic"), import_name("assume"))) void
+assume(int);
+
 extern unsigned char __heap_base;
 unsigned int bump_pointer = &__heap_base;
 

src/libc/src/test-comp.c

@@ -1,6 +1,7 @@
 #include <owi.h>
 
 _Bool __VERIFIER_nondet_bool(void) {
+
   _Bool var = owi_i32();
   owi_assume(or_(var == 0, var == 1));
   return var;