copy language_file.cpp and language_file.h from CBMC

The logic implemented in CBMC's language_filest class typechecks modules
starting from the leaves of the dependency tree.  This is an ill-fit for
both SMV and Verilog, which expect elaboration and type checking to start
from the root (or "main") module.

This copies the file that contains the langauge_filet and language_filest
classes in order to make this change locally.

Author: kroening

src/ebmc/Makefile

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

src/ebmc/transition_system.cpp

@@ -17,14 +17,14 @@ Author: Daniel Kroening, [email protected]
 #include <util/unicode.h>
 
 #include <langapi/language.h>
-#include <langapi/language_file.h>
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
 #include <trans-word-level/show_module_hierarchy.h>
 #include <trans-word-level/show_modules.h>
 #include <verilog/verilog_types.h>
 
 #include "ebmc_error.h"
+#include "ebmc_language_file.h"
 #include "ebmc_version.h"
 #include "output_file.h"
 
@@ -132,7 +132,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
 static bool parse(
   const cmdlinet &cmdline,
   const std::string &filename,
-  language_filest &language_files,
+  ebmc_language_filest &language_files,
   message_handlert &message_handler)
 {
   messaget message(message_handler);
@@ -200,7 +200,7 @@ static bool parse(
 
 bool parse(
   const cmdlinet &cmdline,
-  language_filest &language_files,
+  ebmc_language_filest &language_files,
   message_handlert &message_handler)
 {
   for(unsigned i = 0; i < cmdline.args.size(); i++)
@@ -261,7 +261,7 @@ int get_transition_system(
   //
   // parsing
   //
-  language_filest language_files;
+  ebmc_language_filest language_files;
 
   if(parse(cmdline, language_files, message_handler))
     return 1;