ebmc language interface implementation for Verilog #1454
Conversation
kroening
force-pushed
the
verilog-language-api
branch
2 times, most recently
from
231757d to
113faf9
Compare
kroening
force-pushed
the
verilog-language-api
branch
from
113faf9 to
0741ed9
Compare
| for(unsigned i = 0; i < cmdline.args.size(); i++) | ||
| { | ||
| if(parse(cmdline, cmdline.args[i], language_files, message_handler)) | ||
| return true; | ||
| } |
There was a problem hiding this comment.
Code modernisation: use ranged for
src/verilog/verilog_ebmc_language.h
Outdated
| verilog_ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler) | ||
| : ebmc_languaget(_cmdline, _message_handler) |
There was a problem hiding this comment.
Shouldn't this be const cmdlinet &?
There was a problem hiding this comment.
Yes, but will require change to base class; will do with separate PR.
| } | ||
|
|
||
| // produce the transition system, and return it | ||
| std::optional<transition_systemt> transition_system() override; |
There was a problem hiding this comment.
Should likely be marked nodiscard
There was a problem hiding this comment.
Likewise, will go into base class.
| return {}; | ||
| } | ||
|
|
||
| transition_systemt transition_system; |
There was a problem hiding this comment.
I'd move that declaration closer to where it will actually be used.
| std::string top_module; | ||
|
|
||
| if(cmdline.isset("module")) | ||
| top_module = cmdline.get_value("module"); | ||
| else if(cmdline.isset("top")) | ||
| top_module = cmdline.get_value("top"); |
There was a problem hiding this comment.
Is it ok if top_module remains unset?
There was a problem hiding this comment.
Yes, get_module handles that.
| // do -I | ||
| if(cmdline.isset('I')) | ||
| options.set_option("I", cmdline.get_values('I')); | ||
|
|
||
| options.set_option("force-systemverilog", cmdline.isset("systemverilog")); | ||
|
|
||
| // do -D | ||
| if(cmdline.isset('D')) | ||
| options.set_option("defines", cmdline.get_values('D')); | ||
|
|
||
| language->set_language_options(options, message_handler); |
There was a problem hiding this comment.
We have rather similar code in parse below, perhaps this should be factored out.
There was a problem hiding this comment.
Yes, will do separately.
kroening
force-pushed
the
verilog-language-api
branch
from
0741ed9 to
6fc2de8
Compare
It is unlikely that a language will want to modify the command line; hence, pass a const reference.
This adds an implementation of the ebmc_languaget interface for Verilog.
kroening
force-pushed
the
verilog-language-api
branch
from
6fc2de8 to
916ff1f
Compare
This adds an implementation of the
ebmc_languagetinterface for Verilog.