forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Use global
null_message_handlert
instead of duplicates.
- Loading branch information
1 parent
dab421c
commit 8e20ac6
Showing
6 changed files
with
30 additions
and
30 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -7,6 +7,7 @@ Author: Chris Smowton, [email protected] | |
\*******************************************************************/ | ||
|
||
#include <testing-utils/catch.hpp> | ||
#include <testing-utils/message.h> | ||
|
||
#include <goto-programs/goto_inline.h> | ||
#include <goto-programs/initialize_goto_model.h> | ||
|
@@ -170,7 +171,6 @@ SCENARIO("test_value_set_analysis", | |
{ | ||
config.set_arch("none"); | ||
config.main = ""; | ||
null_message_handlert null_output; | ||
cmdlinet command_line; | ||
|
||
// This classpath is the default, but the config object | ||
|
@@ -181,8 +181,8 @@ SCENARIO("test_value_set_analysis", | |
|
||
register_language(new_java_bytecode_language); | ||
|
||
goto_modelt goto_model= | ||
initialize_goto_model(command_line, null_output); | ||
goto_modelt goto_model = | ||
initialize_goto_model(command_line, null_message_handler); | ||
|
||
null_message_handlert message_handler; | ||
remove_java_new(goto_model, message_handler); | ||
|
@@ -191,7 +191,7 @@ SCENARIO("test_value_set_analysis", | |
|
||
// Fully inline the test program, to avoid VSA conflating | ||
// constructor callsites confusing the results we're trying to check: | ||
goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_output); | ||
goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_message_handler); | ||
|
||
const goto_programt &test_function= | ||
goto_model.goto_functions.function_map.at(TEST_PREFIX "test:()V").body; | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters