[depends: #1339] Get goto model #1285
Conversation
kroening
force-pushed
the
get-goto-model
branch
2 times, most recently
from
ad06057 to
3b3ab2b
Compare
| @@ -25,7 +25,6 @@ void goto_convert( | |||
|
|
|||
| // confusing, will go away | |||
There was a problem hiding this comment.
Is this comment still true?
src/goto-programs/get_goto_model.cpp
Outdated
| << messaget::eom; | ||
|
|
||
| if(read_goto_binary(filename, tmp_model, message_handler)) | ||
| throw 0; |
There was a problem hiding this comment.
How is the actual error going to be conveyed?
src/goto-programs/get_goto_model.cpp
Outdated
| { | ||
| messaget message(message_handler); | ||
|
|
||
| languaget *language=get_language_from_filename(filename); |
There was a problem hiding this comment.
How is this not leaking memory?
|
|
||
| if(!infile) | ||
| { | ||
| message.error() << "failed to open input file `" |
There was a problem hiding this comment.
Shouldn't this also do
source_locationt location;
location.set_file(filename);
message.error().source_location=location;
as is done above?
There was a problem hiding this comment.
Contemplated it, but then we'd be sending out filenames that we know don't exist.
kroening
force-pushed
the
get-goto-model
branch
8 times, most recently
from
a757b6f to
e95796f
Compare
src/goto-programs/get_goto_model.cpp
Outdated
| goto_modelt goto_model; | ||
|
|
||
| // categorize | ||
| for(const auto & filename : cmdline.args) |
src/cbmc/cbmc_parse_options.cpp
Outdated
| cbmc_solverst cbmc_solvers( | ||
| options, | ||
| goto_model.symbol_table, | ||
| ui_message_handler); |
src/cbmc/cbmc_parse_options.cpp
Outdated
| bmct bmc( | ||
| options, | ||
| goto_model.symbol_table, | ||
| ui_message_handler, |
src/cbmc/cbmc_parse_options.cpp
Outdated
|
|
||
| // add the library | ||
| link_to_library(symbol_table, goto_functions, ui_message_handler); | ||
| link_to_library(goto_model, ui_message_handler); |
src/cbmc/cbmc_parse_options.cpp
Outdated
|
|
||
| if(cmdline.isset("drop-unused-functions")) | ||
| { | ||
| // Entry point will have been set before and function pointers removed | ||
| status() << "Removing unused functions" << eom; | ||
| remove_unused_functions(goto_functions, ui_message_handler); | ||
| remove_unused_functions(goto_model, ui_message_handler); |
kroening
force-pushed
the
get-goto-model
branch
4 times, most recently
from
faf2d0f to
33fe5fd
Compare
kroening
force-pushed
the
get-goto-model
branch
from
33fe5fd to
dd1ee91
Compare
|
The failing CI tests indicate that there is work left to be done. |
kroening
force-pushed
the
get-goto-model
branch
3 times, most recently
from
2866ca0 to
dd1ee91
Compare
|
#1339 prepares this. |
|
I am going to close this PR as it appears that work on it has been inactive for an extended period of time. This is not any judgement on how worthwhile this work is. This is part of an effort to reduce the number of open PRs which are not being actively worked on. If you still think it would be worthwhile to get this merged then the branch should be re-based on the latest version of develop and the PR re-opened. |
This is a new and simpler way to arrive at a goto program.