Remove JSIL front-end

We do not have any tests and JSIL is not being developed any further at
https://vtss.doc.ic.ac.uk/research/javascript.html.

Author: tautschnig

.gitignore

@@ -91,10 +91,6 @@ src/ansi-c/ansi_c_y.tab.cpp
 src/ansi-c/ansi_c_y.tab.h
 src/assembler/assembler_lex.yy.cpp
 src/crangler/c_lex.yy.cpp
-src/jsil/jsil_lex.yy.cpp
-src/jsil/jsil_y.output
-src/jsil/jsil_y.tab.cpp
-src/jsil/jsil_y.tab.h
 src/json/json_lex.yy.cpp
 src/json/json_y.output
 src/json/json_y.tab.cpp

CMakeLists.txt

@@ -256,7 +256,6 @@ cprover_default_properties(
     goto-symex
     goto-synthesizer
     goto-synthesizer-lib
-    jsil
     json
     json-symtab-language
     langapi

CODEOWNERS

@@ -56,7 +56,6 @@
 /src/goto-inspect/ @diffblue/diffblue-opensource
 /src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-diff/ @tautschnig @peterschrammel
-/src/jsil/ @kroening @tautschnig
 /src/memory-analyzer/ @tautschnig @kroening
 /jbmc/src/jbmc/ @peterschrammel @TGWDB
 /jbmc/src/janalyzer/ @peterschrammel @TGWDB

doc/architectural/folder-walkthrough.md

@@ -32,7 +32,6 @@ containing the code for a different part of the system.
   * C: \ref ansi-c
   * C++: \ref cpp
   * Java: \ref java_bytecode
-  * JavaScript: \ref jsil
 
 - Tools
 
@@ -155,7 +154,6 @@ digraph directory_dependencies {
     ansi_c [label = "ansi-c", URL = "\ref ansi-c"];
     langapi [URL = "\ref langapi"];
     cpp [URL = "\ref cpp"];
-    jsil [URL = "\ref jsil"];
     java_bytecode [URL = "\ref java_bytecode"];  
   }
 
@@ -174,15 +172,14 @@ digraph directory_dependencies {
   JBMC -> { CBMC, java_bytecode };
   jdiff -> { goto_diff, java_bytecode };
   janalyzer -> { goto_analyzer, java_bytecode };
-  CBMC -> { goto_instrument, jsil };
+  CBMC -> { goto_instrument };
   goto_diff -> { goto_instrument };
-  goto_analyzer -> { analyses, jsil, cpp };
+  goto_analyzer -> { analyses, cpp };
   goto_instrument -> { goto_symex, cpp };
-  goto_cc -> { cpp, jsil };
+  goto_cc -> { cpp };
   smt2_solver -> solvers;
 
   java_bytecode -> { analyses, miniz };
-  jsil -> linking;
   cpp -> ansi_c;
   ansi_c -> langapi;
   langapi -> goto_programs;

jbmc/src/janalyzer/Makefile

@@ -34,11 +34,6 @@ CLEANFILES = janalyzer$(EXEEXT)
 
 all: janalyzer$(EXEEXT)
 
-ifneq ($(wildcard ../jsil/Makefile),)
-  OBJ += ../jsil/jsil$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JSIL
-endif
-
 ###############################################################################
 
 janalyzer$(EXEEXT): $(OBJ)

src/CMakeLists.txt

@@ -99,7 +99,6 @@ add_subdirectory(goto-checker)
 add_subdirectory(goto-programs)
 add_subdirectory(goto-symex)
 add_subdirectory(goto-inspect)
-add_subdirectory(jsil)
 add_subdirectory(json)
 add_subdirectory(json-symtab-language)
 add_subdirectory(langapi)

src/Makefile

@@ -17,7 +17,6 @@ DIRS = analyses \
        goto-programs \
        goto-symex \
        goto-synthesizer \
-       jsil \
        json \
        json-symtab-language \
        langapi \
@@ -82,7 +81,7 @@ crangler.dir: util.dir json.dir
 
 languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir \
-           jsil.dir json.dir json-symtab-language.dir statement-list.dir
+           json.dir json-symtab-language.dir statement-list.dir
 
 solvers.dir: util.dir
 

src/cbmc/CMakeLists.txt

@@ -29,7 +29,6 @@ target_link_libraries(cbmc-lib
 )
 
 add_if_library(cbmc-lib bv_refinement)
-add_if_library(cbmc-lib jsil)
 
 # Executable
 add_executable(cbmc cbmc_main.cpp)

src/cbmc/Makefile

@@ -60,11 +60,6 @@ ifneq ($(wildcard ../bv_refinement/Makefile),)
   CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
 endif
 
-ifneq ($(wildcard ../jsil/Makefile),)
-  OBJ += ../jsil/jsil$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JSIL
-endif
-
 ###############################################################################
 
 cbmc$(EXEEXT): $(OBJ)

src/cbmc/cbmc_languages.cpp

@@ -18,18 +18,10 @@ Author: Daniel Kroening, [email protected]
 #include <json-symtab-language/json_symtab_language.h>
 #include <statement-list/statement_list_language.h>
 
-#ifdef HAVE_JSIL
-#  include <jsil/jsil_language.h>
-#endif
-
 void cbmc_parse_optionst::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_statement_list_language);
   register_language(new_cpp_language);
   register_language(new_json_symtab_language);
-
-#ifdef HAVE_JSIL
-  register_language(new_jsil_language);
-#endif
 }