Skip to content

Commit aac16d5

Browse files
author
Daniel Kroening
authored
Merge pull request #2159 from peterschrammel/clean-up-specc
Clean up references to unused frontends
2 parents d413dd8 + 8414886 commit aac16d5

15 files changed

+0
-157
lines changed

‎src/clobber/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,6 @@ target_link_libraries(clobber-lib
2525
)
2626

2727
add_if_library(clobber-lib bv_refinement)
28-
add_if_library(clobber-lib specc)
29-
add_if_library(clobber-lib php)
3028

3129
# Executable
3230
add_executable(clobber clobber_main.cpp)

‎src/clobber/Makefile

-10
Original file line numberDiff line numberDiff line change
@@ -31,16 +31,6 @@ CLEANFILES = clobber$(EXEEXT)
3131

3232
all: clobber$(EXEEXT)
3333

34-
ifneq ($(wildcard ../specc/Makefile),)
35-
OBJ += ../specc/specc$(LIBEXT)
36-
CP_CXXFLAGS += -DHAVE_SPECC
37-
endif
38-
39-
ifneq ($(wildcard ../php/Makefile),)
40-
OBJ += ../php/php$(LIBEXT)
41-
CP_CXXFLAGS += -DHAVE_PHP
42-
endif
43-
4434
###############################################################################
4535

4636
clobber$(EXEEXT): $(OBJ)

‎src/clobber/clobber_parse_options.cpp

-2
Original file line numberDiff line numberDiff line change
@@ -38,8 +38,6 @@ Author: Daniel Kroening, [email protected]
3838

3939
#include <cbmc/version.h>
4040

41-
// #include "clobber_instrumenter.h"
42-
4341
clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
4442
parse_options_baset(CLOBBER_OPTIONS, argc, argv),
4543
language_uit(cmdline, ui_message_handler),

‎src/goto-analyzer/CMakeLists.txt

