Function to get a goto model from a C program for use in unit tests #5265
Conversation
danpoe
force-pushed
the
refactor/get-goto-model
branch
from
9d3adc0 to
5e0e30b
Compare
| optionst options; | ||
| cbmc_parse_optionst::set_default_options(options); |
There was a problem hiding this comment.
This doesn’t actually do anything though? set_default_options just sets default values on the options, which you then discard.
| const bool error = language.parse(in, ""); | ||
|
|
||
| if(error) | ||
| return {}; |
There was a problem hiding this comment.
I thinki it’d be better to just throw an exception rather than return optional, because presumably you’d expect for unit tests that their input programs do compile (ditto for all the other error cases)
|
|
||
| language_filet &language_file = language_files.add_file(""); | ||
|
|
||
| language_file.language = get_default_language(); |
There was a problem hiding this comment.
This function is called get_goto_model_from_c, so I think this should be something like get_language_from_mode(ID_C).
|
|
||
| cmdlinet cmdline; | ||
|
|
||
| config.main = std::string("main"); |
There was a problem hiding this comment.
Actually, I think this shouldn’t be called only once... because config is a global variable and could be messed with by other tests, ideally this would start with something like config = configt{}; so we can be sure we’re starting from a “clean” config and run every time (it’s not like this is going to cost us much test performance).
There was a problem hiding this comment.
Good point. I've now gotten rid of the initialize function altogether.
| } | ||
| } // namespace | ||
|
|
||
| optionalt<goto_modelt> get_goto_model_from_c(std::istream &in) |
There was a problem hiding this comment.
Not sure if it’s needed right now, but we’ll probably eventually want to set options for config and such in here as well (e.g. by passing in std::function<void(configt&)> which gets to set some options between resetting everything to default and parsing the C.
There was a problem hiding this comment.
I'll leave this for a future PR.
danpoe
force-pushed
the
refactor/get-goto-model
branch
2 times, most recently
from
99c113e to
1210f72
Compare
danpoe
force-pushed
the
refactor/get-goto-model
branch
3 times, most recently
from
e92d1a6 to
174f8f3
Compare
The function takes a C program (as a string or an input stream) and converts it to a goto model.
The function takes a C program (as a string or an input stream) and converts it
to a goto model.