Remove SpecC support

Author: peterschrammel

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)