Skip to content

Commit 3185028

Browse files
author
thk123
committed
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.
1 parent 0047733 commit 3185028

File tree

3 files changed

+71
-0
lines changed

3 files changed

+71
-0
lines changed

unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
# Source files for test utilities
44
SRC = src/expr/require_expr.cpp \
5+
src/ansi-c/c_to_expr.cpp \
56
# Empty last line
67

78
# Test source files

unit/src/ansi-c/c_to_expr.cpp

+35
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test utilities
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Utility for converting strings in to exprt, throwing a CATCH exception
11+
/// if this fails in any way.
12+
///
13+
#include "c_to_expr.h"
14+
15+
#include <catch.hpp>
16+
17+
c_to_exprt::c_to_exprt():
18+
message_handler(
19+
std::unique_ptr<message_handlert>(new ui_message_handlert()))
20+
{
21+
language.set_message_handler(*message_handler);
22+
}
23+
24+
/// Take an input string that should be a valid C rhs expression
25+
/// \param input_string: The string to convert
26+
/// \param ns: The global namespace
27+
/// \return: A constructed expr representing the string
28+
exprt c_to_exprt::operator()(
29+
const std::string &input_string, const namespacet &ns)
30+
{
31+
exprt expr;
32+
bool result=language.to_expr(input_string, "", expr, ns);
33+
REQUIRE(!result);
34+
return expr;
35+
}

unit/src/ansi-c/c_to_expr.h

+35
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test utilities
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Utility for converting strings in to exprt, throwing a CATCH exception
11+
/// if this fails in any way.
12+
13+
#ifndef CPROVER_SRC_ANSI_C_C_TO_EXPR_H
14+
#define CPROVER_SRC_ANSI_C_C_TO_EXPR_H
15+
16+
#include <memory>
17+
18+
#include <util/expr.h>
19+
#include <util/message.h>
20+
#include <util/ui_message.h>
21+
#include <util/namespace.h>
22+
#include <ansi-c/ansi_c_language.h>
23+
24+
class c_to_exprt
25+
{
26+
public:
27+
c_to_exprt();
28+
exprt operator()(const std::string &input_string, const namespacet &ns);
29+
30+
private:
31+
std::unique_ptr<message_handlert> message_handler;
32+
ansi_c_languaget language;
33+
};
34+
35+
#endif // CPROVER_SRC_ANSI_C_C_TO_EXPR_H

0 commit comments

Comments
 (0)