new transition system language API

This adds an API for obtaining a transition system from a source modeling
language, designed to suit Verilog, SMV and similar languages.

Author: kroening

src/ebmc/Makefile

@@ -12,6 +12,7 @@ SRC = \
       diatest.cpp \
       dimacs_writer.cpp \
       ebmc_base.cpp \
+      ebmc_language.cpp \
       ebmc_language_file.cpp \
       ebmc_languages.cpp \
       ebmc_parse_options.cpp \

src/ebmc/ebmc_language.cpp

@@ -0,0 +1,13 @@
+/*******************************************************************\
+
+Module: Abstract interface to support a modeling language
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "ebmc_language.h"
+
+ebmc_languaget::~ebmc_languaget()
+{
+}

src/ebmc/ebmc_language.h

@@ -0,0 +1,43 @@
+/*******************************************************************\
+
+Module: Abstract interface to support a modeling language
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Abstract interface to support a modeling language
+
+#ifndef EBMC_LANGUAGE_H
+#define EBMC_LANGUAGE_H
+
+#include <iosfwd>
+
+class cmdlinet;
+class message_handlert;
+class transition_systemt;
+
+class ebmc_languaget
+{
+public:
+  // constructor / destructor
+  ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler)
+    : cmdline(_cmdline), message_handler(_message_handler)
+  {
+  }
+
+  virtual ~ebmc_languaget();
+
+  /// produce diagnostic output as specified on the command line
+  virtual void diagnostics() = 0;
+
+  /// produce the transition system, and return it
+  virtual transition_systemt transition_system() = 0;
+
+protected:
+  cmdlinet &cmdline;
+  message_handlert &message_handler;
+};
+
+#endif // EBMC_LANGUAGE_H