Skip to content

Commit

Permalink
mark or_ function as static, naked, noinline and optnone
Browse files Browse the repository at this point in the history
  • Loading branch information
zapashcanon committed Jul 30, 2024
1 parent 7931a3c commit a5a0c94
Showing 1 changed file with 4 additions and 7 deletions.
11 changes: 4 additions & 7 deletions src/libc/src/test-comp.c
Original file line number Diff line number Diff line change
@@ -1,19 +1,16 @@
#include <owi.h>

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;
}

Expand Down

0 comments on commit a5a0c94

Please sign in to comment.