Add warnings about missing function declarations

src/framework/constraints.ml

@@ -296,7 +296,11 @@ struct
     in
     let one_function f =
       match Cil.unrollType f.vtype with
-      | TFun (_, params, var_arg, _)  ->
+      | TFun (_, params, var_arg, attrs)  ->
+        if Cil.hasAttribute "missingproto" attrs then (
+          M.msg_final Warning ~category:Program "Function declaration missing";
+          M.warn ~category:Program "Function declaration missing for %s" f.vname
+        );
         let arg_length = List.length args in
         let p_length = Option.map_default List.length 0 params in
         (* Check whether number of arguments fits. *)

tests/regression/00-sanity/02-minimal.c

@@ -1,3 +1,5 @@
+#include <goblint.h>
+
 int main() {
   __goblint_check(1); // reachable, formerly TERM
   return 0;

tests/regression/00-sanity/03-no_succ.c

@@ -1,3 +1,5 @@
+#include <goblint.h>
+
 int main() {
   __goblint_check(1); // reachable, formerly TERM
   return 0;

tests/regression/00-sanity/05-inf_loop.c

@@ -1,3 +1,5 @@
+#include <goblint.h>
+
 int main()
 {
   while (1);

tests/regression/00-sanity/06-term1.c

@@ -1,3 +1,5 @@
+#include <goblint.h>
+
 int main() {
   int i;
   while (1);

tests/regression/00-sanity/07-term2.c

@@ -1,4 +1,5 @@
 #include<stdlib.h>
+#include <goblint.h>
 
 void f() {
   exit(0);

tests/regression/00-sanity/08-asm_nop.c

@@ -1,3 +1,5 @@
+#include <goblint.h>
+
 int main() {
   __asm__ ("nop");
   __goblint_check(1); // reachable, formerly TERM

tests/regression/00-sanity/10-loop_label.c

@@ -1,3 +1,5 @@
+#include <goblint.h>
+
 int main () {
   while (1) {
     while_1_continue: /* CIL label */ ;

tests/regression/00-sanity/41-both_branches-2.c

@@ -4,6 +4,8 @@ struct S {
   int *f[1];
 };
 
+struct S *magic();
+
 int main() {
   struct S* s;
   s = magic();

tests/regression/01-cpa/34-def-exc.c

@@ -1,4 +1,5 @@
 // PARAM: --enable ana.int.def_exc --enable ana.int.interval
+#include <stdlib.h>
 #include <goblint.h>
 #define LONGS(x) (((x) + sizeof(unsigned long) - 1)/sizeof(unsigned long))
 #include<stdbool.h>

tests/regression/02-base/59-evalint-deep.c

@@ -2,7 +2,7 @@
 // contains deep integer expressions that shouldn't cause extremely exponential slowdown
 // when evaluated by base's eval_rv and EvalInt jointly
 // runs (as unknown) under 0.1s
-
+#include <stdlib.h>
 #include <goblint.h>
 void assume_abort_if_not(int cond) {
   if(!cond) {abort();}

tests/regression/02-base/80-unknown-no-spawn.c

@@ -2,6 +2,8 @@
 #include <goblint.h>
 #include <stddef.h>
 
+void magic(void (*)(void*));
+
 void *t_fun(void *arg) {
   __goblint_check(1); // NOWARN (unreachable)
   return NULL;

tests/regression/02-base/92-ad-union-fields.c

@@ -1,5 +1,7 @@
 // TODO: be sound and claim that assert may hold instead of must not hold
 // assert passes when compiled
+#include <stdlib.h>
+#include <assert.h>
 #include <goblint.h>
 
 union u {

tests/regression/03-practical/05-deslash.c

@@ -1,3 +1,6 @@
+#include <stdio.h>
+#include <goblint.h>
+
 int deslash(unsigned char *str) {
     unsigned char *wp, *rp;
 

tests/regression/03-practical/10-big_init.c

@@ -1,4 +1,6 @@
 // Just an example of slow initialization.
+#include <goblint.h>
+
 typedef unsigned char BYTE;
 BYTE Buffer[4096];
 

tests/regression/03-practical/16-union_index.c

@@ -1,3 +1,5 @@
+#include <goblint.h>
+
 typedef union {
    char c[4] ; // c needs to be at least as big as l
    long l ;

tests/regression/03-practical/31-zstd-cctxpool-blobs.c

@@ -1,5 +1,6 @@
 #include <stdlib.h>
 #include <pthread.h>
+#include <goblint.h>
 
 struct ZSTD_CCtx_s {
   int bmi2;

tests/regression/04-mutex/58-pthread-lock-return.c

@@ -1,5 +1,6 @@
 // PARAM: --disable sem.lock.fail
 #include <pthread.h>
+#include <goblint.h>
 
 int g_mutex = 0;
 pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;

tests/regression/04-mutex/94-thread-unsafe_fun_rc.c

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 #include <pthread.h>
 #include <stdio.h>
 

tests/regression/04-mutex/95-thread-unsafe_fun_nr.c

@@ -1,4 +1,5 @@
 #include <pthread.h>
+#include <stdlib.h>
 #include <stdio.h>
 
 pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;

tests/regression/04-mutex/98-thread-local-eq.c

@@ -1,6 +1,7 @@
 #include <pthread.h>
 #include <stdio.h>
 #include <assert.h>
+#include <goblint.h>
 
 __thread int myglobal;
 pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
@@ -10,7 +11,7 @@ void *t_fun(void *arg) {
   int top;
   int* ptr = (int*) arg;
 
-  if(top) { 
+  if(top) {
     ptr = &myglobal;
   }
 

tests/regression/05-lval_ls/17-per_elem_simp.c

@@ -1,5 +1,6 @@
-// PARAM: --set ana.activated[+] "'symb_locks'"  --set ana.activated[+] "'var_eq'" 
+// PARAM: --set ana.activated[+] "'symb_locks'"  --set ana.activated[+] "'var_eq'"
 #include <stdlib.h>
+#include <pthread.h>
 
 typedef long long pthread_t;
 typedef long long pthread_mutex_t;
@@ -15,8 +16,8 @@ struct t {
 };
 
 #define pack(v) (v)
-#define start_unpack(v) 
-#define end_unpack(v) 
+#define start_unpack(v)
+#define end_unpack(v)
 
 void* f(struct t* in) {
   start_unpack(in);
@@ -41,9 +42,9 @@ int main() {
     p = pack(s);
     random--;
   }
-  
+
   if (p == 0) exit(-1);
-  
+
   pthread_create(&t1, 0, f, p);
   pthread_create(&t2, 0, f, p);
   return 1;

tests/regression/05-lval_ls/20-race-null-void.c

@@ -1,5 +1,7 @@
 #include <pthread.h>
+#include <stdlib.h>
 #include <stdio.h>
+#include <goblint.h>
 
 void *t_fun(void *arg) {
   void **top;

tests/regression/05-lval_ls/21-race-null-type.c

@@ -1,6 +1,7 @@
 // PARAM: --enable ana.race.direct-arithmetic
 #include <pthread.h>
 #include <stdio.h>
+#include <goblint.h>
 
 void *t_fun(void *arg) {
   void *top;

tests/regression/05-lval_ls/22-race-null-void-deep.c

@@ -1,5 +1,6 @@
 #include <pthread.h>
 #include <stdio.h>
+#include <goblint.h>
 
 pthread_key_t key;
 

tests/regression/05-lval_ls/23-race-null-type-deep.c

@@ -1,5 +1,6 @@
 // PARAM: --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.spawn
 #include <pthread.h>
+#include <goblint.h>
 
 struct s {
   int f;

tests/regression/09-regions/07-kernel_list_rc.c

@@ -1,11 +1,12 @@
-// PARAM: --set ana.activated[+] "'region'"  --set kernel true --set nonstatic true 
+// PARAM: --set ana.activated[+] "'region'"  --set kernel true --set nonstatic true
 #include<linux/module.h>
 #include<linux/list.h>
 #include<linux/mutex.h>
+#include<linux/slab.h>
 
 struct s {
   struct list_head list;
-}; 
+};
 
 struct list_head A, B;
 
@@ -16,18 +17,18 @@ static DEFINE_MUTEX(B_mutex);
 void t1() {
   struct s *p = kmalloc(sizeof(struct s), GFP_KERNEL);
   INIT_LIST_HEAD(&p->list);
-  
+
   mutex_lock(&A_mutex);
-  list_add(&p->list, &A); 
-  if (p->list.next) 
+  list_add(&p->list, &A);
+  if (p->list.next)
     p->list.next->prev = NULL; //RACE
   mutex_unlock(&A_mutex);
 }
 
 void t2 () {
   struct s *p = kmalloc(sizeof(struct s), GFP_KERNEL);
   INIT_LIST_HEAD(&p->list);
-  
+
   mutex_lock(&B_mutex);
   list_add(&p->list, &A);
   mutex_unlock(&B_mutex);

tests/regression/09-regions/14-kernel_foreach_rc.c

@@ -2,11 +2,12 @@
 #include<linux/module.h>
 #include<linux/list.h>
 #include<linux/mutex.h>
+#include<linux/slab.h>
 
 struct s {
   int datum;
   struct list_head list;
-}; 
+};
 
 struct list_head slot[10];
 struct mutex slots_mutex[10];
@@ -19,20 +20,20 @@ struct s *new(int x) {
 }
 
 void t1(int i) {
-  struct s *p; 
-  
+  struct s *p;
+
   p = new(1);
   mutex_lock(&slots_mutex[i]);
-  list_add(&p->list, &slot[i]); 
+  list_add(&p->list, &slot[i]);
   p = new(2);
-  list_add(&p->list, &slot[i]); 
+  list_add(&p->list, &slot[i]);
   mutex_unlock(&slots_mutex[i]);
 }
 
 void t2 (int j) {
   struct s *pos;
   int j;
-  
+
   mutex_lock(&slots_mutex[j]);
   list_for_each_entry(pos, &slot[j+1], list) {
     pos->datum++; // RACE!

tests/regression/11-heap/03-linked.c

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 #include <goblint.h>
 
 struct list

tests/regression/11-heap/16-issue-1388.c

@@ -1,4 +1,6 @@
 // PARAM: --set ana.malloc.unique_address_count 2 --set ana.activated[-] threadid
+#include <stdlib.h>
+#include <goblint.h>
 
 typedef struct list {
  struct list *next;

tests/regression/11-heap/17-unique-mt.c

@@ -1,4 +1,5 @@
 // PARAM: --set ana.malloc.unique_address_count 3
+#include <stdlib.h>
 #include<pthread.h>
 static int iRThreads = 1;
 static int data1Value = 0;

tests/regression/11-heap/18-unique-st.c

@@ -1,4 +1,5 @@
 // PARAM: --set ana.malloc.unique_address_count 1 --set ana.autotune.activated '["reduceAnalyses"]' --enable ana.autotune.enabled
+#include <stdlib.h>
 #include<pthread.h>
 #include<goblint.h>
 

tests/regression/11-heap/19-malloc-zero.c

@@ -1,4 +1,5 @@
-// PARAM: --set sem.malloc.zero either --set ana.activated[+] memOutOfBounds 
+// PARAM: --set sem.malloc.zero either --set ana.activated[+] memOutOfBounds
+#include <stdlib.h>
 #include<pthread.h>
 #include<goblint.h>
 

tests/regression/13-privatized/80-nondet-struct-ptr.c

@@ -1,6 +1,8 @@
 // PARAM: --set ana.base.privatization protection --enable ana.int.enums
 #include<pthread.h>
 #include<stdlib.h>
+#include <goblint.h>
+
 struct a {
   int b;
 };

tests/regression/13-privatized/81-nondet-local-pointer.c

@@ -2,6 +2,8 @@
 // Like 80-nondet-struct-ptr.c, but somewhat simplified to not use structs and malloc etc
 #include<pthread.h>
 #include<stdlib.h>
+#include <goblint.h>
+
 struct a {
   int b;
 };

tests/regression/13-privatized/82-nondet-global-pointer.c

@@ -2,6 +2,8 @@
 // Like 81-nondet-struct-ptr.c, but with syntactic globals instead of escaping ones.
 #include<pthread.h>
 #include<stdlib.h>
+#include <goblint.h>
+
 struct a {
   int b;
 };

tests/regression/13-privatized/83-nondet-struct-ptr-write.c

@@ -1,6 +1,8 @@
 // PARAM: --set ana.base.privatization write --enable ana.int.enums
 #include<pthread.h>
 #include<stdlib.h>
+#include <goblint.h>
+
 struct a {
   int b;
 };

tests/regression/13-privatized/84-nondet-local-pointer-write.c

@@ -1,6 +1,8 @@
 // PARAM: --set ana.base.privatization write --enable ana.int.enums
 #include<pthread.h>
 #include<stdlib.h>
+#include <goblint.h>
+
 struct a {
   int b;
 };

tests/regression/13-privatized/85-nondet-global-pointer-write.c

@@ -1,6 +1,8 @@
 // PARAM: --set ana.base.privatization write --enable ana.int.enums
 #include<pthread.h>
 #include<stdlib.h>
+#include <goblint.h>
+
 struct a {
   int b;
 };

tests/regression/13-privatized/86-nondet-struct-ptr-lock.c

@@ -1,6 +1,8 @@
 // PARAM: --set ana.base.privatization lock --enable ana.int.enums
 #include<pthread.h>
 #include<stdlib.h>
+#include <goblint.h>
+
 struct a {
   int b;
 };

tests/regression/13-privatized/87-nondet-local-pointer-lock.c

@@ -1,6 +1,8 @@
 // PARAM: --set ana.base.privatization lock --enable ana.int.enums
 #include<pthread.h>
 #include<stdlib.h>
+#include <goblint.h>
+
 struct a {
   int b;
 };