Support C++-20

runtimeverification · Jan 11, 2024 · 904848f · 904848f
1 parent 276afab
commit 904848f
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 14 deletions.
diff --git a/cmake/KLLVMCompilerFlags.cmake b/cmake/KLLVMCompilerFlags.cmake
@@ -1,4 +1,4 @@
-set(CMAKE_CXX_STANDARD          17)
+set(CMAKE_CXX_STANDARD          20)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 set(CMAKE_CXX_EXTENSIONS        OFF)
 

diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h
@@ -103,10 +103,7 @@ class LLVMFunctionEvent : public LLVMStepEvent {
   std::vector<LLVMEvent> arguments;
 
   LLVMFunctionEvent(
-      std::string const &_name, std::string const &_relativePosition)
-      : name(_name)
-      , relativePosition(_relativePosition)
-      , arguments() { }
+      std::string const &_name, std::string const &_relativePosition);
 
 public:
   static sptr<LLVMFunctionEvent>
@@ -117,9 +114,9 @@ class LLVMFunctionEvent : public LLVMStepEvent {
 
   std::string const &getName() const { return name; }
   std::string const &getRelativePosition() const { return relativePosition; }
-  std::vector<LLVMEvent> const &getArguments() const { return arguments; }
+  std::vector<LLVMEvent> const &getArguments() const;
 
-  void addArgument(LLVMEvent const &argument) { arguments.push_back(argument); }
+  void addArgument(LLVMEvent const &argument);
 
   virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
 };
@@ -132,12 +129,7 @@ class LLVMHookEvent : public LLVMStepEvent {
   sptr<KOREPattern> korePattern;
   uint64_t patternLength;
 
-  LLVMHookEvent(std::string const &_name, std::string const &_relativePosition)
-      : name(_name)
-      , relativePosition(_relativePosition)
-      , arguments()
-      , korePattern(nullptr)
-      , patternLength(0u) { }
+  LLVMHookEvent(std::string const &_name, std::string const &_relativePosition);
 
 public:
   static sptr<LLVMHookEvent>
@@ -155,7 +147,7 @@ class LLVMHookEvent : public LLVMStepEvent {
     patternLength = _patternLength;
   }
 
-  void addArgument(LLVMEvent const &argument) { arguments.push_back(argument); }
+  void addArgument(LLVMEvent const &argument);
 
   virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
 };

diff --git a/lib/binary/ProofTraceParser.cpp b/lib/binary/ProofTraceParser.cpp
@@ -6,6 +6,32 @@ namespace kllvm {
 
 constexpr auto indent_size = 2u;
 
+LLVMFunctionEvent::LLVMFunctionEvent(
+    std::string const &_name, std::string const &_relativePosition)
+    : name(_name)
+    , relativePosition(_relativePosition)
+    , arguments() { }
+
+std::vector<LLVMEvent> const &LLVMFunctionEvent::getArguments() const {
+  return arguments;
+}
+
+void LLVMFunctionEvent::addArgument(LLVMEvent const &argument) {
+  arguments.push_back(argument);
+}
+
+LLVMHookEvent::LLVMHookEvent(
+    std::string const &_name, std::string const &_relativePosition)
+    : name(_name)
+    , relativePosition(_relativePosition)
+    , arguments()
+    , korePattern(nullptr)
+    , patternLength(0u) { }
+
+void LLVMHookEvent::addArgument(LLVMEvent const &argument) {
+  arguments.push_back(argument);
+}
+
 void LLVMRewriteEvent::printSubstitution(
     std::ostream &Out, unsigned indent) const {
   std::string Indent(indent * indent_size, ' ');