use SMV and Verilog langauge interfaces

Author: kroening

src/ebmc/build_transition_system.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <langapi/language.h>
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
+#include <smvlang/smv_ebmc_language.h>
 #include <trans-word-level/show_module_hierarchy.h>
 #include <trans-word-level/show_modules.h>
 
@@ -335,39 +336,76 @@ int show_symbol_table(
     cmdline, message_handler, dummy_transition_system);
 }
 
-std::optional<transition_systemt> ebmc_languagest::transition_system()
+static std::set<std::string> file_extensions(const cmdlinet::argst &args)
 {
-  if(cmdline.isset("preprocess"))
-  {
-    preprocess(cmdline, message_handler);
-    return {};
-  }
+  std::set<std::string> result;
 
-  if(cmdline.isset("show-parse"))
+  for(auto &arg : args)
   {
-    show_parse(cmdline, message_handler);
-    return {};
+    std::size_t ext_pos = arg.rfind('.');
+
+    if(ext_pos != std::string::npos)
+    {
+      auto ext = std::string(arg, ext_pos + 1, std::string::npos);
+      result.insert(ext);
+    }
   }
 
-  if(
-    cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-    cmdline.isset("json-modules"))
+  return result;
+}
+
+std::optional<transition_systemt> ebmc_languagest::transition_system()
+{
+  auto extensions = file_extensions(cmdline.args);
+  auto ext_used = [&extensions](const char *ext)
+  { return extensions.find(ext) != extensions.end(); };
+
+  bool have_smv = ext_used("smv");
+  bool have_verilog = ext_used("v") || ext_used("sv");
+
+  if(have_smv && have_verilog)
   {
-    show_modules(cmdline, message_handler);
-    return {};
+    throw ebmc_errort{} << "no support for mixed-language models";
   }
 
-  if(cmdline.isset("show-module-hierarchy"))
+  if(have_smv)
   {
-    show_module_hierarchy(cmdline, message_handler);
-    return {};
+    return smv_ebmc_languaget{cmdline, message_handler}.transition_system();
   }
-
-  if(cmdline.isset("show-symbol-table"))
+  else
   {
-    show_symbol_table(cmdline, message_handler);
-    return {};
+    if(cmdline.isset("preprocess"))
+    {
+      preprocess(cmdline, message_handler);
+      return {};
+    }
+
+    if(cmdline.isset("show-parse"))
+    {
+      show_parse(cmdline, message_handler);
+      return {};
+    }
+
+    if(
+      cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
+      cmdline.isset("json-modules"))
+    {
+      show_modules(cmdline, message_handler);
+      return {};
+    }
+
+    if(cmdline.isset("show-module-hierarchy"))
+    {
+      show_module_hierarchy(cmdline, message_handler);
+      return {};
+    }
+
+    if(cmdline.isset("show-symbol-table"))
+    {
+      show_symbol_table(cmdline, message_handler);
+      return {};
+    }
+
+    return get_transition_system(cmdline, message_handler);
   }
-
-  return get_transition_system(cmdline, message_handler);
 }