diff --git a/CHANGELOG.md b/CHANGELOG.md index b6c2b71..a8b1f30 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,17 +2,16 @@ All notable changes to this project will be documented in this file. -## [2.1.0] - 2024-04-19 +## [2.1.0] - 2024-04-21 ### Changed -- Added installation goal to Makefile +- Added installation goal to Makefile (`PREFIX` envvar) - Added tools.RegEnv which requires envvars to be registered and documented ### Added -- Dockerfile with GenMC v0.10.1-a (from open-s4c/genmc) -- Dockerfile with Dat3m v4.0.1 +- Dockerfile with clang v14, GenMC v0.10.1-a (open-s4c/genmc) and Dartagnan v4.0.1 - vsyncer docker command - Several configuration options (see `vsyncer -h`) - `vsyncer` releases with binaries for Linux, Windows and macOS diff --git a/Dockerfile b/Dockerfile index 6853e5b..7dfaa9a 100644 --- a/Dockerfile +++ b/Dockerfile @@ -35,16 +35,18 @@ RUN apt-get update \ RUN cd /tmp \ && git clone --depth 1 --branch "v0.9" \ - https://github.com/open-s4c/genmc.git genmc9 \ - && cd genmc9 \ + https://github.com/open-s4c/genmc.git genmc9 + +RUN cd /tmp/genmc9 \ && autoreconf --install \ && ./configure --prefix=/usr/share/genmc9 \ && make install -j8 RUN cd /tmp \ && git clone --depth 1 --branch "v0.10.1-a" \ - https://github.com/open-s4c/genmc.git genmc10 \ - && cd genmc10 \ + https://github.com/open-s4c/genmc.git genmc10 + +RUN cd /tmp/genmc10 \ && autoreconf --install \ && ./configure --prefix=/usr/share/genmc10 \ && make install -j8 @@ -65,10 +67,8 @@ RUN apt-get update \ && rm -rf /var/lib/apt/lists/* RUN cd /tmp \ - && git clone \ - https://github.com/hernanponcedeleon/dat3m.git \ - && cd dat3m \ - && git checkout "8d22e4283f26473ed88e226480d84acaf09fad07" + && git clone --depth 1 --branch "4.0.1" \ + https://github.com/hernanponcedeleon/dat3m.git RUN cd /tmp/dat3m \ && mvn clean install -DskipTests \ diff --git a/checker/checker_dartagnan.go b/checker/checker_dartagnan.go index 4c26a29..86110b2 100644 --- a/checker/checker_dartagnan.go +++ b/checker/checker_dartagnan.go @@ -30,6 +30,8 @@ func init() { tools.RegEnv("DARTAGNAN_SET_OPTIONS", "", "Options passed to Dartagnan, replacing the default options") tools.RegEnv("DARTAGNAN_CAT_PATH", "", "Path to custom .cat files") + tools.RegEnv("DARTAGNAN_METHOD", "eager", "Backend method (values: eager | lazy)") + tools.RegEnv("DARTAGNAN_BOUND", "", "Unroll bound integer (default unset)") } // NewDartagnan creates a new checker using Dartagnan model checker. @@ -95,6 +97,14 @@ func (c *DartagnanChecker) run(ctx context.Context, testFn string) (string, erro opts = strings.Split(env, " ") } + if env := tools.GetEnv("DARTAGNAN_METHOD"); env != "" { + opts = append(opts, fmt.Sprintf("--method=%s", env)) + } + + if env := tools.GetEnv("DARTAGNAN_BOUND"); env != "" { + opts = append(opts, fmt.Sprintf("--bound=%s", env)) + } + dartagnanHome := tools.GetEnv("DARTAGNAN_HOME") args := append([]string{"-jar", dartagnanHome + "/dartagnan/target/dartagnan.jar",