Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

bin/llvm-kompile-clang

@@ -256,7 +256,7 @@ if $link; then
       mkdir -p "$python_path"
 
       script_name="$(basename "$output_file").py"
-      cp "$LIBDIR/lldb/klldb.py" "$python_path/$script_name"
+      cp -f "$LIBDIR/lldb/klldb.py" "$python_path/$script_name"
     fi
   fi
 fi

test/defn/imp-slow-proof.kore renamed to test/defn/imp-sum-slow.kore

@@ -1,6 +1,5 @@
 // RUN: %proof-slow-interpreter
 // RUN: %check-proof-out
-// RUN: %check-expanded-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)")]
 
 module BASIC-K

test/defn/imp-proof.kore renamed to test/defn/imp-sum.kore

@@ -1,6 +1,5 @@
 // RUN: %proof-interpreter
 // RUN: %check-proof-out
-// RUN: %check-expanded-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)")]
 
 module BASIC-K

test/defn/imp.kore

@@ -1,5 +1,7 @@
 // RUN: %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)")]
 
 module BASIC-K

test/defn/kool-static.kore

@@ -1,5 +1,7 @@
 // RUN: %interpreter
 // RUN: %check-diff
+// RUN: %proof-interpreter
+// RUN: %check-proof-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md)")]
 
 module BASIC-K

test/defn/test-proof-trace-slow.kore

@@ -151,17 +151,7 @@ def one_line(s):
 
     ('%check-proof-out', one_line('''
         %run-proof-out
-        %kore-proof-trace --verbose %t.out.bin | diff - %test-proof-diff-out
-        result="$?"
-        if [ "$result" -ne 0 ]; then
-            echo "kore-proof-trace error while parsing proof hint trace"
-            exit 1
-        fi
-    ''')),
-
-    ('%check-expanded-proof-out', one_line('''
-        %run-proof-out
-        %kore-proof-trace --verbose --expand-terms %t.out.bin | diff - %test-proof-expanded-diff-out
+        %kore-proof-trace --verbose --expand-terms %t.out.bin | diff - %test-proof-diff-out
         result="$?"
         if [ "$result" -ne 0 ]; then
             echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms"
@@ -185,16 +175,14 @@ def one_line(s):
     ('%test-diff-out', os.path.join('%output-dir', '%test-basename.out.diff')),
     ('%test-dir-out', os.path.join('%output-dir', '%test-basename')),
     ('%test-dir-in', os.path.join('%input-dir', '%test-basename')),
-    ('%test-proof-diff-out', os.path.join('%output-dir', '%test-basename', '%test-basename.out.diff')),
-    ('%test-proof-expanded-diff-out', os.path.join('%output-dir', '%test-basename', '%test-basename.expanded.out.diff')),
+    ('%test-proof-diff-out', os.path.join('%output-dir', '%test-basename.proof.out.diff')),
     ('%test-basename', '`basename %s .kore`'),
 
     ('%allow-pipefail', 'set +o pipefail'),
 
     ('%kore-convert', 'kore-convert'),
 
     ('%kore-proof-trace', 'kore-proof-trace'),
-    ('%kore-proof-trace-test', 'kore-proof-trace-test'),
 ])
 
 config.recursiveExpansionLimit = 10