Skip to content

Commit e20fa55

Browse files
sim642sim642
committed
Replace int -> _Bool in goblint stubs arguments
This matters when applied directly to pointers: #1682 (comment).
1 parent 99a4da4 commit e20fa55

File tree

13 files changed

+59
-59
lines changed

13 files changed

+59
-59
lines changed

‎lib/goblint/runtime/include/goblint.h

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
void __goblint_check(int exp);
2-
void __goblint_assume(int exp);
3-
void __goblint_assert(int exp);
1+
void __goblint_check(_Bool exp);
2+
void __goblint_assume(_Bool exp);
3+
void __goblint_assert(_Bool exp);
44

55
void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to avoid pthread.h interfering with Linux kernel headers
66
void __goblint_globalize(void *ptr);
77

8-
void __goblint_split_begin(int exp);
9-
void __goblint_split_end(int exp);
8+
void __goblint_split_begin(_Bool exp);
9+
void __goblint_split_end(_Bool exp);
1010

1111
void __goblint_bounded(unsigned long long exp);

‎lib/goblint/runtime/src/goblint.c

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@
33

44
// Empty implementations (instead of asserts) because annotating documentation promises no-op right now.
55

6-
void __goblint_check(int exp) {
6+
void __goblint_check(_Bool exp) {
77

88
}
99

10-
void __goblint_assume(int exp) {
10+
void __goblint_assume(_Bool exp) {
1111

1212
}
1313

14-
void __goblint_assert(int exp) {
14+
void __goblint_assert(_Bool exp) {
1515

1616
}
1717

@@ -21,11 +21,11 @@ void __goblint_assume_join(pthread_t thread) {
2121
}
2222

2323

24-
void __goblint_split_begin(int exp) {
24+
void __goblint_split_begin(_Bool exp) {
2525

2626
}
2727

28-
void __goblint_split_end(int exp) {
28+
void __goblint_split_end(_Bool exp) {
2929

3030
}
3131

‎lib/libc/stub/include/assert.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
#ifndef GOBLINT_NO_ASSERT
22

3-
void __goblint_assert(int expression);
3+
void __goblint_assert(_Bool expression);
44
#undef assert
55
#define assert(expression) __goblint_assert(expression)
66

‎tests/regression/01-cpa/33-asserts.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
extern void __goblint_check(int); // NOWARN
2-
extern void __goblint_assume(int);
3-
extern void __goblint_assert(int); // NOWARN
1+
extern void __goblint_check(_Bool); // NOWARN
2+
extern void __goblint_assume(_Bool);
3+
extern void __goblint_assert(_Bool); // NOWARN
44
extern void __goblint_unknown(void*);
55

66
#define check(x) __goblint_check(x) // NOWARN

‎tests/regression/55-loop-unrolling/01-simple-cases.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,13 @@
1010
[Info] unrolling loop at 01-simple-cases.c:157:2-165:2 with factor 5
1111
[Info] unrolling loop at 01-simple-cases.c:174:2-178:2 with factor 5
1212
[Info] unrolling loop at 01-simple-cases.c:187:2-194:2 with factor 5
13-
extern void __goblint_check(int exp ) ;
14-
extern void __goblint_assume(int exp ) ;
15-
extern void __goblint_assert(int exp ) ;
13+
extern void __goblint_check(_Bool exp ) ;
14+
extern void __goblint_assume(_Bool exp ) ;
15+
extern void __goblint_assert(_Bool exp ) ;
1616
extern void __goblint_assume_join() ;
1717
extern void __goblint_globalize(void *ptr ) ;
18-
extern void __goblint_split_begin(int exp ) ;
19-
extern void __goblint_split_end(int exp ) ;
18+
extern void __goblint_split_begin(_Bool exp ) ;
19+
extern void __goblint_split_end(_Bool exp ) ;
2020
extern void __goblint_bounded(unsigned long long exp ) ;
2121
int global ;
2222
void example1(void) ;

‎tests/regression/55-loop-unrolling/02-break.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
$ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 02-break.c
22
[Info] unrolling loop at 02-break.c:6:5-15:2 with factor 5
3-
extern void __goblint_check(int exp ) ;
4-
extern void __goblint_assume(int exp ) ;
5-
extern void __goblint_assert(int exp ) ;
3+
extern void __goblint_check(_Bool exp ) ;
4+
extern void __goblint_assume(_Bool exp ) ;
5+
extern void __goblint_assert(_Bool exp ) ;
66
extern void __goblint_assume_join() ;
77
extern void __goblint_globalize(void *ptr ) ;
8-
extern void __goblint_split_begin(int exp ) ;
9-
extern void __goblint_split_end(int exp ) ;
8+
extern void __goblint_split_begin(_Bool exp ) ;
9+
extern void __goblint_split_end(_Bool exp ) ;
1010
extern void __goblint_bounded(unsigned long long exp ) ;
1111
int main(void)
1212
{

‎tests/regression/55-loop-unrolling/03-break-right-place.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
$ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 03-break-right-place.c
22
[Info] unrolling loop at 03-break-right-place.c:8:5-15:5 with factor 5
3-
extern void __goblint_check(int exp ) ;
4-
extern void __goblint_assume(int exp ) ;
5-
extern void __goblint_assert(int exp ) ;
3+
extern void __goblint_check(_Bool exp ) ;
4+
extern void __goblint_assume(_Bool exp ) ;
5+
extern void __goblint_assert(_Bool exp ) ;
66
extern void __goblint_assume_join() ;
77
extern void __goblint_globalize(void *ptr ) ;
8-
extern void __goblint_split_begin(int exp ) ;
9-
extern void __goblint_split_end(int exp ) ;
8+
extern void __goblint_split_begin(_Bool exp ) ;
9+
extern void __goblint_split_end(_Bool exp ) ;
1010
extern void __goblint_bounded(unsigned long long exp ) ;
1111
int main(void)
1212
{

‎tests/regression/55-loop-unrolling/04-simple.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
$ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 04-simple.c
22
[Info] unrolling loop at 04-simple.c:10:5-13:5 with factor 5
3-
extern void __goblint_check(int exp ) ;
4-
extern void __goblint_assume(int exp ) ;
5-
extern void __goblint_assert(int exp ) ;
3+
extern void __goblint_check(_Bool exp ) ;
4+
extern void __goblint_assume(_Bool exp ) ;
5+
extern void __goblint_assert(_Bool exp ) ;
66
extern void __goblint_assume_join() ;
77
extern void __goblint_globalize(void *ptr ) ;
8-
extern void __goblint_split_begin(int exp ) ;
9-
extern void __goblint_split_end(int exp ) ;
8+
extern void __goblint_split_begin(_Bool exp ) ;
9+
extern void __goblint_split_end(_Bool exp ) ;
1010
extern void __goblint_bounded(unsigned long long exp ) ;
1111
void main(void)
1212
{

‎tests/regression/55-loop-unrolling/05-continue.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
$ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 05-continue.c
22
[Info] unrolling loop at 05-continue.c:9:5-17:5 with factor 5
3-
extern void __goblint_check(int exp ) ;
4-
extern void __goblint_assume(int exp ) ;
5-
extern void __goblint_assert(int exp ) ;
3+
extern void __goblint_check(_Bool exp ) ;
4+
extern void __goblint_assume(_Bool exp ) ;
5+
extern void __goblint_assert(_Bool exp ) ;
66
extern void __goblint_assume_join() ;
77
extern void __goblint_globalize(void *ptr ) ;
8-
extern void __goblint_split_begin(int exp ) ;
9-
extern void __goblint_split_end(int exp ) ;
8+
extern void __goblint_split_begin(_Bool exp ) ;
9+
extern void __goblint_split_end(_Bool exp ) ;
1010
extern void __goblint_bounded(unsigned long long exp ) ;
1111
void main(void)
1212
{

‎tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,13 @@
1010
[Info] unrolling loop at 06-simple-cases-unrolled.c:157:2-165:2 with factor 5
1111
[Info] unrolling loop at 06-simple-cases-unrolled.c:174:2-178:2 with factor 5
1212
[Info] unrolling loop at 06-simple-cases-unrolled.c:187:2-194:2 with factor 5
13-
extern void __goblint_check(int exp ) ;
14-
extern void __goblint_assume(int exp ) ;
15-
extern void __goblint_assert(int exp ) ;
13+
extern void __goblint_check(_Bool exp ) ;
14+
extern void __goblint_assume(_Bool exp ) ;
15+
extern void __goblint_assert(_Bool exp ) ;
1616
extern void __goblint_assume_join() ;
1717
extern void __goblint_globalize(void *ptr ) ;
18-
extern void __goblint_split_begin(int exp ) ;
19-
extern void __goblint_split_end(int exp ) ;
18+
extern void __goblint_split_begin(_Bool exp ) ;
19+
extern void __goblint_split_end(_Bool exp ) ;
2020
extern void __goblint_bounded(unsigned long long exp ) ;
2121
int global ;
2222
void example1(void) ;

‎tests/regression/55-loop-unrolling/07-nested-unroll.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@
33
[Info] unrolling loop at 07-nested-unroll.c:6:5-10:5 with factor 5
44
[Info] unrolling loop at 07-nested-unroll.c:13:9-15:9 with factor 5
55
[Info] unrolling loop at 07-nested-unroll.c:12:5-16:5 with factor 5
6-
extern void __goblint_check(int exp ) ;
7-
extern void __goblint_assume(int exp ) ;
8-
extern void __goblint_assert(int exp ) ;
6+
extern void __goblint_check(_Bool exp ) ;
7+
extern void __goblint_assume(_Bool exp ) ;
8+
extern void __goblint_assert(_Bool exp ) ;
99
extern void __goblint_assume_join() ;
1010
extern void __goblint_globalize(void *ptr ) ;
11-
extern void __goblint_split_begin(int exp ) ;
12-
extern void __goblint_split_end(int exp ) ;
11+
extern void __goblint_split_begin(_Bool exp ) ;
12+
extern void __goblint_split_end(_Bool exp ) ;
1313
extern void __goblint_bounded(unsigned long long exp ) ;
1414
int main(void)
1515
{

‎tests/regression/55-loop-unrolling/09-weird.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
$ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 2 --enable justcil --set dbg.justcil-printer clean 09-weird.c
22
[Info] unrolling loop at 09-weird.c:8:5-11:5 with factor 2
3-
extern void __goblint_check(int exp ) ;
4-
extern void __goblint_assume(int exp ) ;
5-
extern void __goblint_assert(int exp ) ;
3+
extern void __goblint_check(_Bool exp ) ;
4+
extern void __goblint_assume(_Bool exp ) ;
5+
extern void __goblint_assert(_Bool exp ) ;
66
extern void __goblint_assume_join() ;
77
extern void __goblint_globalize(void *ptr ) ;
8-
extern void __goblint_split_begin(int exp ) ;
9-
extern void __goblint_split_end(int exp ) ;
8+
extern void __goblint_split_begin(_Bool exp ) ;
9+
extern void __goblint_split_end(_Bool exp ) ;
1010
extern void __goblint_bounded(unsigned long long exp ) ;
1111
void main(void)
1212
{

‎tests/regression/55-loop-unrolling/10-continue-right-place.t

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
$ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 11 --enable justcil --set dbg.justcil-printer clean 10-continue-right-place.c
22
[Info] unrolling loop at 10-continue-right-place.c:7:3-15:3 with factor 11
3-
extern void __goblint_check(int exp ) ;
4-
extern void __goblint_assume(int exp ) ;
5-
extern void __goblint_assert(int exp ) ;
3+
extern void __goblint_check(_Bool exp ) ;
4+
extern void __goblint_assume(_Bool exp ) ;
5+
extern void __goblint_assert(_Bool exp ) ;
66
extern void __goblint_assume_join() ;
77
extern void __goblint_globalize(void *ptr ) ;
8-
extern void __goblint_split_begin(int exp ) ;
9-
extern void __goblint_split_end(int exp ) ;
8+
extern void __goblint_split_begin(_Bool exp ) ;
9+
extern void __goblint_split_end(_Bool exp ) ;
1010
extern void __goblint_bounded(unsigned long long exp ) ;
1111
int main(void)
1212
{

0 commit comments

Comments
 (0)