From 965655e60f4adf0b92d7fc9fc849f7b073862bd0 Mon Sep 17 00:00:00 2001 From: Theodoros Kasampalis Date: Wed, 31 Jul 2024 14:42:08 -0500 Subject: [PATCH] Shared memory writer for proof hints (#1122) This PR adds a subclass of the abstract `proof_trace_writer` for outputting hints into a ringbuffer that lives in shared memory. This output method is intended to be used with the shared memory option of the `kore-proof-trace` parser to communicate hints through shared memory instead of through a file. Since we now can test the shared memory based proof generation/consumption loop, we also do not include the helper `kore-proof-trace-shm-writer` tool in the installation. --- include/kllvm/binary/serializer.h | 36 ++++++++++ lib/binary/serializer.cpp | 27 +++++++ runtime/main/main.ll | 13 +++- runtime/util/finish_rewriting.cpp | 72 +++++++++++++++++-- test/defn/imp-sum-slow.kore | 1 + test/defn/imp-sum.kore | 1 + test/defn/imp.kore | 1 + test/defn/kool-static.kore | 1 + test/lit.cfg.py | 20 ++++-- test/proof/add-rewrite.kore | 1 + test/proof/arith.kore | 1 + test/proof/assoc-function.kore | 1 + test/proof/builtin-functions.kore | 1 + test/proof/builtin-hook-events.kore | 1 + test/proof/builtin-int.kore | 1 + test/proof/builtin-io.kore | 1 + test/proof/builtin-json.kore | 1 + test/proof/cast.kore | 1 + test/proof/cell-collection.kore | 1 + test/proof/cell-value.kore | 1 + test/proof/concurrent-counters.kore | 1 + test/proof/conditional-function.kore | 1 + test/proof/custom-klabel-fun.kore | 1 + test/proof/decrement-int.kore | 1 + test/proof/decrement.kore | 1 + test/proof/double-rewrite.kore | 1 + test/proof/dv.kore | 1 + test/proof/exit-cell.kore | 1 + test/proof/fresh-gen.kore | 1 + test/proof/fun-context.kore | 1 + test/proof/imp.kore | 1 + test/proof/imp5-rw-literal.kore | 1 + test/proof/imp5-rw-succ.kore | 1 + test/proof/imp5.kore | 1 + test/proof/injections.kore | 1 + test/proof/is-zero.kore | 1 + test/proof/lambda-explicit-subst.kore | 1 + test/proof/let.kore | 1 + test/proof/list-assoc.kore | 1 + test/proof/list-cons.kore | 1 + test/proof/list-factory.kore | 1 + test/proof/list-semantic.kore | 1 + test/proof/macro.kore | 1 + test/proof/map-fun.kore | 1 + test/proof/memo-function.kore | 1 + test/proof/modular-config.kore | 1 + test/proof/nested-cells.kore | 1 + test/proof/non-rec-function.kore | 1 + test/proof/pcf.kore | 1 + test/proof/peano.kore | 1 + test/proof/prioritized-rule.kore | 1 + test/proof/projection.kore | 1 + test/proof/reg.kore | 1 + test/proof/set-fun.kore | 1 + test/proof/simple.kore | 1 + test/proof/single-rewrite.kore | 1 + test/proof/sum-cell.kore | 1 + test/proof/tree-reverse-int.kore | 1 + test/proof/tree-reverse.kore | 1 + test/proof/two-counters.kore | 1 + test/proof/type-cast.kore | 1 + .../CMakeLists.txt | 5 -- 62 files changed, 213 insertions(+), 16 deletions(-) diff --git a/include/kllvm/binary/serializer.h b/include/kllvm/binary/serializer.h index fe4cc4cd3..fd908d55b 100644 --- a/include/kllvm/binary/serializer.h +++ b/include/kllvm/binary/serializer.h @@ -2,6 +2,7 @@ #define AST_SERIALIZER_H #include +#include #include #include @@ -160,6 +161,8 @@ class proof_trace_writer { write(&n, 1); } + virtual void write_eof() = 0; + void write_bool(bool b) { write(&b, sizeof(bool)); } void write_uint32(uint32_t i) { write(&i, sizeof(uint32_t)); } void write_uint64(uint64_t i) { write(&i, sizeof(uint64_t)); } @@ -172,9 +175,42 @@ class proof_trace_file_writer : public proof_trace_writer { public: proof_trace_file_writer(FILE *file) : file_(file) { } + + void write(void const *ptr, size_t len) override; + void write_string(char const *str, size_t len) override; + void write_string(char const *str) override; + void write_eof() override { } +}; + +class proof_trace_ringbuffer_writer : public proof_trace_writer { +private: + shm_ringbuffer *shm_buffer_; + sem_t *data_avail_; + sem_t *space_avail_; + + void write(uint8_t const *ptr, size_t len = 1); + +public: + proof_trace_ringbuffer_writer( + void *shm_object, sem_t *data_avail, sem_t *space_avail) + : shm_buffer_(reinterpret_cast(shm_object)) + , data_avail_(data_avail) + , space_avail_(space_avail) { } + + ~proof_trace_ringbuffer_writer() override { shm_buffer_->~shm_ringbuffer(); } + + proof_trace_ringbuffer_writer(proof_trace_ringbuffer_writer const &) = delete; + proof_trace_ringbuffer_writer(proof_trace_ringbuffer_writer &&) = delete; + proof_trace_ringbuffer_writer & + operator=(proof_trace_ringbuffer_writer const &) + = delete; + proof_trace_ringbuffer_writer &operator=(proof_trace_ringbuffer_writer &&) + = delete; + void write(void const *ptr, size_t len) override; void write_string(char const *str, size_t len) override; void write_string(char const *str) override; + void write_eof() override; }; } // namespace kllvm diff --git a/lib/binary/serializer.cpp b/lib/binary/serializer.cpp index 5f30f2658..b9e0692f2 100644 --- a/lib/binary/serializer.cpp +++ b/lib/binary/serializer.cpp @@ -222,4 +222,31 @@ void proof_trace_file_writer::write_string(char const *str) { fputs(str, file_); } +void proof_trace_ringbuffer_writer::write(uint8_t const *ptr, size_t len) { + for (size_t i = 0; i < len; i++) { + sem_wait(space_avail_); + shm_buffer_->put(&ptr[i]); + sem_post(data_avail_); + } +} + +void proof_trace_ringbuffer_writer::write(void const *ptr, size_t len) { + auto const *data = reinterpret_cast(ptr); + write(data, len); +} + +void proof_trace_ringbuffer_writer::write_string(char const *str, size_t len) { + auto const *data = reinterpret_cast(str); + write(data, len); +} + +void proof_trace_ringbuffer_writer::write_string(char const *str) { + auto const *data = reinterpret_cast(str); + write(data, strlen(str)); +} + +void proof_trace_ringbuffer_writer::write_eof() { + shm_buffer_->put_eof(); +} + } // namespace kllvm diff --git a/runtime/main/main.ll b/runtime/main/main.ll index c4630c663..c74a34335 100644 --- a/runtime/main/main.ll +++ b/runtime/main/main.ll @@ -19,11 +19,13 @@ declare void @print_proof_hint_header(ptr) @statistics.flag = private constant [13 x i8] c"--statistics\00" @binary_out.flag = private constant [16 x i8] c"--binary-output\00" @proof_out.flag = private constant [15 x i8] c"--proof-output\00" +@use_shm.flag = private constant [20 x i8] c"--use-shared-memory\00" @proof_writer = external global ptr @statistics = external global i1 @binary_output = external global i1 @proof_output = external global i1 +@use_shm = external global i1 declare i32 @strcmp(ptr %a, ptr %b) @@ -63,10 +65,19 @@ binary.set: proof.body: %proof.cmp = call i32 @strcmp(ptr %arg, ptr getelementptr inbounds ([15 x i8], ptr @proof_out.flag, i64 0, i64 0)) %proof.eq = icmp eq i32 %proof.cmp, 0 - br i1 %proof.eq, label %proof.set, label %body.tail + br i1 %proof.eq, label %proof.set, label %shm.body proof.set: store i1 1, ptr @proof_output + br label %shm.body + +shm.body: + %shm.cmp = call i32 @strcmp(ptr %arg, ptr getelementptr inbounds ([20 x i8], ptr @use_shm.flag, i64 0, i64 0)) + %shm.eq = icmp eq i32 %shm.cmp, 0 + br i1 %shm.eq, label %shm.set, label %body.tail + +shm.set: + store i1 1, ptr @use_shm br label %body.tail body.tail: diff --git a/runtime/util/finish_rewriting.cpp b/runtime/util/finish_rewriting.cpp index 0e347956e..38ef22b9f 100644 --- a/runtime/util/finish_rewriting.cpp +++ b/runtime/util/finish_rewriting.cpp @@ -1,16 +1,21 @@ +#include + #include #include +#include #include #include +#include extern "C" { FILE *output_file = nullptr; -kllvm::proof_trace_writer *proof_writer = nullptr; +void *proof_writer = nullptr; bool statistics = false; bool binary_output = false; bool proof_output = false; +bool use_shm = false; extern int64_t steps; extern bool safe_partial; @@ -18,7 +23,55 @@ extern bool proof_hint_instrumentation_slow; int32_t get_exit_code(block *); +#define ERR_EXIT(msg) \ + do { \ + perror(msg); \ + exit(1); \ + } while (0) + +static void set_up_shm_writer(char const *output_filename) { + // Open existing shared memory object + int fd = shm_open(output_filename, O_RDWR, 0); + if (fd == -1) { + ERR_EXIT("shm_open writer"); + } + + // Map the object into the caller's address space + size_t shm_size = sizeof(kllvm::shm_ringbuffer); + void *shm_object + = mmap(nullptr, shm_size, PROT_READ | PROT_WRITE, MAP_SHARED, fd, 0); + if (shm_object == MAP_FAILED) { + ERR_EXIT("mmap writer"); + } + + // MacOS has deprecated unnamed semaphores, so we need to use named ones + std::string base_name(output_filename); + std::string data_avail_sem_name = base_name + ".d"; + std::string space_avail_sem_name = base_name + ".s"; + + // Open existing semaphores + // NOLINTNEXTLINE(*-pro-type-vararg) + sem_t *data_avail = sem_open(data_avail_sem_name.c_str(), 0); + if (data_avail == SEM_FAILED) { + ERR_EXIT("sem_init data_avail writer"); + } + // NOLINTNEXTLINE(*-pro-type-vararg) + sem_t *space_avail = sem_open(space_avail_sem_name.c_str(), 0); + if (space_avail == SEM_FAILED) { + ERR_EXIT("sem_init space_avail writer"); + } + + // Create the proof_trace_ringbuffer_writer object + proof_writer = new kllvm::proof_trace_ringbuffer_writer( + shm_object, data_avail, space_avail); +} + void init_outputs(char const *output_filename) { + if (proof_output && use_shm) { + set_up_shm_writer(output_filename); + return; + } + output_file = fopen(output_filename, "a"); if (proof_output) { proof_writer = new kllvm::proof_trace_file_writer(output_file); @@ -34,8 +87,8 @@ void init_outputs(char const *output_filename) { = std::unique_ptr(output_file, fclose); // Similar for deletinging the proof_output_buffer data structure - [[maybe_unused]] auto deleter - = std::unique_ptr(proof_writer); + auto *w = static_cast(proof_writer); + [[maybe_unused]] auto deleter = std::unique_ptr(w); if (error && safe_partial) { throw std::runtime_error( @@ -43,8 +96,10 @@ void init_outputs(char const *output_filename) { } if (!output_file) { - throw std::runtime_error( - "Called finish_rewriting with no output file specified"); + if (!proof_output || !use_shm) { + throw std::runtime_error( + "Called finish_rewriting with no output file specified"); + } } if (statistics) { @@ -58,11 +113,16 @@ void init_outputs(char const *output_filename) { print_configuration(output_file, subject); } } else if (!error && !proof_hint_instrumentation_slow) { - write_uint64_to_proof_trace(proof_writer, 0xFFFFFFFFFFFFFFFF); + w->write_uint64(0xFFFFFFFFFFFFFFFF); serialize_configuration_to_proof_writer(proof_writer, subject); } auto exit_code = error ? 113 : get_exit_code(subject); + + if (proof_output) { + w->write_eof(); + } + std::exit(exit_code); } } diff --git a/test/defn/imp-sum-slow.kore b/test/defn/imp-sum-slow.kore index b7cb28097..e5e978242 100644 --- a/test/defn/imp-sum-slow.kore +++ b/test/defn/imp-sum-slow.kore @@ -1,5 +1,6 @@ // RUN: %proof-slow-interpreter // RUN: %check-proof-out +// RUN: %check-proof-shm-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 diff --git a/test/defn/imp-sum.kore b/test/defn/imp-sum.kore index bed2ef8f6..e2524841b 100644 --- a/test/defn/imp-sum.kore +++ b/test/defn/imp-sum.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-proof-out +// RUN: %check-proof-shm-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 diff --git a/test/defn/imp.kore b/test/defn/imp.kore index 6d3528e56..0fd24d81b 100644 --- a/test/defn/imp.kore +++ b/test/defn/imp.kore @@ -2,6 +2,7 @@ // RUN: %check-grep // RUN: %proof-interpreter // RUN: %check-proof-out +// RUN: %check-proof-shm-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 diff --git a/test/defn/kool-static.kore b/test/defn/kool-static.kore index f18b73528..71109baa4 100644 --- a/test/defn/kool-static.kore +++ b/test/defn/kool-static.kore @@ -2,6 +2,7 @@ // RUN: %check-diff // RUN: %proof-interpreter // RUN: %check-proof-out +// RUN: %check-proof-shm-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 diff --git a/test/lit.cfg.py b/test/lit.cfg.py index f41b42714..9ad232e23 100644 --- a/test/lit.cfg.py +++ b/test/lit.cfg.py @@ -167,10 +167,14 @@ def one_line(s): echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms and streaming parser" exit 1 fi + ''')), + + ('%check-proof-shm-out', one_line(''' + %kore-rich-header %s > %t.header.bin %kore-proof-trace --shared-memory --verbose --expand-terms %t.header.bin %test-shm-buffer | diff - %test-proof-diff-out & reader_pid="$!" sleep 1 - %kore-proof-trace-shm-writer %t.out.bin %test-shm-buffer + %run-proof-shm-out wait $reader_pid result="$?" if [ "$result" -ne 0 ]; then @@ -196,11 +200,9 @@ def one_line(s): ('%check-dir-proof-out', one_line(''' %kore-rich-header %s > %t.header.bin - count=0 for out in %test-dir-out/*.proof.out.diff; do in=%test-dir-in/`basename $out .proof.out.diff`.in hint=%t.`basename $out .proof.out.diff`.hint - shmbuf=%test-shm-buffer.$count rm -f $hint %t.interpreter $in -1 $hint --proof-output %kore-proof-trace --verbose --expand-terms %t.header.bin $hint | diff - $out @@ -215,10 +217,19 @@ def one_line(s): echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms and streaming parser" exit 1 fi + done + ''')), + + ('%check-dir-proof-shm-out', one_line(''' + %kore-rich-header %s > %t.header.bin + count=0 + for out in %test-dir-out/*.proof.out.diff; do + in=%test-dir-in/`basename $out .proof.out.diff`.in + shmbuf=%test-shm-buffer.$count %kore-proof-trace --shared-memory --verbose --expand-terms %t.header.bin $shmbuf | diff - $out & reader_pid="$!" sleep 1 - %kore-proof-trace-shm-writer $hint $shmbuf + %t.interpreter $in -1 $shmbuf --proof-output --use-shared-memory wait $reader_pid result="$?" if [ "$result" -ne 0 ]; then @@ -232,6 +243,7 @@ def one_line(s): ('%run-binary-out', 'rm -f %t.out.bin && %t.interpreter %test-input -1 %t.out.bin --binary-output'), ('%run-binary', 'rm -f %t.bin && %convert-input && %t.interpreter %t.bin -1 /dev/stdout'), ('%run-proof-out', 'rm -f %t.out.bin && %t.interpreter %test-input -1 %t.out.bin --proof-output'), + ('%run-proof-shm-out', '%t.interpreter %test-input -1 %test-shm-buffer --proof-output --use-shared-memory'), ('%run', '%t.interpreter %test-input -1 /dev/stdout'), ('%kprint-check', 'kprint %S %s true | diff - %s.out'), diff --git a/test/proof/add-rewrite.kore b/test/proof/add-rewrite.kore index 0ea6bf1dc..ad1789080 100644 --- a/test/proof/add-rewrite.kore +++ b/test/proof/add-rewrite.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out // RUN: %check-proof-debug-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k)")] diff --git a/test/proof/arith.kore b/test/proof/arith.kore index 12ad87e57..16d36481f 100644 --- a/test/proof/arith.kore +++ b/test/proof/arith.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/arith/arith.k)")] module BASIC-K diff --git a/test/proof/assoc-function.kore b/test/proof/assoc-function.kore index d111c9a2e..dc2dbcfa1 100644 --- a/test/proof/assoc-function.kore +++ b/test/proof/assoc-function.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/assoc-function/assoc-function.k)")] module BASIC-K diff --git a/test/proof/builtin-functions.kore b/test/proof/builtin-functions.kore index e7b612112..f503f9771 100644 --- a/test/proof/builtin-functions.kore +++ b/test/proof/builtin-functions.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-functions/builtin-functions.k)")] module BASIC-K diff --git a/test/proof/builtin-hook-events.kore b/test/proof/builtin-hook-events.kore index 5880ce9c9..3d410de3f 100644 --- a/test/proof/builtin-hook-events.kore +++ b/test/proof/builtin-hook-events.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-hook-events/builtin-hook-events.k)")] module BASIC-K diff --git a/test/proof/builtin-int.kore b/test/proof/builtin-int.kore index 98e8e7869..e5fde6c2a 100644 --- a/test/proof/builtin-int.kore +++ b/test/proof/builtin-int.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-int/builtin-int.k)")] module BASIC-K diff --git a/test/proof/builtin-io.kore b/test/proof/builtin-io.kore index 00d4dd456..ce89bf38c 100644 --- a/test/proof/builtin-io.kore +++ b/test/proof/builtin-io.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-io/builtin-io.k)")] module BASIC-K diff --git a/test/proof/builtin-json.kore b/test/proof/builtin-json.kore index b40273eed..d9d279bf6 100644 --- a/test/proof/builtin-json.kore +++ b/test/proof/builtin-json.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/builtin-json/builtin-json.k)")] module BASIC-K diff --git a/test/proof/cast.kore b/test/proof/cast.kore index 39560d2a8..660f1d842 100644 --- a/test/proof/cast.kore +++ b/test/proof/cast.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/cast/cast.k)")] module BASIC-K diff --git a/test/proof/cell-collection.kore b/test/proof/cell-collection.kore index 0ba0adb8e..0ee8e18a6 100644 --- a/test/proof/cell-collection.kore +++ b/test/proof/cell-collection.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/cell-collection/cell-collection.k)")] module BASIC-K diff --git a/test/proof/cell-value.kore b/test/proof/cell-value.kore index 34bd91958..88b81dad4 100644 --- a/test/proof/cell-value.kore +++ b/test/proof/cell-value.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/cell-value/cell-value.k)")] module BASIC-K diff --git a/test/proof/concurrent-counters.kore b/test/proof/concurrent-counters.kore index 469d8e564..b0f2164a0 100644 --- a/test/proof/concurrent-counters.kore +++ b/test/proof/concurrent-counters.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/concurrent-counters/concurrent-counters.k)")] module BASIC-K diff --git a/test/proof/conditional-function.kore b/test/proof/conditional-function.kore index 485800310..ed10999ff 100644 --- a/test/proof/conditional-function.kore +++ b/test/proof/conditional-function.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/conditional-function/conditional-function.k)")] module BASIC-K diff --git a/test/proof/custom-klabel-fun.kore b/test/proof/custom-klabel-fun.kore index 29fdb1edc..f6dea8de6 100644 --- a/test/proof/custom-klabel-fun.kore +++ b/test/proof/custom-klabel-fun.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/custom-klabel-fun/custom-klabel-fun.k)")] module BASIC-K diff --git a/test/proof/decrement-int.kore b/test/proof/decrement-int.kore index 6e7e18299..3d32cb23d 100644 --- a/test/proof/decrement-int.kore +++ b/test/proof/decrement-int.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/decrement-int/decrement-int.k)")] module BASIC-K diff --git a/test/proof/decrement.kore b/test/proof/decrement.kore index 1a306d0f5..7481daa4e 100644 --- a/test/proof/decrement.kore +++ b/test/proof/decrement.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/decrement/decrement.k)")] module BASIC-K diff --git a/test/proof/double-rewrite.kore b/test/proof/double-rewrite.kore index 464b27884..fa49ec340 100644 --- a/test/proof/double-rewrite.kore +++ b/test/proof/double-rewrite.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/double-rewrite/double-rewrite.k)")] module BASIC-K diff --git a/test/proof/dv.kore b/test/proof/dv.kore index a34962262..5662341f8 100644 --- a/test/proof/dv.kore +++ b/test/proof/dv.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/dv/dv.k)")] module BASIC-K diff --git a/test/proof/exit-cell.kore b/test/proof/exit-cell.kore index e568bf2ff..2daf760f4 100644 --- a/test/proof/exit-cell.kore +++ b/test/proof/exit-cell.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/exit-cell/exit-cell.k)")] module BASIC-K diff --git a/test/proof/fresh-gen.kore b/test/proof/fresh-gen.kore index 9da218f6a..4b9a01b71 100644 --- a/test/proof/fresh-gen.kore +++ b/test/proof/fresh-gen.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/fresh-gen/fresh-gen.k)")] module BASIC-K diff --git a/test/proof/fun-context.kore b/test/proof/fun-context.kore index f7bc96cc7..1f7b0096f 100644 --- a/test/proof/fun-context.kore +++ b/test/proof/fun-context.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/fun-context/fun-context.k)")] module BASIC-K diff --git a/test/proof/imp.kore b/test/proof/imp.kore index 0d516736d..ad03f3369 100644 --- a/test/proof/imp.kore +++ b/test/proof/imp.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/imp/imp.k)")] module BASIC-K diff --git a/test/proof/imp5-rw-literal.kore b/test/proof/imp5-rw-literal.kore index cc1da17a8..acae11fde 100644 --- a/test/proof/imp5-rw-literal.kore +++ b/test/proof/imp5-rw-literal.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/imp5-rw-literal/imp5-rw-literal.k)")] module BASIC-K diff --git a/test/proof/imp5-rw-succ.kore b/test/proof/imp5-rw-succ.kore index 28582afe2..958346aeb 100644 --- a/test/proof/imp5-rw-succ.kore +++ b/test/proof/imp5-rw-succ.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/imp5-rw-succ/imp5-rw-succ.k)")] module BASIC-K diff --git a/test/proof/imp5.kore b/test/proof/imp5.kore index 23ce3e4c5..c8d63f433 100644 --- a/test/proof/imp5.kore +++ b/test/proof/imp5.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/imp5/imp5.k)")] module BASIC-K diff --git a/test/proof/injections.kore b/test/proof/injections.kore index 4783cf797..7a672af4c 100644 --- a/test/proof/injections.kore +++ b/test/proof/injections.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/injections/injections.k)")] module BASIC-K diff --git a/test/proof/is-zero.kore b/test/proof/is-zero.kore index f80d7a444..301bd0277 100644 --- a/test/proof/is-zero.kore +++ b/test/proof/is-zero.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/is-zero/is-zero.k)")] module BASIC-K diff --git a/test/proof/lambda-explicit-subst.kore b/test/proof/lambda-explicit-subst.kore index 5f9d96f73..3699b0988 100644 --- a/test/proof/lambda-explicit-subst.kore +++ b/test/proof/lambda-explicit-subst.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/lambda-explicit-subst/lambda-explicit-subst.k)")] module BASIC-K diff --git a/test/proof/let.kore b/test/proof/let.kore index f78e4a557..32b023317 100644 --- a/test/proof/let.kore +++ b/test/proof/let.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/let/let.k)")] module BASIC-K diff --git a/test/proof/list-assoc.kore b/test/proof/list-assoc.kore index 7069cdf4b..eab360297 100644 --- a/test/proof/list-assoc.kore +++ b/test/proof/list-assoc.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/list-assoc/list-assoc.k)")] module BASIC-K diff --git a/test/proof/list-cons.kore b/test/proof/list-cons.kore index 93e1fb3d8..917b257fe 100644 --- a/test/proof/list-cons.kore +++ b/test/proof/list-cons.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/list-cons/list-cons.k)")] module BASIC-K diff --git a/test/proof/list-factory.kore b/test/proof/list-factory.kore index acb714e6c..3ef6aa62f 100644 --- a/test/proof/list-factory.kore +++ b/test/proof/list-factory.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/list-factory/list-factory.k)")] module BASIC-K diff --git a/test/proof/list-semantic.kore b/test/proof/list-semantic.kore index 11925544d..b1732273e 100644 --- a/test/proof/list-semantic.kore +++ b/test/proof/list-semantic.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/list-semantic/list-semantic.k)")] module BASIC-K diff --git a/test/proof/macro.kore b/test/proof/macro.kore index 006242627..4decf3864 100644 --- a/test/proof/macro.kore +++ b/test/proof/macro.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/macro/macro.k)")] module BASIC-K diff --git a/test/proof/map-fun.kore b/test/proof/map-fun.kore index 4adedcc0a..54ca2c505 100644 --- a/test/proof/map-fun.kore +++ b/test/proof/map-fun.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/map-fun/map-fun.k)")] module BASIC-K diff --git a/test/proof/memo-function.kore b/test/proof/memo-function.kore index 060157361..f224e78b7 100644 --- a/test/proof/memo-function.kore +++ b/test/proof/memo-function.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/memo-function/memo-function.k)")] module BASIC-K diff --git a/test/proof/modular-config.kore b/test/proof/modular-config.kore index 2f2ffe0cd..bbff3b1cc 100644 --- a/test/proof/modular-config.kore +++ b/test/proof/modular-config.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/modular-config/modular-config.k)")] module BASIC-K diff --git a/test/proof/nested-cells.kore b/test/proof/nested-cells.kore index a70c3f940..ac5e6f899 100644 --- a/test/proof/nested-cells.kore +++ b/test/proof/nested-cells.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/nested-cells/nested-cells.k)")] module BASIC-K diff --git a/test/proof/non-rec-function.kore b/test/proof/non-rec-function.kore index d85054f6e..226c8a712 100644 --- a/test/proof/non-rec-function.kore +++ b/test/proof/non-rec-function.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/non-rec-function/non-rec-function.k)")] module BASIC-K diff --git a/test/proof/pcf.kore b/test/proof/pcf.kore index bd15570e5..32b996b01 100644 --- a/test/proof/pcf.kore +++ b/test/proof/pcf.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/pcf/pcf.k)")] module BASIC-K diff --git a/test/proof/peano.kore b/test/proof/peano.kore index 3588383ef..db287243a 100644 --- a/test/proof/peano.kore +++ b/test/proof/peano.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/peano/peano.k)")] module BASIC-K diff --git a/test/proof/prioritized-rule.kore b/test/proof/prioritized-rule.kore index 1f04a6414..b189779f3 100644 --- a/test/proof/prioritized-rule.kore +++ b/test/proof/prioritized-rule.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/prioritized-rule/prioritized-rule.k)")] module BASIC-K diff --git a/test/proof/projection.kore b/test/proof/projection.kore index fbea6c9fb..fb405cd7a 100644 --- a/test/proof/projection.kore +++ b/test/proof/projection.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/projection/projection.k)")] module BASIC-K diff --git a/test/proof/reg.kore b/test/proof/reg.kore index dcbd40dd1..5e9fb55a5 100644 --- a/test/proof/reg.kore +++ b/test/proof/reg.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/reg/reg.k)")] module BASIC-K diff --git a/test/proof/set-fun.kore b/test/proof/set-fun.kore index 6e9de67a8..991c3f42c 100644 --- a/test/proof/set-fun.kore +++ b/test/proof/set-fun.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/set-fun/set-fun.k)")] module BASIC-K diff --git a/test/proof/simple.kore b/test/proof/simple.kore index 288c58148..50f67af8c 100644 --- a/test/proof/simple.kore +++ b/test/proof/simple.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/simple/simple.k)")] module BASIC-K diff --git a/test/proof/single-rewrite.kore b/test/proof/single-rewrite.kore index f9e1f0c65..1b4ab3f4c 100644 --- a/test/proof/single-rewrite.kore +++ b/test/proof/single-rewrite.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/single-rewrite/single-rewrite.k)")] module BASIC-K diff --git a/test/proof/sum-cell.kore b/test/proof/sum-cell.kore index 620d81705..2ca51e4a5 100644 --- a/test/proof/sum-cell.kore +++ b/test/proof/sum-cell.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/sum-cell/sum-cell.k)")] module BASIC-K diff --git a/test/proof/tree-reverse-int.kore b/test/proof/tree-reverse-int.kore index 0951d02f8..589993ebb 100644 --- a/test/proof/tree-reverse-int.kore +++ b/test/proof/tree-reverse-int.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/tree-reverse-int/tree-reverse-int.k)")] module BASIC-K diff --git a/test/proof/tree-reverse.kore b/test/proof/tree-reverse.kore index 833f5cd2c..1389eff39 100644 --- a/test/proof/tree-reverse.kore +++ b/test/proof/tree-reverse.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/tree-reverse/tree-reverse.k)")] module BASIC-K diff --git a/test/proof/two-counters.kore b/test/proof/two-counters.kore index 90eb1b29d..52ac79a87 100644 --- a/test/proof/two-counters.kore +++ b/test/proof/two-counters.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/two-counters/two-counters.k)")] module BASIC-K diff --git a/test/proof/type-cast.kore b/test/proof/type-cast.kore index 43d54f2a8..51bd4e2e0 100644 --- a/test/proof/type-cast.kore +++ b/test/proof/type-cast.kore @@ -1,5 +1,6 @@ // RUN: %proof-interpreter // RUN: %check-dir-proof-out +// RUN: %check-dir-proof-shm-out [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/type-cast/type-cast.k)")] module BASIC-K diff --git a/tools/kore-proof-trace-shm-writer/CMakeLists.txt b/tools/kore-proof-trace-shm-writer/CMakeLists.txt index 19bda1990..b2c017ebe 100644 --- a/tools/kore-proof-trace-shm-writer/CMakeLists.txt +++ b/tools/kore-proof-trace-shm-writer/CMakeLists.txt @@ -5,8 +5,3 @@ kllvm_add_tool(kore-proof-trace-shm-writer target_link_libraries(kore-proof-trace-shm-writer PUBLIC BinaryKore ) - -install( - TARGETS kore-proof-trace-shm-writer - RUNTIME DESTINATION bin -)