Factor out language_infot from languaget

src/analyses/goto_check.cpp

@@ -1275,7 +1275,8 @@ void goto_checkt::add_guarded_claim(
     goto_programt::targett t=new_code.add_instruction(type);
 
     std::string source_expr_string;
-    get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
+    get_language_from_mode(mode)->info.from_expr(
+      src_expr, source_expr_string, ns);
 
     t->guard.swap(new_expr);
     t->source_location=source_location;

src/ansi-c/Makefile

@@ -4,6 +4,7 @@ SRC = anonymous_member.cpp \
       ansi_c_entry_point.cpp \
       ansi_c_internal_additions.cpp \
       ansi_c_language.cpp \
+      ansi_c_language_info.cpp \
       ansi_c_lex.yy.cpp \
       ansi_c_parse_tree.cpp \
       ansi_c_parser.cpp \

src/ansi-c/ansi_c_language.cpp

@@ -21,15 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include "ansi_c_entry_point.h"
 #include "ansi_c_typecheck.h"
 #include "ansi_c_parser.h"
-#include "expr2c.h"
 #include "c_preprocess.h"
 #include "ansi_c_internal_additions.h"
-#include "type2name.h"
-
-std::set<std::string> ansi_c_languaget::extensions() const
-{
-  return { "c", "i" };
-}
 
 void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
 {
@@ -144,36 +137,9 @@ void ansi_c_languaget::show_parse(std::ostream &out)
   parse_tree.output(out);
 }
 
-std::unique_ptr<languaget> new_ansi_c_language()
-{
-  return util_make_unique<ansi_c_languaget>();
-}
-
-bool ansi_c_languaget::from_expr(
-  const exprt &expr,
-  std::string &code,
-  const namespacet &ns)
-{
-  code=expr2c(expr, ns);
-  return false;
-}
-
-bool ansi_c_languaget::from_type(
-  const typet &type,
-  std::string &code,
-  const namespacet &ns)
+std::unique_ptr<languaget> new_ansi_c_language(const language_infot &info)
 {
-  code=type2c(type, ns);
-  return false;
-}
-
-bool ansi_c_languaget::type_to_name(
-  const typet &type,
-  std::string &name,
-  const namespacet &ns)
-{
-  name=type2name(type, ns);
-  return false;
+  return std::unique_ptr<ansi_c_languaget>(new ansi_c_languaget(info));
 }
 
 bool ansi_c_languaget::to_expr(

src/ansi-c/ansi_c_language.h

@@ -39,44 +39,24 @@ class ansi_c_languaget:public languaget
 
   void show_parse(std::ostream &out) override;
 
+  explicit ansi_c_languaget(const language_infot &info) : languaget(info)
+  {
+  }
   ~ansi_c_languaget() override;
-  ansi_c_languaget() { }
-
-  bool from_expr(
-    const exprt &expr,
-    std::string &code,
-    const namespacet &ns) override;
-
-  bool from_type(
-    const typet &type,
-    std::string &code,
-    const namespacet &ns) override;
-
-  bool type_to_name(
-    const typet &type,
-    std::string &name,
-    const namespacet &ns) override;
 
   bool to_expr(
     const std::string &code,
     const std::string &module,
     exprt &expr,
     const namespacet &ns) override;
 
-  std::unique_ptr<languaget> new_language() override
-  { return util_make_unique<ansi_c_languaget>(); }
-
-  std::string id() const override { return "C"; }
-  std::string description() const override { return "ANSI-C 99"; }
-  std::set<std::string> extensions() const override;
-
   void modules_provided(std::set<std::string> &modules) override;
 
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
 };
 
-std::unique_ptr<languaget> new_ansi_c_language();
+std::unique_ptr<languaget> new_ansi_c_language(const language_infot &info);
 
 #endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_H

src/ansi-c/ansi_c_language_info.cpp

@@ -0,0 +1,52 @@
+/*******************************************************************\
+
+Module: C Language
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "ansi_c_language_info.h"
+
+#include "expr2c.h"
+#include "type2name.h"
+
+#include "ansi_c_language.h"
+
+std::set<std::string> ansi_c_language_infot::extensions() const
+{
+  return {"c", "i"};
+}
+
+bool ansi_c_language_infot::from_expr(
+  const exprt &expr,
+  std::string &code,
+  const namespacet &ns) const
+{
+  code = expr2c(expr, ns);
+  return false;
+}
+
+bool ansi_c_language_infot::from_type(
+  const typet &type,
+  std::string &code,
+  const namespacet &ns) const
+{
+  code = type2c(type, ns);
+  return false;
+}
+
+bool ansi_c_language_infot::type_to_name(
+  const typet &type,
+  std::string &name,
+  const namespacet &ns) const
+{
+  name = type2name(type, ns);
+  return false;
+}
+
+std::unique_ptr<language_infot> new_ansi_c_language_info()
+{
+  return std::unique_ptr<language_infot>(
+    new ansi_c_language_infot(new_ansi_c_language));
+}

src/ansi-c/ansi_c_language_info.h

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+Module: C Language
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H
+#define CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H
+
+#include <memory>
+
+#include <langapi/language_info.h>
+
+class ansi_c_language_infot : public language_infot
+{
+public:
+  explicit ansi_c_language_infot(language_factoryt _factory)
+    : language_infot(_factory)
+  {
+  }
+
+  irep_idt id() const override
+  {
+    return ID_C;
+  }
+
+  std::string description() const override
+  {
+    return "C";
+  }
+
+  std::set<std::string> extensions() const override;
+
+  bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
+    const override;
+
+  bool from_type(const typet &type, std::string &code, const namespacet &ns)
+    const override;
+
+  bool type_to_name(const typet &type, std::string &name, const namespacet &ns)
+    const override;
+};
+
+std::unique_ptr<language_infot> new_ansi_c_language_info();
+
+#endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H

src/ansi-c/cprover_library.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <sstream>
 
+#include <langapi/mode.h>
+
 #include <util/config.h>
 
 #include "ansi_c_language.h"
@@ -88,9 +90,9 @@ void add_library(
 
   std::istringstream in(src);
 
-  ansi_c_languaget ansi_c_language;
-  ansi_c_language.set_message_handler(message_handler);
-  ansi_c_language.parse(in, "");
+  auto ansi_c_language = get_language_from_mode(ID_C);
+  ansi_c_language->set_message_handler(message_handler);
+  ansi_c_language->parse(in, "");
 
-  ansi_c_language.typecheck(symbol_table, "<built-in-library>");
+  ansi_c_language->typecheck(symbol_table, "<built-in-library>");
 }

src/cbmc/CMakeLists.txt

@@ -16,6 +16,7 @@ target_link_libraries(cbmc-lib
     goto-instrument-lib
     goto-programs
     goto-symex
+    jsil
     json
     langapi
     linking
@@ -26,7 +27,6 @@ target_link_libraries(cbmc-lib
 )
 
 add_if_library(cbmc-lib bv_refinement)
-add_if_library(cbmc-lib jsil)
 
 # Executable
 add_executable(cbmc cbmc_main.cpp)

src/cbmc/Makefile

@@ -49,7 +49,9 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
       ../util/util$(LIBEXT) \
-      ../json/json$(LIBEXT)
+      ../json/json$(LIBEXT) \
+      ../jsil/jsil$(LIBEXT) \
+      # Empty last line
 
 INCLUDES= -I ..
 
@@ -67,11 +69,6 @@ ifneq ($(wildcard ../bv_refinement/Makefile),)
   CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
 endif
 
-ifneq ($(wildcard ../jsil/Makefile),)
-  OBJ += ../jsil/jsil$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JSIL
-endif
-
 ###############################################################################
 
 cbmc$(EXEEXT): $(OBJ)

src/cbmc/cbmc_languages.cpp

@@ -13,19 +13,13 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
-#include <ansi-c/ansi_c_language.h>
-#include <cpp/cpp_language.h>
-
-#ifdef HAVE_JSIL
-#include <jsil/jsil_language.h>
-#endif
+#include <ansi-c/ansi_c_language_info.h>
+#include <cpp/cpp_language_info.h>
+#include <jsil/jsil_language_info.h>
 
 void cbmc_parse_optionst::register_languages()
 {
-  register_language(new_ansi_c_language);
-  register_language(new_cpp_language);
-
-  #ifdef HAVE_JSIL
-  register_language(new_jsil_language);
-  #endif
+  register_language(new_ansi_c_language_info);
+  register_language(new_cpp_language_info);
+  register_language(new_jsil_language_info);
 }

src/clobber/clobber_parse_options.cpp

@@ -20,8 +20,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/options.h>
 #include <util/memory_info.h>
 
-#include <ansi-c/ansi_c_language.h>
-#include <cpp/cpp_language.h>
+#include <ansi-c/ansi_c_language_info.h>
+#include <cpp/cpp_language_info.h>
 
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/show_properties.h>
@@ -105,8 +105,8 @@ int clobber_parse_optionst::doit()
     return 0;
   }
 
-  register_language(new_ansi_c_language);
-  register_language(new_cpp_language);
+  register_language(new_ansi_c_language_info);
+  register_language(new_cpp_language_info);
 
   //
   // command line options

src/cpp/Makefile

@@ -11,6 +11,7 @@ SRC = cpp_constructor.cpp \
       cpp_internal_additions.cpp \
       cpp_is_pod.cpp \
       cpp_language.cpp \
+      cpp_language_info.cpp \
       cpp_name.cpp \
       cpp_namespace_spec.cpp \
       cpp_parse_tree.cpp \