diff --git a/tests/incremental/11-restart/11-paper-example.c b/tests/incremental/11-restart/11-paper-example.c index e16d273f5f..d7a569b558 100644 --- a/tests/incremental/11-restart/11-paper-example.c +++ b/tests/incremental/11-restart/11-paper-example.c @@ -3,7 +3,7 @@ pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; -int (*fp)() = NULL; +int (*fp)(void) = NULL; int bad() { return -1; diff --git a/tests/regression/00-sanity/15-unused_arg.c b/tests/regression/00-sanity/15-unused_arg.c index a7dc6970e6..6587a0b9e4 100644 --- a/tests/regression/00-sanity/15-unused_arg.c +++ b/tests/regression/00-sanity/15-unused_arg.c @@ -4,9 +4,9 @@ void f() { glob++; // NOWARN! } -void (*fptr) = f; +void (*fptr)(void) = f; -int g(void (*ptr)()) { +int g(void (*ptr)(void)) { return 0; } diff --git a/tests/regression/00-sanity/38-evalfunvar-dead.c b/tests/regression/00-sanity/38-evalfunvar-dead.c index 26c779c7e6..2483e6ed4e 100644 --- a/tests/regression/00-sanity/38-evalfunvar-dead.c +++ b/tests/regression/00-sanity/38-evalfunvar-dead.c @@ -1,7 +1,7 @@ #include int main() { - int (*fp)() = &rand; + int (*fp)(void) = &rand; abort(); fp(); // NOWARN (No suitable function to call) return 0; diff --git a/tests/regression/01-cpa/06-pointers.c b/tests/regression/01-cpa/06-pointers.c index c70080c01e..b151a00117 100644 --- a/tests/regression/01-cpa/06-pointers.c +++ b/tests/regression/01-cpa/06-pointers.c @@ -8,7 +8,7 @@ int fun_5b() { return 5; } int main () { int i,j,k1,k2,k3; int *p, **pp; - int (*fp)(); //pointer to function + int (*fp)(void); //pointer to function // reading through pointer i = 5; diff --git a/tests/regression/01-cpa/09-arrays.c b/tests/regression/01-cpa/09-arrays.c index 07025a2a4c..c38ffb8933 100644 --- a/tests/regression/01-cpa/09-arrays.c +++ b/tests/regression/01-cpa/09-arrays.c @@ -18,9 +18,9 @@ int main () { int a[] = {2,2,2}; int b[2], c[3]; - int (*f[2])() = {fun_5, fun_6}; - int (*g[2])() = {fun_5, fun_5b}; - int (*fp)(); + int (*f[2])(void) = {fun_5, fun_6}; + int (*g[2])(void) = {fun_5, fun_5b}; + int (*fp)(void); int *ip; int (*iap)[]; diff --git a/tests/regression/01-cpa/46-funptr_path.c b/tests/regression/01-cpa/46-funptr_path.c index 8e2523ad37..e06784ef9d 100644 --- a/tests/regression/01-cpa/46-funptr_path.c +++ b/tests/regression/01-cpa/46-funptr_path.c @@ -16,7 +16,7 @@ void fun2() { int main() { int x = __VERIFIER_nondet_int(); - void (*fp)(); + void (*fp)(void); if (x) { pthread_mutex_lock(&mutex); diff --git a/tests/regression/02-base/46-spawn-global-funptrs.c b/tests/regression/02-base/46-spawn-global-funptrs.c index 24474a6cf3..e67a6e4145 100644 --- a/tests/regression/02-base/46-spawn-global-funptrs.c +++ b/tests/regression/02-base/46-spawn-global-funptrs.c @@ -9,13 +9,13 @@ void bar() { __goblint_check(1); // assert reachable } -void (*funs[2])() = { +void (*funs[2])(void) = { &foo, &bar }; extern void magic1(); -extern void magic2(void (*funs[])()); +extern void magic2(void (*funs[])(void)); int main() { magic1(); // invalidate funs a bit diff --git a/tests/regression/03-practical/06-callback.c b/tests/regression/03-practical/06-callback.c index 6cc6ab132f..0c35b155ef 100644 --- a/tests/regression/03-practical/06-callback.c +++ b/tests/regression/03-practical/06-callback.c @@ -9,7 +9,7 @@ void callme(void) { x = 5; } -void callfun(void (*fun)()) { +void callfun(void (*fun)(void)) { fun(); return; } diff --git a/tests/regression/04-mutex/19-call_by_ptr_rc.c b/tests/regression/04-mutex/19-call_by_ptr_rc.c index b4895bb7cf..2d4166c390 100644 --- a/tests/regression/04-mutex/19-call_by_ptr_rc.c +++ b/tests/regression/04-mutex/19-call_by_ptr_rc.c @@ -2,7 +2,7 @@ extern int __VERIFIER_nondet_int(); #include -void foo(int (*callback)()) { +void foo(int (*callback)(void)) { for (int i = 0; i < 10; i++) { if (__VERIFIER_nondet_int()) callback(); diff --git a/tests/regression/04-mutex/21-sound_base.c b/tests/regression/04-mutex/21-sound_base.c index 18086eb570..612eaff8de 100644 --- a/tests/regression/04-mutex/21-sound_base.c +++ b/tests/regression/04-mutex/21-sound_base.c @@ -6,7 +6,7 @@ int global; void bad() { global++; } // RACE! void good() { printf("Hello!"); } -void (*f)() = good; +void (*f)(void) = good; void *t_fun(void *arg) { f(); // RACE! diff --git a/tests/regression/04-mutex/27-base_rc.c b/tests/regression/04-mutex/27-base_rc.c index 68874fcc07..3e05f512c6 100644 --- a/tests/regression/04-mutex/27-base_rc.c +++ b/tests/regression/04-mutex/27-base_rc.c @@ -13,11 +13,11 @@ void good() { pthread_mutex_unlock(&gm); } -void (*f)() = good; +void (*f)(void) = good; pthread_mutex_t fm = PTHREAD_MUTEX_INITIALIZER; void *t_fun(void *arg) { - void (*g)(); + void (*g)(void); pthread_mutex_lock(&fm); g = f; // NORACE diff --git a/tests/regression/04-mutex/28-base_nr.c b/tests/regression/04-mutex/28-base_nr.c index 58962d74b9..9a0325bc9a 100644 --- a/tests/regression/04-mutex/28-base_nr.c +++ b/tests/regression/04-mutex/28-base_nr.c @@ -13,11 +13,11 @@ void good() { pthread_mutex_unlock(&gm); } -void (*f)() = good; +void (*f)(void) = good; pthread_mutex_t fm = PTHREAD_MUTEX_INITIALIZER; void *t_fun(void *arg) { - void (*g)(); + void (*g)(void); pthread_mutex_lock(&fm); g = f; // NORACE diff --git a/tests/regression/04-mutex/29-funstruct_rc.c b/tests/regression/04-mutex/29-funstruct_rc.c index 9b1dd0a671..a3087e7718 100644 --- a/tests/regression/04-mutex/29-funstruct_rc.c +++ b/tests/regression/04-mutex/29-funstruct_rc.c @@ -7,7 +7,7 @@ pthread_mutex_t B_mutex = PTHREAD_MUTEX_INITIALIZER; struct ops { int (*f)(int); - void (*g)(); + void (*g)(void); }; extern void register_dev(struct ops *); diff --git a/tests/regression/04-mutex/30-funstruct_nr.c b/tests/regression/04-mutex/30-funstruct_nr.c index 99bc27947d..7fb075bb4e 100644 --- a/tests/regression/04-mutex/30-funstruct_nr.c +++ b/tests/regression/04-mutex/30-funstruct_nr.c @@ -7,7 +7,7 @@ pthread_mutex_t B_mutex = PTHREAD_MUTEX_INITIALIZER; struct ops { int (*f)(int); - void (*g)(); + void (*g)(void); }; extern void register_dev(struct ops *); diff --git a/tests/regression/04-mutex/50-funptr_rc.c b/tests/regression/04-mutex/50-funptr_rc.c index 1bb2840c5e..f5fa217177 100644 --- a/tests/regression/04-mutex/50-funptr_rc.c +++ b/tests/regression/04-mutex/50-funptr_rc.c @@ -5,7 +5,7 @@ int f1() { return 4; } int f2() { return 5; } -int (*fp)() = f1; +int (*fp)(void) = f1; pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; diff --git a/tests/regression/04-mutex/56-extern_call_by_ptr_rc.c b/tests/regression/04-mutex/56-extern_call_by_ptr_rc.c index 77ba0243e6..75a0ab8da3 100644 --- a/tests/regression/04-mutex/56-extern_call_by_ptr_rc.c +++ b/tests/regression/04-mutex/56-extern_call_by_ptr_rc.c @@ -1,6 +1,6 @@ #include -extern void foo(int (*callback)()); +extern void foo(int (*callback)(void)); int glob; diff --git a/tests/regression/13-privatized/95-mm-calloc.c b/tests/regression/13-privatized/95-mm-calloc.c index 60a88379fc..6ca7dbbafa 100644 --- a/tests/regression/13-privatized/95-mm-calloc.c +++ b/tests/regression/13-privatized/95-mm-calloc.c @@ -3,7 +3,7 @@ #include #include struct a { - void (*b)(); + void (*b)(void); }; int g = 0; diff --git a/tests/regression/22-partitioned_arrays/05-adapted_from_01_09_array.c b/tests/regression/22-partitioned_arrays/05-adapted_from_01_09_array.c index 5d3dad5967..ac8717a3ea 100644 --- a/tests/regression/22-partitioned_arrays/05-adapted_from_01_09_array.c +++ b/tests/regression/22-partitioned_arrays/05-adapted_from_01_09_array.c @@ -19,9 +19,9 @@ int main () { int a[] = {2,2,2}; int b[2], c[3]; - int (*f[2])() = {fun_5, fun_6}; - int (*g[2])() = {fun_5, fun_5b}; - int (*fp)(); + int (*f[2])(void) = {fun_5, fun_6}; + int (*g[2])(void) = {fun_5, fun_5b}; + int (*fp)(void); int *ip; int (*iap)[]; diff --git a/tests/regression/23-partitioned_arrays_last/05-adapted_from_01_09_array.c b/tests/regression/23-partitioned_arrays_last/05-adapted_from_01_09_array.c index 4f5bab8103..49719e1ac9 100644 --- a/tests/regression/23-partitioned_arrays_last/05-adapted_from_01_09_array.c +++ b/tests/regression/23-partitioned_arrays_last/05-adapted_from_01_09_array.c @@ -19,9 +19,9 @@ int main () { int a[] = {2,2,2}; int b[2], c[3]; - int (*f[2])() = {fun_5, fun_6}; - int (*g[2])() = {fun_5, fun_5b}; - int (*fp)(); + int (*f[2])(void) = {fun_5, fun_6}; + int (*g[2])(void) = {fun_5, fun_5b}; + int (*fp)(void); int *ip; int (*iap)[]; diff --git a/tests/regression/28-race_reach/19-callback_racing.c b/tests/regression/28-race_reach/19-callback_racing.c index 04eaaeef4f..456660655e 100644 --- a/tests/regression/28-race_reach/19-callback_racing.c +++ b/tests/regression/28-race_reach/19-callback_racing.c @@ -4,7 +4,7 @@ extern int __VERIFIER_nondet_int(); #include #include "racemacros.h" -void foo(int (*callback)()) { +void foo(int (*callback)(void)) { for (int i = 0; i < 10; i++) { if (__VERIFIER_nondet_int()) callback(); diff --git a/tests/regression/28-race_reach/20-callback_racefree.c b/tests/regression/28-race_reach/20-callback_racefree.c index e41896f31a..dd78bc51b4 100644 --- a/tests/regression/28-race_reach/20-callback_racefree.c +++ b/tests/regression/28-race_reach/20-callback_racefree.c @@ -4,7 +4,7 @@ extern int __VERIFIER_nondet_int(); #include #include "racemacros.h" -void foo(int (*callback)()) { +void foo(int (*callback)(void)) { for (int i = 0; i < 10; i++) { if (__VERIFIER_nondet_int()) callback(); diff --git a/tests/regression/28-race_reach/27-funptr_racing.c b/tests/regression/28-race_reach/27-funptr_racing.c index 7210d0d56c..a93bc30b94 100644 --- a/tests/regression/28-race_reach/27-funptr_racing.c +++ b/tests/regression/28-race_reach/27-funptr_racing.c @@ -16,11 +16,11 @@ void good() { pthread_mutex_unlock(&gm); } -void (*f)() = good; +void (*f)(void) = good; pthread_mutex_t fm = PTHREAD_MUTEX_INITIALIZER; void *t_fun(void *arg) { - void (*g)(); + void (*g)(void); pthread_mutex_lock(&fm); g = f; diff --git a/tests/regression/28-race_reach/28-funptr_racefree.c b/tests/regression/28-race_reach/28-funptr_racefree.c index f36168aaaa..a72266d4c7 100644 --- a/tests/regression/28-race_reach/28-funptr_racefree.c +++ b/tests/regression/28-race_reach/28-funptr_racefree.c @@ -15,11 +15,11 @@ void good() { pthread_mutex_unlock(&gm); } -void (*f)() = good; +void (*f)(void) = good; pthread_mutex_t fm = PTHREAD_MUTEX_INITIALIZER; void *t_fun(void *arg) { - void (*g)(); + void (*g)(void); pthread_mutex_lock(&fm); g = f; diff --git a/tests/regression/28-race_reach/95-deref-fun.c b/tests/regression/28-race_reach/95-deref-fun.c index f1431d9221..d76d362134 100644 --- a/tests/regression/28-race_reach/95-deref-fun.c +++ b/tests/regression/28-race_reach/95-deref-fun.c @@ -1,7 +1,7 @@ // PARAM: --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" #include // NOCRASH -void foo(int (*callback)()) { +void foo(int (*callback)(void)) { } int bar() { diff --git a/tests/regression/67-interval-sets-two/18-adapted_from_01_09_array.c b/tests/regression/67-interval-sets-two/18-adapted_from_01_09_array.c index 9e95421320..16cb9f8f20 100644 --- a/tests/regression/67-interval-sets-two/18-adapted_from_01_09_array.c +++ b/tests/regression/67-interval-sets-two/18-adapted_from_01_09_array.c @@ -19,9 +19,9 @@ int main () { int a[] = {2,2,2}; int b[2], c[3]; - int (*f[2])() = {fun_5, fun_6}; - int (*g[2])() = {fun_5, fun_5b}; - int (*fp)(); + int (*f[2])(void) = {fun_5, fun_6}; + int (*g[2])(void) = {fun_5, fun_5b}; + int (*fp)(void); int *ip; int (*iap)[]; diff --git a/tests/sv-comp/cfg/free_spawn_ub_true-unreach-call.c b/tests/sv-comp/cfg/free_spawn_ub_true-unreach-call.c index c5f565b13e..9f54cd950d 100644 --- a/tests/sv-comp/cfg/free_spawn_ub_true-unreach-call.c +++ b/tests/sv-comp/cfg/free_spawn_ub_true-unreach-call.c @@ -8,7 +8,7 @@ void foo() int main() { - void (*p)() = &foo; + void (*p)(void) = &foo; free(p); // TODO: free shouldn't spawn return 0; } \ No newline at end of file diff --git a/tests/sv-comp/cfg/free_spawn_ub_true-unreach-call.expected b/tests/sv-comp/cfg/free_spawn_ub_true-unreach-call.expected index 0a0df994d4..0aec5cffd0 100644 --- a/tests/sv-comp/cfg/free_spawn_ub_true-unreach-call.expected +++ b/tests/sv-comp/cfg/free_spawn_ub_true-unreach-call.expected @@ -1,27 +1,27 @@ -┌───────────────────────────────────┐ -│ _ │ -└───────────────────────────────────┘ +┌─────────────────────┐ +│ _ │ +└─────────────────────┘ │ │ Entry main ▼ -┌───────────────────────────────────┐ -│ _ │ -└───────────────────────────────────┘ +┌─────────────────────┐ +│ _ │ +└─────────────────────┘ │ - │ Assign 'p = (void (*)())(& foo)' + │ Assign 'p = & foo' ▼ -┌───────────────────────────────────┐ -│ _ │ -└───────────────────────────────────┘ +┌─────────────────────┐ +│ _ │ +└─────────────────────┘ │ │ Proc 'free(p)' ▼ -┌───────────────────────────────────┐ -│ _ │ -└───────────────────────────────────┘ +┌─────────────────────┐ +│ _ │ +└─────────────────────┘ │ │ Ret (Some 0, main) ▼ -┌───────────────────────────────────┐ -│ _ │ -└───────────────────────────────────┘ +┌─────────────────────┐ +│ _ │ +└─────────────────────┘