From 466f12b3dc480b19bb0fd7db0788a5b86cd051f4 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 24 Sep 2018 11:27:00 +0100 Subject: [PATCH 1/3] Move contents of goto_program_template.cpp to goto_program.cpp goto_program_template.cpp seems to be a relict of times where we had goto_program_template.h --- src/goto-programs/Makefile | 1 - src/goto-programs/goto_program.cpp | 28 ++++++++++++++ src/goto-programs/goto_program_template.cpp | 42 --------------------- 3 files changed, 28 insertions(+), 43 deletions(-) delete mode 100644 src/goto-programs/goto_program_template.cpp diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 3dfa58eed2b..9fb7f85537f 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -19,7 +19,6 @@ SRC = adjust_float_expressions.cpp \ goto_inline_class.cpp \ goto_inline.cpp \ goto_program.cpp \ - goto_program_template.cpp \ goto_trace.cpp \ graphml_witness.cpp \ initialize_goto_model.cpp \ diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 48a99d276bd..4ebf5f469e7 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -698,3 +698,31 @@ bool goto_programt::equals(const goto_programt &other) const return true; } + +std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t) +{ + switch(t) + { + case NO_INSTRUCTION_TYPE: out << "NO_INSTRUCTION_TYPE"; break; + case GOTO: out << "GOTO"; break; + case ASSUME: out << "ASSUME"; break; + case ASSERT: out << "ASSERT"; break; + case OTHER: out << "OTHER"; break; + case DECL: out << "DECL"; break; + case DEAD: out << "DEAD"; break; + case SKIP: out << "SKIP"; break; + case START_THREAD: out << "START_THREAD"; break; + case END_THREAD: out << "END_THREAD"; break; + case LOCATION: out << "LOCATION"; break; + case END_FUNCTION: out << "END_FUNCTION"; break; + case ATOMIC_BEGIN: out << "ATOMIC_BEGIN"; break; + case ATOMIC_END: out << "ATOMIC_END"; break; + case RETURN: out << "RETURN"; break; + case ASSIGN: out << "ASSIGN"; break; + case FUNCTION_CALL: out << "FUNCTION_CALL"; break; + default: + out << "?"; + } + + return out; +} diff --git a/src/goto-programs/goto_program_template.cpp b/src/goto-programs/goto_program_template.cpp deleted file mode 100644 index 53dfafaf32a..00000000000 --- a/src/goto-programs/goto_program_template.cpp +++ /dev/null @@ -1,42 +0,0 @@ -/*******************************************************************\ - -Module: Goto Program Template - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Goto Program Template - -#include "goto_program.h" - -#include - -std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t) -{ - switch(t) - { - case NO_INSTRUCTION_TYPE: out << "NO_INSTRUCTION_TYPE"; break; - case GOTO: out << "GOTO"; break; - case ASSUME: out << "ASSUME"; break; - case ASSERT: out << "ASSERT"; break; - case OTHER: out << "OTHER"; break; - case DECL: out << "DECL"; break; - case DEAD: out << "DEAD"; break; - case SKIP: out << "SKIP"; break; - case START_THREAD: out << "START_THREAD"; break; - case END_THREAD: out << "END_THREAD"; break; - case LOCATION: out << "LOCATION"; break; - case END_FUNCTION: out << "END_FUNCTION"; break; - case ATOMIC_BEGIN: out << "ATOMIC_BEGIN"; break; - case ATOMIC_END: out << "ATOMIC_END"; break; - case RETURN: out << "RETURN"; break; - case ASSIGN: out << "ASSIGN"; break; - case FUNCTION_CALL: out << "FUNCTION_CALL"; break; - default: - out << "?"; - } - - return out; -} From c999fe5a9f215a0f4e986647819f1b01e2d004f3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 24 Sep 2018 11:28:03 +0100 Subject: [PATCH 2/3] Clang-format after moving a function. --- src/goto-programs/goto_program.cpp | 72 ++++++++++++++++++++++-------- 1 file changed, 53 insertions(+), 19 deletions(-) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 4ebf5f469e7..2f8d8bdd9e1 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -703,25 +703,59 @@ std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t) { switch(t) { - case NO_INSTRUCTION_TYPE: out << "NO_INSTRUCTION_TYPE"; break; - case GOTO: out << "GOTO"; break; - case ASSUME: out << "ASSUME"; break; - case ASSERT: out << "ASSERT"; break; - case OTHER: out << "OTHER"; break; - case DECL: out << "DECL"; break; - case DEAD: out << "DEAD"; break; - case SKIP: out << "SKIP"; break; - case START_THREAD: out << "START_THREAD"; break; - case END_THREAD: out << "END_THREAD"; break; - case LOCATION: out << "LOCATION"; break; - case END_FUNCTION: out << "END_FUNCTION"; break; - case ATOMIC_BEGIN: out << "ATOMIC_BEGIN"; break; - case ATOMIC_END: out << "ATOMIC_END"; break; - case RETURN: out << "RETURN"; break; - case ASSIGN: out << "ASSIGN"; break; - case FUNCTION_CALL: out << "FUNCTION_CALL"; break; - default: - out << "?"; + case NO_INSTRUCTION_TYPE: + out << "NO_INSTRUCTION_TYPE"; + break; + case GOTO: + out << "GOTO"; + break; + case ASSUME: + out << "ASSUME"; + break; + case ASSERT: + out << "ASSERT"; + break; + case OTHER: + out << "OTHER"; + break; + case DECL: + out << "DECL"; + break; + case DEAD: + out << "DEAD"; + break; + case SKIP: + out << "SKIP"; + break; + case START_THREAD: + out << "START_THREAD"; + break; + case END_THREAD: + out << "END_THREAD"; + break; + case LOCATION: + out << "LOCATION"; + break; + case END_FUNCTION: + out << "END_FUNCTION"; + break; + case ATOMIC_BEGIN: + out << "ATOMIC_BEGIN"; + break; + case ATOMIC_END: + out << "ATOMIC_END"; + break; + case RETURN: + out << "RETURN"; + break; + case ASSIGN: + out << "ASSIGN"; + break; + case FUNCTION_CALL: + out << "FUNCTION_CALL"; + break; + default: + out << "?"; } return out; From e98d8b9140f840da7791e3fd4c4044838a27d925 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 24 Sep 2018 14:09:56 +0100 Subject: [PATCH 3/3] Add doxygen --- src/goto-programs/goto_program.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 2f8d8bdd9e1..310e85c6d46 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -699,6 +699,7 @@ bool goto_programt::equals(const goto_programt &other) const return true; } +/// Outputs a string representation of a `goto_program_instruction_typet` std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t) { switch(t)