diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp index 899255db..e6fc9d95 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -94,10 +94,6 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler) return 1; } - // do -I - if(cmdline.isset('I')) - config.verilog.include_paths = cmdline.get_values('I'); - auto language = get_language_from_filename(filename); if(language == nullptr) @@ -110,9 +106,12 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler) } optionst options; + + // do -I + if(cmdline.isset('I')) + options.set_option("I", cmdline.get_values('I')); + options.set_option("force-systemverilog", cmdline.isset("systemverilog")); - options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions")); - options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets")); // do -D if(cmdline.isset('D')) @@ -162,6 +161,11 @@ static bool parse( languaget &language = *lf.language; optionst options; + + // do -I + if(cmdline.isset('I')) + options.set_option("I", cmdline.get_values('I')); + options.set_option("force-systemverilog", cmdline.isset("systemverilog")); options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions")); options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets")); @@ -242,10 +246,6 @@ int get_transition_system( { messaget message(message_handler); - // do -I - if(cmdline.isset('I')) - config.verilog.include_paths = cmdline.get_values('I'); - if(cmdline.isset("preprocess")) return preprocess(cmdline, message_handler); diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp index fc6b277c..cde151f2 100644 --- a/src/verilog/verilog_language.cpp +++ b/src/verilog/verilog_language.cpp @@ -36,6 +36,7 @@ void verilog_languaget::set_language_options( { force_systemverilog = options.get_bool_option("force-systemverilog"); vl2smv_extensions = options.get_bool_option("vl2smv-extensions"); + include_paths = options.get_list_option("I"); initial_defines = options.get_list_option("defines"); warn_implicit_nets = options.get_bool_option("warn-implicit-nets"); } @@ -107,7 +108,7 @@ bool verilog_languaget::preprocess( message_handlert &message_handler) { verilog_preprocessort preprocessor( - instream, outstream, message_handler, path, initial_defines); + instream, outstream, message_handler, path, include_paths, initial_defines); try { preprocessor.preprocessor(); } catch(int e) { return true; } diff --git a/src/verilog/verilog_language.h b/src/verilog/verilog_language.h index 0f566e91..a590d498 100644 --- a/src/verilog/verilog_language.h +++ b/src/verilog/verilog_language.h @@ -94,6 +94,7 @@ class verilog_languaget:public languaget bool force_systemverilog = false; bool vl2smv_extensions = false; bool warn_implicit_nets = false; + std::list include_paths; std::list initial_defines; verilog_parse_treet parse_tree; }; diff --git a/src/verilog/verilog_preprocessor.cpp b/src/verilog/verilog_preprocessor.cpp index 11d9558a..2cd68e03 100644 --- a/src/verilog/verilog_preprocessor.cpp +++ b/src/verilog/verilog_preprocessor.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "verilog_preprocessor.h" -#include #include #include "expr2verilog.h" @@ -136,7 +135,7 @@ std::filesystem::path verilog_preprocessort::find_include_file( } // Then try include paths in given order. - for(const auto &include_path : config.verilog.include_paths) + for(const auto &include_path : include_paths) { auto full_name = std::filesystem::path{include_path}.append(given_filename); if(std::filesystem::directory_entry(full_name).exists()) diff --git a/src/verilog/verilog_preprocessor.h b/src/verilog/verilog_preprocessor.h index 53616c73..4e208854 100644 --- a/src/verilog/verilog_preprocessor.h +++ b/src/verilog/verilog_preprocessor.h @@ -22,8 +22,10 @@ class verilog_preprocessort:public preprocessort std::ostream &_out, message_handlert &_message_handler, const std::string &_filename, + const std::list &_include_paths, const std::list &_initial_defines) : preprocessort(_in, _out, _message_handler, _filename), + include_paths(_include_paths), initial_defines(_initial_defines) { condition=true; @@ -33,6 +35,7 @@ class verilog_preprocessort:public preprocessort protected: // from the command line + const std::list &include_paths; const std::list &initial_defines; using tokent = verilog_preprocessor_token_sourcet::tokent; diff --git a/src/vlindex/verilog_indexer.cpp b/src/vlindex/verilog_indexer.cpp index fc5c45ef..9ac67b9c 100644 --- a/src/vlindex/verilog_indexer.cpp +++ b/src/vlindex/verilog_indexer.cpp @@ -92,7 +92,7 @@ std::string verilog_indexert::preprocess(const std::string &file_name) console_message_handlert message_handler; verilog_preprocessort preprocessor( - in_stream, preprocessed, message_handler, file_name, {}); + in_stream, preprocessed, message_handler, file_name, {}, {}); try {