Added JSIL support to cbmc, goto-cc, goto-analyzer

Author: tautschnig

src/cbmc/Makefile

@@ -55,6 +55,11 @@ ifneq ($(wildcard ../java_bytecode/Makefile),)
   endif
 endif
 
+ifneq ($(wildcard ../jsil/Makefile),)
+  OBJ += ../jsil/jsil$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_JSIL
+endif
+
 ifneq ($(wildcard ../specc/Makefile),)
   OBJ += ../specc/specc$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_SPECC

src/cbmc/cbmc_languages.cpp

@@ -19,6 +19,10 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/java_bytecode_language.h>
 #endif
 
+#ifdef HAVE_JSIL
+#include <jsil/jsil_language.h>
+#endif
+
 #include "cbmc_parse_options.h"
 
 /*******************************************************************\
@@ -45,5 +49,9 @@ void cbmc_parse_optionst::register_languages()
   #ifdef HAVE_JAVA_BYTECODE
   register_language(new_java_bytecode_language);
   #endif
+
+  #ifdef HAVE_JSIL
+  register_language(new_jsil_language);
+  #endif
 }
 

src/goto-analyzer/Makefile

@@ -35,6 +35,11 @@ ifneq ($(wildcard ../java_bytecode/Makefile),)
   endif
 endif
 
+ifneq ($(wildcard ../jsil/Makefile),)
+  OBJ += ../jsil/jsil$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_JSIL
+endif
+
 ifneq ($(wildcard ../specc/Makefile),)
   OBJ += ../specc/specc$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_SPECC

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 #include <java_bytecode/java_bytecode_language.h>
+#include <jsil/jsil_language.h>
 
 #include <goto-programs/set_properties.h>
 #include <goto-programs/remove_function_pointers.h>
@@ -79,6 +80,7 @@ void goto_analyzer_parse_optionst::register_languages()
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
   register_language(new_java_bytecode_language);
+  register_language(new_jsil_language);
 }
 
 /*******************************************************************\

src/goto-cc/Makefile

@@ -40,6 +40,11 @@ ifneq ($(wildcard ../java_bytecode/Makefile),)
   endif
 endif
 
+ifneq ($(wildcard ../jsil/Makefile),)
+  OBJ += ../jsil/jsil$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_JSIL
+endif
+
 ###############################################################################
 
 goto-cc$(EXEEXT): $(OBJ)

src/goto-cc/compile.cpp

@@ -179,7 +179,8 @@ bool compilet::add_input_file(const std::string &file_name)
      ext=="i" ||
      ext=="ii" ||
      ext=="class" ||
-     ext=="jar")
+     ext=="jar" ||
+     ext=="jsil")
   {
     source_files.push_back(file_name);
   }

src/goto-cc/goto_cc_languages.cpp

@@ -11,6 +11,7 @@ Author: CM Wintersteiger
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 #include <java_bytecode/java_bytecode_language.h>
+#include <jsil/jsil_language.h>
 
 #ifdef HAVE_SPECC
 #include <specc/specc_language.h>
@@ -35,6 +36,7 @@ void goto_cc_modet::register_languages()
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
   register_language(new_java_bytecode_language);
+  register_language(new_jsil_language);
 
   #ifdef HAVE_SPECC
   register_language(new_specc_language);