Merge branch 'master' into interactive

Author: sim642

.devcontainer/Dockerfile

@@ -1,9 +1,9 @@
 # just -opam tag because make setup will install ocaml compiler
-FROM ocaml/opam:ubuntu-21.04-opam AS dev
+FROM ocaml/opam:ubuntu-22.04-opam AS dev
 
 # TODO: use opam depext
 RUN sudo apt-get update \
-    && sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf pkg-config ruby gem curl
+    && sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf gcc-multilib pkg-config ruby gem curl
 
 # remove default Docker <[email protected]> git credentials added by opam base image: https://github.com/avsm/ocaml-dockerfile/blob/f184554282a3836bf3f1c34d20e77d0530f8349d/src-opam/dockerfile_linux.ml#L24-L28
 # this prevents devcontainer from using outside git credentials: https://code.visualstudio.com/docs/remote/containers#_sharing-git-credentials-with-your-container

.github/workflows/locked.yml

@@ -57,6 +57,44 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+  extraction:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-latest
+        ocaml-compiler:
+          - 4.14.0 # matches opam lock file
+          # don't add any other because they won't be used
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v3
+
+      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
+        env:
+          # otherwise setup-ocaml pins non-locked dependencies
+          # https://github.com/ocaml/setup-ocaml/issues/166
+          OPAMLOCKED: locked
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+      - name: Install spin
+        run: sudo apt-get -y install spin
+
+      - name: Install dependencies
+        run: opam install . --deps-only --locked --with-test
+
+      - name: Build
+        run: ./make.sh nat
+
+      - name: Test extraction
+        run: cd tests/extraction && ./test.sh
+
+
   gobview:
     strategy:
       fail-fast: false

.gitignore

@@ -22,6 +22,7 @@ doclist.odocl
 autom4te.cache
 mytests
 result/*
+pml-result/*
 tests/regression/*/goblint_temp
 linux-headers
 

Dockerfile

@@ -1,14 +1,14 @@
 # dev stage: development environment with opam, ocaml and dependencies
 
 # just -opam tag because make setup will install ocaml compiler
-FROM ocaml/opam:ubuntu-21.04-opam AS dev
+FROM ocaml/opam:ubuntu-22.04-opam AS dev
 
 # copy only files for make setup to cache docker layers without code changes
 COPY --chown=opam Makefile make.sh goblint.opam goblint.opam.locked /home/opam/analyzer/
 WORKDIR /home/opam/analyzer/
 # TODO: use opam depext
 RUN sudo apt-get update \
-    && sudo apt-get install -y libgmp-dev libmpfr-dev pkg-config autoconf
+    && sudo apt-get install -y libgmp-dev libmpfr-dev pkg-config autoconf gcc-multilib
 # update local opam repository because base image may be outdated
 RUN cd /home/opam/opam-repository \
     && git pull origin master \
@@ -27,12 +27,12 @@ RUN make relocatable
 
 
 # final stage: minimal run environment for small docker image
-FROM ubuntu:21.04
+FROM ubuntu:22.04
 
 # cannot use opam depext because no opam here, also additional preprocessing/header dependencies
 # libgmp for zarith, libmpfr for apron, cpp for preprocessing, libc6 for pthread.h, libgcc for stddef.h
 RUN apt-get update \
-    && apt-get install -y libgmp-dev libmpfr-dev cpp libc6-dev libgcc-10-dev \
+    && apt-get install -y libgmp-dev libmpfr-dev cpp libc6-dev libc6-dev-i386 libgcc-11-dev lib32gcc-11-dev \
     && rm -rf /var/lib/apt/lists/*
 COPY --from=relocatable /home/opam/analyzer/relocatable /opt/goblint/analyzer
 ENTRYPOINT ["/opt/goblint/analyzer/bin/goblint"]