Merge branch 'develop' into _update-deps/runtimeverification/hs-backe…

…nd-booster
runtimeverification · Dec 5, 2023 · 00a4666 · 00a4666
2 parents 2ce694f + d442b63
commit 00a4666
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 4 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/...tribution/pl-tutorial/2_languages/3_fun/1_untyped/2_substitution/fun-untyped.md b/...tribution/pl-tutorial/2_languages/3_fun/1_untyped/2_substitution/fun-untyped.md
@@ -2,6 +2,10 @@
 copyright: Copyright (c) K Team. All Rights Reserved.
 ---
 
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both substitution and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
 # FUN — Untyped — Substitution
 
 Author: Grigore Roșu ([email protected])  

diff --git a/k-distribution/pl-tutorial/2_languages/4_logik/basic/logik.md b/k-distribution/pl-tutorial/2_languages/4_logik/basic/logik.md
@@ -2,6 +2,9 @@
 copyright: Copyright (c) K Team. All Rights Reserved.
 ---
 
+// NOTE: this definition is not runnable as is.
+// It is intended for documentation and academic purposes only.
+
 # LOGIK
 
 Author: Grigore Roșu ([email protected])  

diff --git a/k-distribution/pl-tutorial/2_languages/4_logik/extended/exercises/logik-extended/logik.k b/k-distribution/pl-tutorial/2_languages/4_logik/extended/exercises/logik-extended/logik.k
@@ -1,4 +1,8 @@
 // Copyright (c) K Team. All Rights Reserved.
+
+// NOTE: this definition is not runnable as is.
+// It is intended for documentation and academic purposes only.
+
 require "unification.k"
 
 module LOGIK-COMMON

diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend
+2 −2		bin/llvm-kompile-clang
+5 −15		bindings/c/lib.cpp
+5 −0		bindings/core/src/core.cpp
+6 −3		bindings/python/ast.cpp
+5 −0		bindings/python/package/kllvm/__init__.py
+13 −4		bindings/python/runtime.cpp
+1 −1		debug/kgdb.py
+16 −13		include/kllvm/ast/AST.h
+27 −2		include/kllvm/binary/deserializer.h
+2 −0		include/kllvm/bindings/core/core.h
+2 −0		include/runtime/header.h
+3 −10		lib/ast/AST.cpp
+10 −16		lib/codegen/CreateTerm.cpp
+22 −32		lib/codegen/Decision.cpp
+72 −49		lib/codegen/EmitConfigParser.cpp
+3 −7		lib/codegen/ProofEvent.cpp
+4 −1		runtime/collections/lists.cpp
+5 −2		runtime/collections/maps.cpp
+4 −1		runtime/collections/rangemaps.cpp
+4 −1		runtime/collections/sets.cpp
+2 −3		runtime/util/ConfigurationParser.cpp
+17 −5		runtime/util/ConfigurationSerializer.cpp
+85 −0		test/defn/k-files/wasm-maps.k
+2,900 −0		test/defn/wasm-maps.kore
+1 −0		test/input/wasm-maps.in
+1 −0		test/output/wasm-maps.out.diff
+2,152 −0		test/python/Inputs/raw-term.kore
+6,145 −0		test/python/Inputs/sorts.kore
+4 −0		test/python/k-files/raw-term.k
+12 −0		test/python/k-files/sorts.k
+33 −0		test/python/test_raw_term.py
+26 −0		test/python/test_return_sorts.py
+3 −4		tools/llvm-kompile-codegen/main.cpp
+4 −0		unittests/runtime-collections/lists.cpp
+4 −0		unittests/runtime-ffi/ffi.cpp
+1 −0		unittests/runtime-strings/bytestest.cpp