Skip to content

Commit 98cac0e

Browse files
author
Daniel Kroening
committed
new interface for read_goto_binary()
1 parent d54d101 commit 98cac0e

File tree

3 files changed

+26
-2
lines changed

3 files changed

+26
-2
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -898,10 +898,13 @@ void goto_instrument_parse_optionst::get_goto_program()
898898
{
899899
status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
900900

901-
if(read_goto_binary(cmdline.args[0],
902-
goto_model, get_message_handler()))
901+
auto result = read_goto_binary(cmdline.args[0], get_message_handler());
902+
903+
if(!result.has_value())
903904
throw 0;
904905

906+
goto_model = std::move(result.value());
907+
905908
config.set(cmdline);
906909
}
907910

src/goto-programs/read_goto_binary.cpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,20 @@ bool read_goto_binary(
3636
filename, dest.symbol_table, dest.goto_functions, message_handler);
3737
}
3838

39+
optionalt<goto_modelt>
40+
read_goto_binary(const std::string &filename, message_handlert &message_handler)
41+
{
42+
goto_modelt dest;
43+
44+
if(read_goto_binary(
45+
filename, dest.symbol_table, dest.goto_functions, message_handler))
46+
{
47+
return {};
48+
}
49+
else
50+
return std::move(dest);
51+
}
52+
3953
bool read_goto_binary(
4054
const std::string &filename,
4155
symbol_tablet &symbol_table,

src/goto-programs/read_goto_binary.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,9 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <string>
1616

17+
#include <util/deprecate.h>
18+
#include <util/optional.h>
19+
1720
class goto_functionst;
1821
class goto_modelt;
1922
class message_handlert;
@@ -25,11 +28,15 @@ bool read_goto_binary(
2528
goto_functionst &,
2629
message_handlert &);
2730

31+
DEPRECATED("use two-parameter variant instead")
2832
bool read_goto_binary(
2933
const std::string &filename,
3034
goto_modelt &dest,
3135
message_handlert &);
3236

37+
optionalt<goto_modelt>
38+
read_goto_binary(const std::string &filename, message_handlert &);
39+
3340
bool is_goto_binary(const std::string &filename);
3441

3542
bool read_object_and_link(

0 commit comments

Comments
 (0)