From 5cd0c45842d217da405563cfca925584d0994b91 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 18 Sep 2019 09:00:49 +0100 Subject: [PATCH] add_to_front method for code_with_references_listt This will make it easier to add declarations at the begginning of a list of codet after the rest of the code has been generated. --- jbmc/src/java_bytecode/code_with_references.cpp | 6 ++++++ jbmc/src/java_bytecode/code_with_references.h | 2 ++ 2 files changed, 8 insertions(+) diff --git a/jbmc/src/java_bytecode/code_with_references.cpp b/jbmc/src/java_bytecode/code_with_references.cpp index e1814bdde5..0055e6d935 100644 --- a/jbmc/src/java_bytecode/code_with_references.cpp +++ b/jbmc/src/java_bytecode/code_with_references.cpp @@ -68,3 +68,9 @@ void code_with_references_listt::append(code_with_references_listt &&other) { list.splice(list.end(), other.list); } + +void code_with_references_listt::add_to_front(code_without_referencest code) +{ + auto ptr = std::make_shared(std::move(code)); + list.emplace_front(std::move(ptr)); +} diff --git a/jbmc/src/java_bytecode/code_with_references.h b/jbmc/src/java_bytecode/code_with_references.h index fa9556e37d..ba775f88ad 100644 --- a/jbmc/src/java_bytecode/code_with_references.h +++ b/jbmc/src/java_bytecode/code_with_references.h @@ -101,6 +101,8 @@ public: void add(reference_allocationt ref); void append(code_with_references_listt &&other); + + void add_to_front(code_without_referencest code); }; #endif // CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H