From 45b8189fb5f28e2bdb6ba103f8c0c92b6cbd055f Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Fri, 6 Dec 2024 17:33:22 -0600 Subject: [PATCH] Added a test for conditional compilation with gc strategy flag. --- test/defn/imp.kore | 2 ++ test/lit.cfg.py | 7 +++++++ 2 files changed, 9 insertions(+) diff --git a/test/defn/imp.kore b/test/defn/imp.kore index 4ac67067f..bccd8575e 100644 --- a/test/defn/imp.kore +++ b/test/defn/imp.kore @@ -1,6 +1,8 @@ // RUN: %interpreter // RUN: %check-grep // RUN: %check-statistics +// RUN: %gcs-interpreter +// RUN: %check-grep // RUN: %proof-interpreter // RUN: %check-proof-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")] diff --git a/test/lit.cfg.py b/test/lit.cfg.py index 28f223eeb..cca48be9c 100644 --- a/test/lit.cfg.py +++ b/test/lit.cfg.py @@ -98,6 +98,13 @@ def exclude_x86_and_llvm18(s): exit 1 fi ''')), + ('%gcs-interpreter', one_line(''' + output=$(%kompile %s main --use-gcstrategy -o %t.interpreter 2>&1) + if [[ -n "$output" ]]; then + echo "llvm-kompile error or warning: $output" + exit 1 + fi + ''')), ('%proof-interpreter', one_line(''' output=$(%kompile %s main --proof-hint-instrumentation -o %t.interpreter 2>&1) if [[ -n "$output" ]]; then