diff --git a/src/clobber/CMakeLists.txt b/src/clobber/CMakeLists.txt index 2e4803df7e2..a67792c0e87 100644 --- a/src/clobber/CMakeLists.txt +++ b/src/clobber/CMakeLists.txt @@ -25,8 +25,6 @@ target_link_libraries(clobber-lib ) add_if_library(clobber-lib bv_refinement) -add_if_library(clobber-lib specc) -add_if_library(clobber-lib php) # Executable add_executable(clobber clobber_main.cpp) diff --git a/src/clobber/Makefile b/src/clobber/Makefile index d9b9f09de1c..aa195f87233 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -31,16 +31,6 @@ CLEANFILES = clobber$(EXEEXT) all: clobber$(EXEEXT) -ifneq ($(wildcard ../specc/Makefile),) - OBJ += ../specc/specc$(LIBEXT) - CP_CXXFLAGS += -DHAVE_SPECC -endif - -ifneq ($(wildcard ../php/Makefile),) - OBJ += ../php/php$(LIBEXT) - CP_CXXFLAGS += -DHAVE_PHP -endif - ############################################################################### clobber$(EXEEXT): $(OBJ) diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 05d9c3f75f0..42693cb16cb 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -38,8 +38,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -// #include "clobber_instrumenter.h" - clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv): parse_options_baset(CLOBBER_OPTIONS, argc, argv), language_uit(cmdline, ui_message_handler), diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt index 175b1f99ab6..354069d913a 100644 --- a/src/goto-analyzer/CMakeLists.txt +++ b/src/goto-analyzer/CMakeLists.txt @@ -23,8 +23,6 @@ target_link_libraries(goto-analyzer-lib add_if_library(goto-analyzer-lib java_bytecode) add_if_library(goto-analyzer-lib jsil) -add_if_library(goto-analyzer-lib specc) -add_if_library(goto-analyzer-lib php) # Executable add_executable(goto-analyzer goto_analyzer_main.cpp) diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-cc/goto_cc_languages.cpp index c3246b5b8f1..3e0b56aeed4 100644 --- a/src/goto-cc/goto_cc_languages.cpp +++ b/src/goto-cc/goto_cc_languages.cpp @@ -17,17 +17,9 @@ Author: CM Wintersteiger #include #include -#ifdef HAVE_SPECC -#include -#endif - void goto_cc_modet::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); register_language(new_jsil_language); - - #ifdef HAVE_SPECC - register_language(new_specc_language); - #endif } diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt index 2839634244c..ebaec4b3b99 100644 --- a/src/goto-diff/CMakeLists.txt +++ b/src/goto-diff/CMakeLists.txt @@ -25,7 +25,6 @@ target_link_libraries(goto-diff-lib add_if_library(goto-diff-lib java_bytecode) add_if_library(goto-diff-lib jsil) -add_if_library(goto-diff-lib php) # Executable add_executable(goto-diff goto_diff_main.cpp) diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 22304c2a5b7..9325b323c64 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -46,16 +46,6 @@ CLEANFILES = goto-diff$(EXEEXT) all: goto-diff$(EXEEXT) -ifneq ($(wildcard ../specc/Makefile),) - OBJ += ../specc/specc$(LIBEXT) - CP_CXXFLAGS += -DHAVE_SPECC -endif - -ifneq ($(wildcard ../php/Makefile),) - OBJ += ../php/php$(LIBEXT) - CP_CXXFLAGS += -DHAVE_PHP -endif - ############################################################################### goto-diff$(EXEEXT): $(OBJ) diff --git a/src/goto-diff/goto_diff_languages.cpp b/src/goto-diff/goto_diff_languages.cpp index c930f20e77b..814ef326488 100644 --- a/src/goto-diff/goto_diff_languages.cpp +++ b/src/goto-diff/goto_diff_languages.cpp @@ -16,20 +16,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#ifdef HAVE_SPECC -#include -#endif - #include void goto_diff_languagest::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); - - #ifdef HAVE_SPECC - register_language(new_specc_language); - #endif - register_language(new_java_bytecode_language); } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 236dd782db6..7ab9a4eb42d 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -506,12 +506,6 @@ void goto_convertt::convert( convert_non_deterministic_goto(code, dest); else if(statement==ID_ifthenelse) convert_ifthenelse(to_code_ifthenelse(code), dest, mode); - else if(statement==ID_specc_notify) - convert_specc_notify(code, dest); - else if(statement==ID_specc_wait) - convert_specc_wait(code, dest); - else if(statement==ID_specc_par) - convert_specc_par(code, dest); else if(statement==ID_start_thread) convert_start_thread(code, dest); else if(statement==ID_end_thread) @@ -1499,84 +1493,6 @@ void goto_convertt::convert_non_deterministic_goto( convert_goto(code, dest); } -void goto_convertt::convert_specc_notify( - const codet &code, - goto_programt &dest) -{ - #if 0 - goto_programt::targett t=dest.add_instruction(EVENT); - - forall_operands(it, code) - convert_specc_event(*it, t->events); - - t->code.swap(code); - t->source_location=code.source_location(); - #endif - - copy(code, OTHER, dest); -} - -void goto_convertt::convert_specc_event( - const exprt &op, - std::set &events) -{ - if(op.id()==ID_or || op.id()==ID_and) - { - forall_operands(it, op) - convert_specc_event(*it, events); - } - else if(op.id()==ID_specc_event) - { - irep_idt event=op.get(ID_identifier); - - if(has_prefix(id2string(event), "specc::")) - event=std::string(id2string(event), 7, std::string::npos); - - events.insert(event); - } - else - { - error().source_location=op.find_source_location(); - error() << "convert_convert_event got " << op.id() << eom; - throw 0; - } -} - -void goto_convertt::convert_specc_wait( - const codet &code, - goto_programt &dest) -{ - #if 0 - goto_programt::targett t=dest.add_instruction(WAIT); - - if(code.operands().size()!=1) - { - error().source_location=code.find_source_location(); - error() << "specc_wait expects one operand" << eom; - throw 0; - } - - const exprt &op=code.op0(); - - if(op.id()=="or") - t->or_semantics=true; - - convert_specc_event(op, t->events); - - t->code.swap(code); - t->source_location=code.source_location(); - #endif - - copy(code, OTHER, dest); -} - -void goto_convertt::convert_specc_par( - const codet &code, - goto_programt &dest) -{ - copy(code, OTHER, dest); -} - void goto_convertt::convert_start_thread( const codet &code, goto_programt &dest) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index b362566893e..8e4ad995a4e 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -292,11 +292,6 @@ class goto_convertt:public messaget const code_function_callt &code, goto_programt &dest, const irep_idt &mode); - void convert_specc_notify(const codet &code, goto_programt &dest); - void convert_specc_wait(const codet &code, goto_programt &dest); - void convert_specc_par(const codet &code, goto_programt &dest); - void convert_specc_event(const exprt &op, - std::set &events); void convert_start_thread(const codet &code, goto_programt &dest); void convert_end_thread(const codet &code, goto_programt &dest); void convert_atomic_begin(const codet &code, goto_programt &dest); diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 7cd08339d7a..aea661e5b62 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1541,11 +1541,6 @@ void value_sett::apply_code_rec( assign(lhs, exprt(ID_invalid), ns, false, false); } } - else if(statement=="specc_notify" || - statement=="specc_wait") - { - // ignore, does not change variables - } else if(statement==ID_expression) { // can be ignored, we don't expect side effects here diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index d72e7fdda19..3b88a081984 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -1442,11 +1442,6 @@ void value_set_fit::apply_code( assign(lhs, exprt(ID_invalid, lhs.type()), ns); } - else if(statement==ID_specc_notify || - statement==ID_specc_wait) - { - // ignore, does not change variables - } else if(statement==ID_expression) { // can be ignored, we don't expect side effects here diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 080100829a8..a04f5ae8b3a 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -1597,11 +1597,6 @@ void value_set_fivrt::apply_code( assign(lhs, exprt(ID_invalid, lhs.type()), ns); } - else if(statement==ID_specc_notify || - statement==ID_specc_wait) - { - // ignore, does not change variables - } else if(statement==ID_expression) { // can be ignored, we don't expect side effects here diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index e031f6b0d42..0c3a48fb088 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -1255,11 +1255,6 @@ void value_set_fivrnst::apply_code( assign(lhs, exprt(ID_invalid, lhs.type()), ns); } - else if(statement==ID_specc_notify || - statement==ID_specc_wait) - { - // ignore, does not change variables - } else if(statement==ID_expression) { // can be ignored, we don't expect side effects here diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index d9bebfa5b22..b0fac1ce788 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -381,10 +381,6 @@ IREP_ID_ONE(atomic_begin) IREP_ID_ONE(atomic_end) IREP_ID_ONE(start_thread) IREP_ID_ONE(end_thread) -IREP_ID_ONE(specc_notify) -IREP_ID_ONE(specc_par) -IREP_ID_ONE(specc_wait) -IREP_ID_ONE(specc_event) IREP_ID_ONE(coverage_criterion) IREP_ID_ONE(initializer) IREP_ID_ONE(anonymous)