-2
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@ target_link_libraries(goto-analyzer-lib
2323

2424
add_if_library(goto-analyzer-lib java_bytecode)
2525
add_if_library(goto-analyzer-lib jsil)
26-
add_if_library(goto-analyzer-lib specc)
27-
add_if_library(goto-analyzer-lib php)
2826

2927
# Executable
3028
add_executable(goto-analyzer goto_analyzer_main.cpp)

‎src/goto-cc/goto_cc_languages.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -17,17 +17,9 @@ Author: CM Wintersteiger
1717
#include <cpp/cpp_language.h>
1818
#include <jsil/jsil_language.h>
1919

20-
#ifdef HAVE_SPECC
21-
#include <specc/specc_language.h>
22-
#endif
23-
2420
void goto_cc_modet::register_languages()
2521
{
2622
register_language(new_ansi_c_language);
2723
register_language(new_cpp_language);
2824
register_language(new_jsil_language);
29-
30-
#ifdef HAVE_SPECC
31-
register_language(new_specc_language);
32-
#endif
3325
}

‎src/goto-diff/CMakeLists.txt

-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@ target_link_libraries(goto-diff-lib
2525

2626
add_if_library(goto-diff-lib java_bytecode)
2727
add_if_library(goto-diff-lib jsil)
28-
add_if_library(goto-diff-lib php)
2928

3029
# Executable
3130
add_executable(goto-diff goto_diff_main.cpp)

‎src/goto-diff/Makefile

-10
Original file line numberDiff line numberDiff line change
@@ -46,16 +46,6 @@ CLEANFILES = goto-diff$(EXEEXT)
4646

4747
all: goto-diff$(EXEEXT)
4848

49-
ifneq ($(wildcard ../specc/Makefile),)
50-
OBJ += ../specc/specc$(LIBEXT)
51-
CP_CXXFLAGS += -DHAVE_SPECC
52-
endif
53-
54-
ifneq ($(wildcard ../php/Makefile),)
55-
OBJ += ../php/php$(LIBEXT)
56-
CP_CXXFLAGS += -DHAVE_PHP
57-
endif
58-
5949
###############################################################################
6050

6151
goto-diff$(EXEEXT): $(OBJ)

‎src/goto-diff/goto_diff_languages.cpp

-9
Original file line numberDiff line numberDiff line change
@@ -16,20 +16,11 @@ Author: Daniel Kroening, [email protected]
1616
#include <ansi-c/ansi_c_language.h>
1717
#include <cpp/cpp_language.h>
1818

19-
#ifdef HAVE_SPECC
20-
#include <specc/specc_language.h>
21-
#endif
22-
2319
#include <java_bytecode/java_bytecode_language.h>
2420

2521
void goto_diff_languagest::register_languages()
2622
{
2723
register_language(new_ansi_c_language);
2824
register_language(new_cpp_language);
29-
30-
#ifdef HAVE_SPECC
31-
register_language(new_specc_language);
32-
#endif
33-
3425
register_language(new_java_bytecode_language);
3526
}

‎src/goto-programs/goto_convert.cpp

-84
Original file line numberDiff line numberDiff line change
@@ -506,12 +506,6 @@ void goto_convertt::convert(
506506
convert_non_deterministic_goto(code, dest);
507507
else if(statement==ID_ifthenelse)
508508
convert_ifthenelse(to_code_ifthenelse(code), dest, mode);
509-
else if(statement==ID_specc_notify)
510-
convert_specc_notify(code, dest);
511-
else if(statement==ID_specc_wait)
512-
convert_specc_wait(code, dest);
513-
else if(statement==ID_specc_par)
514-
convert_specc_par(code, dest);
515509
else if(statement==ID_start_thread)
516510
convert_start_thread(code, dest);
517511
else if(statement==ID_end_thread)
@@ -1499,84 +1493,6 @@ void goto_convertt::convert_non_deterministic_goto(
14991493
convert_goto(code, dest);
15001494
}
15011495

1502-
void goto_convertt::convert_specc_notify(
1503-
const codet &code,
1504-
goto_programt &dest)
1505-
{
1506-
#if 0
1507-
goto_programt::targett t=dest.add_instruction(EVENT);
1508-
1509-
forall_operands(it, code)
1510-
convert_specc_event(*it, t->events);
1511-
1512-
t->code.swap(code);
1513-
t->source_location=code.source_location();
1514-
#endif
1515-
1516-
copy(code, OTHER, dest);
1517-
}
1518-
1519-
void goto_convertt::convert_specc_event(
1520-
const exprt &op,
1521-
std::set<irep_idt> &events)
1522-
{
1523-
if(op.id()==ID_or || op.id()==ID_and)
1524-
{
1525-
forall_operands(it, op)
1526-
convert_specc_event(*it, events);
1527-
}
1528-
else if(op.id()==ID_specc_event)
1529-
{
1530-
irep_idt event=op.get(ID_identifier);
1531-
1532-
if(has_prefix(id2string(event), "specc::"))
1533-
event=std::string(id2string(event), 7, std::string::npos);
1534-
1535-
events.insert(event);
1536-
}
1537-
else
1538-
{
1539-
error().source_location=op.find_source_location();
1540-
error() << "convert_convert_event got " << op.id() << eom;
1541-
throw 0;
1542-
}
1543-
}
1544-
1545-
void goto_convertt::convert_specc_wait(
1546-
const codet &code,
1547-
goto_programt &dest)
1548-
{
1549-
#if 0
1550-
goto_programt::targett t=dest.add_instruction(WAIT);
1551-
1552-
if(code.operands().size()!=1)
1553-
{
1554-
error().source_location=code.find_source_location();
1555-
error() << "specc_wait expects one operand" << eom;
1556-
throw 0;
1557-
}
1558-
1559-
const exprt &op=code.op0();
1560-
1561-
if(op.id()=="or")
1562-
t->or_semantics=true;
1563-
1564-
convert_specc_event(op, t->events);
1565-
1566-
t->code.swap(code);
1567-
t->source_location=code.source_location();
1568-
#endif
1569-
1570-
copy(code, OTHER, dest);
1571-
}
1572-
1573-
void goto_convertt::convert_specc_par(
1574-
const codet &code,
1575-
goto_programt &dest)
1576-
{
1577-
copy(code, OTHER, dest);
1578-
}
1579-
15801496
void goto_convertt::convert_start_thread(
15811497
const codet &code,
15821498
goto_programt &dest)

‎src/goto-programs/goto_convert_class.h

-5
Original file line numberDiff line numberDiff line change
@@ -292,11 +292,6 @@ class goto_convertt:public messaget
292292
const code_function_callt &code,
293293
goto_programt &dest,
294294
const irep_idt &mode);
295-
void convert_specc_notify(const codet &code, goto_programt &dest);
296-
void convert_specc_wait(const codet &code, goto_programt &dest);
297-
void convert_specc_par(const codet &code, goto_programt &dest);
298-
void convert_specc_event(const exprt &op,
299-
std::set<irep_idt> &events);
300295
void convert_start_thread(const codet &code, goto_programt &dest);
301296
void convert_end_thread(const codet &code, goto_programt &dest);
302297
void convert_atomic_begin(const codet &code, goto_programt &dest);

‎src/pointer-analysis/value_set.cpp

-5
Original file line numberDiff line numberDiff line change
@@ -1541,11 +1541,6 @@ void value_sett::apply_code_rec(
15411541
assign(lhs, exprt(ID_invalid), ns, false, false);
15421542
}
15431543
}
1544-
else if(statement=="specc_notify" ||
1545-
statement=="specc_wait")
1546-
{
1547-
// ignore, does not change variables
1548-
}
15491544
else if(statement==ID_expression)
15501545
{
15511546
// can be ignored, we don't expect side effects here

‎src/pointer-analysis/value_set_fi.cpp

-5
Original file line numberDiff line numberDiff line change
@@ -1442,11 +1442,6 @@ void value_set_fit::apply_code(
14421442

14431443
assign(lhs, exprt(ID_invalid, lhs.type()), ns);
14441444
}
1445-
else if(statement==ID_specc_notify ||
1446-
statement==ID_specc_wait)
1447-
{
1448-
// ignore, does not change variables
1449-
}
14501445
else if(statement==ID_expression)
14511446
{
14521447
// can be ignored, we don't expect side effects here

‎src/pointer-analysis/value_set_fivr.cpp

-5
Original file line numberDiff line numberDiff line change
@@ -1597,11 +1597,6 @@ void value_set_fivrt::apply_code(
15971597

15981598
assign(lhs, exprt(ID_invalid, lhs.type()), ns);
15991599
}
1600-
else if(statement==ID_specc_notify ||
1601-
statement==ID_specc_wait)
1602-
{
1603-
// ignore, does not change variables
1604-
}
16051600
else if(statement==ID_expression)
16061601
{
16071602
// can be ignored, we don't expect side effects here

‎src/pointer-analysis/value_set_fivrns.cpp

-5
Original file line numberDiff line numberDiff line change
@@ -1255,11 +1255,6 @@ void value_set_fivrnst::apply_code(
12551255

12561256
assign(lhs, exprt(ID_invalid, lhs.type()), ns);
12571257
}
1258-
else if(statement==ID_specc_notify ||
1259-
statement==ID_specc_wait)
1260-
{
1261-
// ignore, does not change variables
1262-
}
12631258
else if(statement==ID_expression)
12641259
{
12651260
// can be ignored, we don't expect side effects here

‎src/util/irep_ids.def

-4
Original file line numberDiff line numberDiff line change
@@ -381,10 +381,6 @@ IREP_ID_ONE(atomic_begin)
381381
IREP_ID_ONE(atomic_end)
382382
IREP_ID_ONE(start_thread)
383383
IREP_ID_ONE(end_thread)
384-
IREP_ID_ONE(specc_notify)
385-
IREP_ID_ONE(specc_par)
386-
IREP_ID_ONE(specc_wait)
387-
IREP_ID_ONE(specc_event)
388384
IREP_ID_ONE(coverage_criterion)
389385
IREP_ID_ONE(initializer)
390386
IREP_ID_ONE(anonymous)

0 commit comments

Comments
 (0)