forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Added utility class to convert strings into expressions
In turns the error return state into a CATCH exception so the test will fail without cluttering tests with checks on the flag when it is just setup code for the actual test.
- Loading branch information
thk123
committed
Jul 18, 2017
1 parent
0047733
commit 3185028
Showing
3 changed files
with
71 additions
and
0 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
/*******************************************************************\ | ||
Module: Unit test utilities | ||
Author: DiffBlue Limited. All rights reserved. | ||
\*******************************************************************/ | ||
|
||
/// \file | ||
/// Utility for converting strings in to exprt, throwing a CATCH exception | ||
/// if this fails in any way. | ||
/// | ||
#include "c_to_expr.h" | ||
|
||
#include <catch.hpp> | ||
|
||
c_to_exprt::c_to_exprt(): | ||
message_handler( | ||
std::unique_ptr<message_handlert>(new ui_message_handlert())) | ||
{ | ||
language.set_message_handler(*message_handler); | ||
} | ||
|
||
/// Take an input string that should be a valid C rhs expression | ||
/// \param input_string: The string to convert | ||
/// \param ns: The global namespace | ||
/// \return: A constructed expr representing the string | ||
exprt c_to_exprt::operator()( | ||
const std::string &input_string, const namespacet &ns) | ||
{ | ||
exprt expr; | ||
bool result=language.to_expr(input_string, "", expr, ns); | ||
REQUIRE(!result); | ||
return expr; | ||
} |
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 |
---|---|---|
@@ -0,0 +1,35 @@ | ||
/*******************************************************************\ | ||
Module: Unit test utilities | ||
Author: DiffBlue Limited. All rights reserved. | ||
\*******************************************************************/ | ||
|
||
/// \file | ||
/// Utility for converting strings in to exprt, throwing a CATCH exception | ||
/// if this fails in any way. | ||
|
||
#ifndef CPROVER_SRC_ANSI_C_C_TO_EXPR_H | ||
#define CPROVER_SRC_ANSI_C_C_TO_EXPR_H | ||
|
||
#include <memory> | ||
|
||
#include <util/expr.h> | ||
#include <util/message.h> | ||
#include <util/ui_message.h> | ||
#include <util/namespace.h> | ||
#include <ansi-c/ansi_c_language.h> | ||
|
||
class c_to_exprt | ||
{ | ||
public: | ||
c_to_exprt(); | ||
exprt operator()(const std::string &input_string, const namespacet &ns); | ||
|
||
private: | ||
std::unique_ptr<message_handlert> message_handler; | ||
ansi_c_languaget language; | ||
}; | ||
|
||
#endif // CPROVER_SRC_ANSI_C_C_TO_EXPR_H |