Skip to content

Commit c1fa1f5

Browse files
author
Simon Tietz
committed
Merge branch 'master' of github.com:N0W0RK/goblint-analyzer
2 parents f6df1c5 + f3e582b commit c1fa1f5

File tree

3 files changed

+44
-0
lines changed

3 files changed

+44
-0
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// PARAM: --set asm_is_nop false
2+
3+
#include <goblint.h>
4+
5+
int main(void) {
6+
7+
int v = 0;
8+
9+
__asm__("nop": "=x"(v));
10+
11+
__goblint_assert(v==0); //UNKNOWN
12+
}
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// PARAM: --set asm_is_nop false
2+
3+
#include <goblint.h>
4+
5+
int main(void) {
6+
7+
int r;
8+
int v;
9+
10+
__asm__ goto ("nop": : : : test);
11+
12+
v = 0;
13+
14+
test:
15+
16+
__goblint_assert(v == 0); //UNKNOWN
17+
18+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// PARAM: --set asm_is_nop false
2+
#include <setjmp.h>
3+
4+
jmp_buf buf;
5+
6+
int main(void) {
7+
8+
if (!setjmp(buf)) {
9+
10+
__asm__("nop" : "=m"(buf));
11+
12+
longjmp(buf, 1); //WARN
13+
}
14+
}

0 commit comments

Comments
 (0)