Clean up references to unused frontends

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)

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)

src/clobber/clobber_parse_options.cpp

@@ -38,8 +38,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <cbmc/version.h>
 
-// #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),

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)

src/goto-cc/goto_cc_languages.cpp

@@ -17,17 +17,9 @@ Author: CM Wintersteiger
 #include <cpp/cpp_language.h>
 #include <jsil/jsil_language.h>
 
-#ifdef HAVE_SPECC
-#include <specc/specc_language.h>
-#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
 }

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)

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)

src/goto-diff/goto_diff_languages.cpp

@@ -16,20 +16,11 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 
-#ifdef HAVE_SPECC
-#include <specc/specc_language.h>
-#endif
-
 #include <java_bytecode/java_bytecode_language.h>
 
 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);
 }

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<irep_idt> &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)

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<irep_idt> &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);

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

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

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

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

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)