Added a test for conditional compilation with gc strategy flag.

runtimeverification · Dec 6, 2024 · 45b8189 · 45b8189
1 parent 01c324b
commit 45b8189
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git 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
@@ -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