From a5a0c942e4954f62afcd097b21de4dab800655e5 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Fri, 26 Jul 2024 14:39:22 +0200 Subject: [PATCH 1/2] mark or_ function as static, naked, noinline and optnone --- src/libc/src/test-comp.c | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/libc/src/test-comp.c b/src/libc/src/test-comp.c index 692edc5f1..15a8c76e2 100644 --- a/src/libc/src/test-comp.c +++ b/src/libc/src/test-comp.c @@ -1,19 +1,16 @@ #include -inline __attribute__((always_inline)) int or_(int a, int b) { +static __attribute__((naked,noinline,optnone)) _Bool or_(_Bool a, _Bool b) { __asm__ __volatile__("local.get 0;" - "i32.const 0;" - "i32.ne;" "local.get 1;" - "i32.const 0;" - "i32.ne;" "i32.or;" "return;"); } _Bool __VERIFIER_nondet_bool(void) { - _Bool var = owi_i32(); - owi_assume(or_(var == 0, var == 1)); + const _Bool var = owi_i32(); + const _Bool pc = or_(var == 0, var == 1); + owi_assume(pc); return var; } From d8029b66494e37844dd2bf2cfb9b76579a986054 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Tue, 30 Jul 2024 16:38:55 +0200 Subject: [PATCH 2/2] more warnings when compiling our C stdlib --- src/libc/script.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/libc/script.ml b/src/libc/script.ml index f6b827ab5..01a3789b7 100644 --- a/src/libc/script.ml +++ b/src/libc/script.ml @@ -14,8 +14,8 @@ let () = let out = Format.sprintf "%s.o" filename in let n = Format.ksprintf Sys.command - "clang -g -O3 -ffreestanding --no-standard-libraries --target=wasm32 \ - -c -m32 -Iinclude -Wno-int-conversion -Wno-return-type \ + "clang -O3 -ffreestanding --no-standard-libraries --target=wasm32 -c \ + -m32 -Iinclude -Wall -Werror -Wno-int-conversion -Wno-return-type \ -fbracket-depth=512 -DWANT_STRTOD_WITHOUT_LONG_DOUBLE -o %s %s" out c_filename in