Merge branch 'develop' into HOTFIX-Int2Bytes-refactoring-no-2

runtimeverification · Jul 21, 2024 · c9a7794 · c9a7794
2 parents 6225293 + 343c564
commit c9a7794
Show file tree

Hide file tree

Showing 8 changed files with 12 additions and 12 deletions.
diff --git a/.github/workflows/update-deps.yml b/.github/workflows/update-deps.yml
@@ -59,7 +59,7 @@ jobs:
           cd llvm-backend/src/main/native/llvm-backend
           git checkout "${llvm_backend_version}"
           cd -
-          sed -i 's!      url = "github:runtimeverification/llvm-backend/.*";!      url = "github:runtimeverification/llvm-backend/'"${llvm_backend_version}"'";!' flake.nix
+          sed -i 's!    llvm-backend.url = "github:runtimeverification/llvm-backend/.*";!    llvm-backend.url = "github:runtimeverification/llvm-backend/'"${llvm_backend_version}"'";!' flake.nix
           if git add flake.nix llvm-backend/src/main/native/llvm-backend && git commit -m "flake.nix, llvm-backend/src/main/native/llvm-backend: update to version ${llvm_backend_version}"; then
             changed=true
           fi

diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release
@@ -1 +1 @@
-v0.1.40
+v0.1.46
diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release
@@ -1 +1 @@
-0.1.57
+0.1.59
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.56";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.59";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.32";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend
diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend
diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py
@@ -201,7 +201,7 @@ def name(self) -> str:
 
     @property
     def relative_position(self) -> str:
-        """Return the relative position of the LLVM function event in the proof trace. Ex.: (0:0:0:0)."""
+        """Return the relative position of the LLVM function event in the proof trace."""
         return self._function_event.relative_position
 
     @property
@@ -243,7 +243,7 @@ def name(self) -> str:
 
     @property
     def relative_position(self) -> str:
-        """Return the relative position of the hook event in the proof trace. Ex.: (0:0:0:0)."""
+        """Return the relative position of the hook event in the proof trace."""
         return self._hook_event.relative_position
 
     @property
+2 −0		.github/workflows/master.yml
+14 −33		booster/library/Booster/CLOptions.hs
+4 −9		booster/library/Booster/LLVM.hs
+2 −94		booster/library/Booster/LLVM/Internal.hs
+51 −31		booster/library/Booster/SMT/Interface.hs
+0 −124		booster/library/Booster/Trace.hs
+0 −96		booster/library/Booster/Trace/TH.hs
+1 −2		booster/package.yaml
+1 −1		booster/test/rpc-integration/test-collectiontest/README.md
+2 −29		booster/test/rpc-integration/test-collectiontest/state-map-lookup.simplify
+2 −2		booster/test/rpc-integration/test-collectiontest/state-map-lookupOrDefault.simplify
+0 −6		booster/tools/booster/Server.hs
+2 −1		booster/tools/rpc-client/RpcClient.hs
+1 −1		deps/k_release
+1 −6		dev-tools/booster-dev/Server.hs
+0 −382		dev-tools/eventlog-parser/EventlogParser.hs
+0 −111		dev-tools/eventlog-parser/FrameDict.hs
+1 −7		dev-tools/kore-rpc-dev/Server.hs
+1 −22		dev-tools/package.yaml
+1 −1		kore-rpc-types/kore-rpc-types.cabal
+15 −8		kore/app/share/GlobalMain.hs
+2 −1		kore/kore.cabal
+1 −1		package/debian/changelog
+1 −1		package/version
+21 −5		bin/llvm-kompile-clang
+12 −0		bindings/c/include/kllvm-c/kllvm-c.h
+11 −0		bindings/c/lib.cpp
+1 −1		bindings/core/CMakeLists.txt
+22 −0		bindings/core/src/core.cpp
+2 −1		include/kllvm/ast/AST.h
+8 −0		include/kllvm/bindings/core/core.h
+1 −0		lib/codegen/ApplyPasses.cpp
+1 −1		nix/llvm-backend.nix
+1 −1		package/debian/changelog
+1 −1		package/version
+40 −0		test/c/Inputs/flat-namespace.c
+6,525 −0		test/c/flat-namespace.kore
+14 −0		test/c/k-files/flat-namespace.k
+1 −4		tools/k-rule-apply/CMakeLists.txt
+0 −83		tools/k-rule-apply/auxiliar.h
+30 −46		tools/k-rule-apply/main.cpp
+86 −0		tools/k-rule-apply/shims.cpp
+33 −0		tools/k-rule-apply/shims.h