Skip to content

Commit 4455dee

Browse files
authored
Merge pull request #3213 from diffblue/static_show_domain_return
static_show_domain doesn't determine SAFE/UNSAFE
2 parents 0bfe213 + 2d1c730 commit 4455dee

File tree

4 files changed

+8
-11
lines changed

4 files changed

+8
-11
lines changed

jbmc/src/janalyzer/janalyzer_parse_options.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -588,8 +588,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
588588
bool result = true;
589589
if(options.get_bool_option("show"))
590590
{
591-
result = static_show_domain(
592-
goto_model, *analyzer, options, out);
591+
static_show_domain(goto_model, *analyzer, options, out);
592+
return CPROVER_EXIT_SUCCESS;
593593
}
594594
else if(options.get_bool_option("verify"))
595595
{

src/goto-analyzer/goto_analyzer_parse_options.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -621,13 +621,13 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
621621

622622
// Perform the task
623623
status() << "Performing task" << eom;
624+
624625
bool result = true;
626+
625627
if(options.get_bool_option("show"))
626628
{
627-
result = static_show_domain(goto_model,
628-
*analyzer,
629-
options,
630-
out);
629+
static_show_domain(goto_model, *analyzer, options, out);
630+
return CPROVER_EXIT_SUCCESS;
631631
}
632632
else if(options.get_bool_option("verify"))
633633
{

src/goto-analyzer/static_show_domain.cpp

+1-4
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,7 @@ Author: Martin Brain, [email protected]
1717
/// \param ai: the abstract interpreter after it has been run to fix point
1818
/// \param options: the parsed user options
1919
/// \param out: output stream for the printing
20-
/// \return: false on success with the domain printed to out
21-
bool static_show_domain(
20+
void static_show_domain(
2221
const goto_modelt &goto_model,
2322
const ai_baset &ai,
2423
const optionst &options,
@@ -48,6 +47,4 @@ bool static_show_domain(
4847
// 'text' or console output
4948
ai.output(goto_model, out);
5049
}
51-
52-
return false;
5350
}

src/goto-analyzer/static_show_domain.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ class goto_modelt;
1616
class message_handlert;
1717
class optionst;
1818

19-
bool static_show_domain(
19+
void static_show_domain(
2020
const goto_modelt &,
2121
const ai_baset &,
2222
const optionst &,

0 commit comments

Comments
 (0)