Test rawTerm support

runtimeverification · Dec 7, 2023 · af324df · af324df
1 parent e8f261b
commit af324df
Show file tree

Hide file tree

Showing 6 changed files with 247 additions and 193 deletions.
diff --git a/include/runtime/header.h b/include/runtime/header.h
@@ -411,7 +411,7 @@ extern const uint32_t first_inj_tag, last_inj_tag;
 bool is_injection(block *);
 block *strip_injection(block *);
 block *constructKItemInj(void *subject, const char *sort, bool raw_value);
-block *constructRawTerm(void *subject, const char *sort);
+block *constructRawTerm(void *subject, const char *sort, bool raw_value);
 }
 
 std::string floatToString(const floating *);

diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp
@@ -453,7 +453,7 @@ void serializeTermToFile(
 
 void serializeRawTermToFile(
     const char *filename, void *subject, const char *sort) {
-  block *term = constructRawTerm(subject, sort);
+  block *term = constructRawTerm(subject, sort, true);
 
   char *data;
   size_t size;
@@ -467,7 +467,7 @@ void serializeRawTermToFile(
 std::shared_ptr<kllvm::KOREPattern>
 sortedTermToKorePattern(block *subject, const char *sort) {
   auto is_kitem = (std::string(sort) == "SortKItem{}");
-  block *term = is_kitem ? subject : constructRawTerm(subject, sort);
+  block *term = is_kitem ? subject : constructRawTerm(subject, sort, false);
 
   char *data_out;
   size_t size_out;

diff --git a/runtime/util/util.cpp b/runtime/util/util.cpp
@@ -29,10 +29,10 @@ block *constructKItemInj(void *subject, const char *sort, bool raw_value) {
   return static_cast<block *>(constructCompositePattern(tag, args));
 }
 
-block *constructRawTerm(void *subject, const char *sort) {
+block *constructRawTerm(void *subject, const char *sort, bool raw_value) {
   auto tag = getTagForSymbolName("rawTerm{}");
   auto args = std::vector{
-      static_cast<void *>(constructKItemInj(subject, sort, true))};
+      static_cast<void *>(constructKItemInj(subject, sort, raw_value))};
   return static_cast<block *>(constructCompositePattern(tag, args));
 }