Skip to content

Commit 67be193

Browse files
tautschnigtautschnig
committed
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.
1 parent fd28cb2 commit 67be193

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

51 files changed

+5
-3603
lines changed

‎.gitignore

-4
Original file line numberDiff line numberDiff line change
@@ -91,10 +91,6 @@ src/ansi-c/ansi_c_y.tab.cpp
9191
src/ansi-c/ansi_c_y.tab.h
9292
src/assembler/assembler_lex.yy.cpp
9393
src/crangler/c_lex.yy.cpp
94-
src/jsil/jsil_lex.yy.cpp
95-
src/jsil/jsil_y.output
96-
src/jsil/jsil_y.tab.cpp
97-
src/jsil/jsil_y.tab.h
9894
src/json/json_lex.yy.cpp
9995
src/json/json_y.output
10096
src/json/json_y.tab.cpp

‎CMakeLists.txt

-1
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,6 @@ cprover_default_properties(
256256
goto-symex
257257
goto-synthesizer
258258
goto-synthesizer-lib
259-
jsil
260259
json
261260
json-symtab-language
262261
langapi

‎CODEOWNERS

-1
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,6 @@
5656
/src/goto-inspect/ @diffblue/diffblue-opensource
5757
/src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
5858
/src/goto-diff/ @tautschnig @peterschrammel
59-
/src/jsil/ @kroening @tautschnig
6059
/src/memory-analyzer/ @tautschnig @kroening
6160
/jbmc/src/jbmc/ @peterschrammel @TGWDB
6261
/jbmc/src/janalyzer/ @peterschrammel @TGWDB

‎doc/architectural/folder-walkthrough.md

+3-6
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ containing the code for a different part of the system.
3232
* C: \ref ansi-c
3333
* C++: \ref cpp
3434
* Java: \ref java_bytecode
35-
* JavaScript: \ref jsil
3635

3736
- Tools
3837

@@ -155,7 +154,6 @@ digraph directory_dependencies {
155154
ansi_c [label = "ansi-c", URL = "\ref ansi-c"];
156155
langapi [URL = "\ref langapi"];
157156
cpp [URL = "\ref cpp"];
158-
jsil [URL = "\ref jsil"];
159157
java_bytecode [URL = "\ref java_bytecode"];
160158
}
161159

@@ -174,15 +172,14 @@ digraph directory_dependencies {
174172
JBMC -> { CBMC, java_bytecode };
175173
jdiff -> { goto_diff, java_bytecode };
176174
janalyzer -> { goto_analyzer, java_bytecode };
177-
CBMC -> { goto_instrument, jsil };
175+
CBMC -> { goto_instrument };
178176
goto_diff -> { goto_instrument };
179-
goto_analyzer -> { analyses, jsil, cpp };
177+
goto_analyzer -> { analyses, cpp };
180178
goto_instrument -> { goto_symex, cpp };
181-
goto_cc -> { cpp, jsil };
179+
goto_cc -> { cpp };
182180
smt2_solver -> solvers;
183181

184182
java_bytecode -> { analyses, miniz };
185-
jsil -> linking;
186183
cpp -> ansi_c;
187184
ansi_c -> langapi;
188185
langapi -> goto_programs;

‎jbmc/src/janalyzer/Makefile

-5
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,6 @@ CLEANFILES = janalyzer$(EXEEXT)
3434

3535
all: janalyzer$(EXEEXT)
3636

37-
ifneq ($(wildcard ../jsil/Makefile),)
38-
OBJ += ../jsil/jsil$(LIBEXT)
39-
CP_CXXFLAGS += -DHAVE_JSIL
40-
endif
41-
4237
###############################################################################
4338

4439
janalyzer$(EXEEXT): $(OBJ)

‎src/CMakeLists.txt

-1
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,6 @@ add_subdirectory(goto-checker)
9999
add_subdirectory(goto-programs)
100100
add_subdirectory(goto-symex)
101101
add_subdirectory(goto-inspect)
102-
add_subdirectory(jsil)
103102
add_subdirectory(json)
104103
add_subdirectory(json-symtab-language)
105104
add_subdirectory(langapi)

‎src/Makefile

+1-2
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ DIRS = analyses \
1717
goto-programs \
1818
goto-symex \
1919
goto-synthesizer \
20-
jsil \
2120
json \
2221
json-symtab-language \
2322
langapi \
@@ -82,7 +81,7 @@ crangler.dir: util.dir json.dir
8281

8382
languages: util.dir langapi.dir \
8483
cpp.dir ansi-c.dir xmllang.dir assembler.dir \
85-
jsil.dir json.dir json-symtab-language.dir statement-list.dir
84+
json.dir json-symtab-language.dir statement-list.dir
8685

8786
solvers.dir: util.dir
8887

‎src/cbmc/CMakeLists.txt

-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ target_link_libraries(cbmc-lib
2929
)
3030

3131
add_if_library(cbmc-lib bv_refinement)
32-
add_if_library(cbmc-lib jsil)
3332

3433
# Executable
3534
add_executable(cbmc cbmc_main.cpp)

‎src/cbmc/Makefile

-5
Original file line numberDiff line numberDiff line change
@@ -60,11 +60,6 @@ ifneq ($(wildcard ../bv_refinement/Makefile),)
6060
CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
6161
endif
6262

63-
ifneq ($(wildcard ../jsil/Makefile),)
64-
OBJ += ../jsil/jsil$(LIBEXT)
65-
CP_CXXFLAGS += -DHAVE_JSIL
66-
endif
67-
6863
###############################################################################
6964

7065
cbmc$(EXEEXT): $(OBJ)

‎src/cbmc/cbmc_languages.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -18,18 +18,10 @@ Author: Daniel Kroening, [email protected]
1818
#include <json-symtab-language/json_symtab_language.h>
1919
#include <statement-list/statement_list_language.h>
2020

21-
#ifdef HAVE_JSIL
22-
# include <jsil/jsil_language.h>
23-
#endif
24-
2521
void cbmc_parse_optionst::register_languages()
2622
{
2723
register_language(new_ansi_c_language);
2824
register_language(new_statement_list_language);
2925
register_language(new_cpp_language);
3026
register_language(new_json_symtab_language);
31-
32-
#ifdef HAVE_JSIL
33-
register_language(new_jsil_language);
34-
#endif
3527
}

‎src/cbmc/module_dependencies.txt

-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ goto-checker
66
goto-instrument
77
goto-programs
88
goto-symex
9-
jsil
109
json
1110
json-symtab-language
1211
langapi # should go away

‎src/cprover/CMakeLists.txt

-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ target_link_libraries(cprover-lib
2929
)
3030

3131
add_if_library(cprover-lib bv_refinement)
32-
add_if_library(cprover-lib jsil)
3332

3433
# Executable
3534
add_executable(cprover cprover_main.cpp)

‎src/goto-analyzer/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,6 @@ target_link_libraries(goto-analyzer-lib
2222
util
2323
)
2424

25-
add_if_library(goto-analyzer-lib jsil)
26-
2725
# Executable
2826
add_executable(goto-analyzer goto_analyzer_main.cpp)
2927
target_link_libraries(goto-analyzer goto-analyzer-lib)

‎src/goto-analyzer/Makefile

-5
Original file line numberDiff line numberDiff line change
@@ -36,11 +36,6 @@ CLEANFILES = goto-analyzer$(EXEEXT)
3636

3737
all: goto-analyzer$(EXEEXT)
3838

39-
ifneq ($(wildcard ../jsil/Makefile),)
40-
OBJ += ../jsil/jsil$(LIBEXT)
41-
CP_CXXFLAGS += -DHAVE_JSIL
42-
endif
43-
4439
###############################################################################
4540

4641
goto-analyzer$(EXEEXT): $(OBJ)

‎src/goto-analyzer/goto_analyzer_languages.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -16,16 +16,8 @@ Author: Martin Brain, [email protected]
1616
#include <ansi-c/ansi_c_language.h>
1717
#include <cpp/cpp_language.h>
1818

19-
#ifdef HAVE_JSIL
20-
# include <jsil/jsil_language.h>
21-
#endif
22-
2319
void goto_analyzer_parse_optionst::register_languages()
2420
{
2521
register_language(new_ansi_c_language);
2622
register_language(new_cpp_language);
27-
28-
#ifdef HAVE_JSIL
29-
register_language(new_jsil_language);
30-
#endif
3123
}

‎src/goto-analyzer/module_dependencies.txt

-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ goto-checker
77
goto-programs
88
java_bytecode # will go away
99
langapi # should go away
10-
jsil
1110
json
1211
util

‎src/goto-cc/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,6 @@ target_link_libraries(goto-cc-lib
2020
langapi
2121
)
2222

23-
add_if_library(goto-cc-lib jsil)
24-
2523
# Executable
2624
add_executable(goto-cc goto_cc_main.cpp)
2725
target_link_libraries(goto-cc goto-cc-lib)

‎src/goto-cc/Makefile

-5
Original file line numberDiff line numberDiff line change
@@ -51,11 +51,6 @@ else
5151
all: goto-gcc$(EXEEXT)
5252
endif
5353

54-
ifneq ($(wildcard ../jsil/Makefile),)
55-
OBJ += ../jsil/jsil$(LIBEXT)
56-
CP_CXXFLAGS += -DHAVE_JSIL
57-
endif
58-
5954
###############################################################################
6055

6156
goto-gcc$(EXEEXT): goto-cc$(EXEEXT)

‎src/goto-cc/compile.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -141,7 +141,7 @@ static file_typet detect_file_type(
141141
if(
142142
ext == "c" || ext == "cc" || ext == "cp" || ext == "cpp" || ext == "CPP" ||
143143
ext == "c++" || ext == "C" || ext == "i" || ext == "ii" || ext == "class" ||
144-
ext == "jar" || ext == "jsil")
144+
ext == "jar")
145145
{
146146
return file_typet::SOURCE_FILE;
147147
}

‎src/goto-cc/goto_cc_languages.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -16,16 +16,8 @@ Author: CM Wintersteiger
1616
#include <ansi-c/ansi_c_language.h>
1717
#include <cpp/cpp_language.h>
1818

19-
#ifdef HAVE_JSIL
20-
# include <jsil/jsil_language.h>
21-
#endif
22-
2319
void goto_cc_modet::register_languages()
2420
{
2521
register_language(new_ansi_c_language);
2622
register_language(new_cpp_language);
27-
28-
#ifdef HAVE_JSIL
29-
register_language(new_jsil_language);
30-
#endif
3123
}

‎src/goto-cc/module_dependencies.txt

-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@ ansi-c
22
cpp
33
goto-cc
44
goto-programs
5-
jsil
65
json
76
langapi # should go away
87
linking

‎src/goto-diff/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@ target_link_libraries(goto-diff-lib
2323
solvers
2424
)
2525

26-
add_if_library(goto-diff-lib jsil)
27-
2826
# Executable
2927
add_executable(goto-diff goto_diff_main.cpp)
3028
target_link_libraries(goto-diff goto-diff-lib)

‎src/goto-programs/goto_convert_functions.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,6 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
4343
symbol_pair.second.type.id() == ID_code &&
4444
(symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
4545
symbol_pair.second.mode == ID_java ||
46-
symbol_pair.second.mode == "jsil" ||
4746
symbol_pair.second.mode == ID_statement_list))
4847
{
4948
symbol_list.push_back(symbol_pair.first);

‎src/jsil/CMakeLists.txt

-13
This file was deleted.

‎src/jsil/Makefile

-42
This file was deleted.

‎src/jsil/README.md

-6
This file was deleted.

‎src/jsil/expr2jsil.cpp

-35
This file was deleted.

‎src/jsil/expr2jsil.h

-24
This file was deleted.

0 commit comments

Comments
 (0)