test: Add goblint static analyser.

.github/workflows/ci.yml

@@ -16,7 +16,7 @@ jobs:
   analysis:
     strategy:
       matrix:
-        tool: [autotools, clang-tidy, compcert, cppcheck, doxygen, infer, misra, tcc, tokstyle]
+        tool: [autotools, clang-tidy, compcert, cppcheck, doxygen, goblint, infer, misra, tcc, tokstyle]
     runs-on: ubuntu-latest
     steps:
       - name: Set up Docker Buildx

other/docker/goblint/BUILD.bazel

@@ -0,0 +1,8 @@
+load("@rules_cc//cc:defs.bzl", "cc_library")
+
+cc_library(
+    name = "sodium",
+    testonly = True,
+    srcs = ["sodium.c"],
+    deps = ["@libsodium"],
+)

other/docker/goblint/Dockerfile

@@ -0,0 +1,26 @@
+FROM ghcr.io/goblint/analyzer:latest
+
+RUN apt-get update && \
+ DEBIAN_FRONTEND="noninteractive" apt-get install -y --no-install-recommends \
+ libsodium-dev \
+ tcc \
+ && apt-get clean \
+ && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /work
+COPY auto_tests/ /work/auto_tests/
+COPY testing/ /work/testing/
+COPY toxav/ /work/toxav/
+COPY toxcore/ /work/toxcore/
+COPY toxencryptsave/ /work/toxencryptsave/
+COPY third_party/ /work/third_party/
+
+COPY other/make_single_file /work/other/
+COPY other/docker/goblint/sodium.c /work/other/docker/goblint/
+
+RUN other/make_single_file -core auto_tests/tox_new_test.c other/docker/goblint/sodium.c > analysis.c
+# Try compiling+linking just to make sure we have all the fake functions.
+RUN tcc analysis.c
+
+COPY other/docker/goblint/analysis.json /work/other/docker/goblint/
+RUN /opt/goblint/analyzer/bin/goblint --conf /work/other/docker/goblint/analysis.json analysis.c

other/docker/goblint/analysis.json

@@ -0,0 +1,43 @@
+{
+	"ana": {
+		"activated": [
+			"base","mallocWrapper","escape","mutex","mutexEvents","access","assert","expRelation"
+		],
+		"arrayoob": true,
+		"wp": true,
+		"apron": {
+            "strengthening": true
+        },
+		"base": {
+			"structs" : {
+				"domain" : "combined-sk"
+			},
+			"arrays": {
+				"domain": "partitioned"
+			}
+		},
+		"malloc": {
+			"wrappers": [
+				"mem_balloc",
+				"mem_alloc",
+				"mem_valloc",
+				"mem_vrealloc"
+			]
+		}
+	},
+    "warn": {
+        "behavior": false,
+        "call": false,
+        "integer": true,
+        "float": false,
+        "race": false,
+        "deadcode": false,
+        "unsound": false,
+        "imprecise": false,
+        "success": false,
+        "unknown": false
+    },
+	"exp": {
+		"earlyglobs": true
+	}
+}

other/docker/goblint/run

@@ -0,0 +1,5 @@
+#!/bin/sh
+
+set -eux
+BUILD=goblint
+docker build -t "toxchat/c-toxcore:$BUILD" -f "other/docker/$BUILD/Dockerfile" .

other/docker/goblint/sodium.c

@@ -0,0 +1,112 @@
+#include <sodium.h>
+
+#include <string.h>
+
+int crypto_sign_keypair(unsigned char *pk, unsigned char *sk)
+{
+    memset(pk, 0, 32);
+    memset(sk, 0, 32);
+    return 0;
+}
+int crypto_sign_ed25519_pk_to_curve25519(unsigned char *curve25519_pk,
+                                         const unsigned char *ed25519_pk)
+{
+    memset(curve25519_pk, 0, 32);
+    return 0;
+}
+int crypto_sign_ed25519_sk_to_curve25519(unsigned char *curve25519_sk,
+                                         const unsigned char *ed25519_sk)
+{
+    memset(curve25519_sk, 0, 32);
+    return 0;
+}
+void sodium_memzero(void * const pnt, const size_t len)
+{
+    memset(pnt, 0, len);
+}
+int sodium_mlock(void * const addr, const size_t len)
+{
+    return 0;
+}
+int sodium_munlock(void * const addr, const size_t len)
+{
+    return 0;
+}
+int crypto_verify_32(const unsigned char *x, const unsigned char *y)
+{
+    return memcmp(x, y, 32);
+}
+int crypto_verify_64(const unsigned char *x, const unsigned char *y)
+{
+    return memcmp(x, y, 64);
+}
+int crypto_sign_detached(unsigned char *sig, unsigned long long *siglen_p,
+                         const unsigned char *m, unsigned long long mlen,
+                         const unsigned char *sk)
+{
+    return 0;
+}
+int crypto_sign_verify_detached(const unsigned char *sig,
+                                const unsigned char *m,
+                                unsigned long long mlen,
+                                const unsigned char *pk)
+{
+    return 0;
+}
+int crypto_box_beforenm(unsigned char *k, const unsigned char *pk,
+                        const unsigned char *sk)
+{
+    memset(k, 0, 32);
+    return 0;
+}
+int crypto_box_afternm(unsigned char *c, const unsigned char *m,
+                       unsigned long long mlen, const unsigned char *n,
+                       const unsigned char *k)
+{
+    memset(c, 0, 32);
+    return 0;
+}
+int crypto_box_open_afternm(unsigned char *m, const unsigned char *c,
+                            unsigned long long clen, const unsigned char *n,
+                            const unsigned char *k)
+{
+    return 0;
+}
+int crypto_scalarmult_curve25519_base(unsigned char *q,
+                                      const unsigned char *n)
+{
+    memset(q, 0, 32);
+    return 0;
+}
+int crypto_auth(unsigned char *out, const unsigned char *in,
+                unsigned long long inlen, const unsigned char *k)
+{
+    return 0;
+}
+int crypto_auth_verify(const unsigned char *h, const unsigned char *in,
+                       unsigned long long inlen, const unsigned char *k)
+{
+    return 0;
+}
+int crypto_hash_sha256(unsigned char *out, const unsigned char *in,
+                       unsigned long long inlen)
+{
+    return 0;
+}
+int crypto_hash_sha512(unsigned char *out, const unsigned char *in,
+                       unsigned long long inlen)
+{
+    return 0;
+}
+void randombytes(unsigned char * const buf, const unsigned long long buf_len)
+{
+    memset(buf, 0, buf_len);
+}
+uint32_t randombytes_uniform(const uint32_t upper_bound)
+{
+    return upper_bound;
+}
+int sodium_init(void)
+{
+    return 0;
+}