File tree 1 file changed +21
-0
lines changed
1 file changed +21
-0
lines changed Original file line number Diff line number Diff line change 8
8
9
9
#include < catch.hpp>
10
10
11
+ #include < java_bytecode/java_types.h>
11
12
#include < util/arith_tools.h>
12
13
#include < util/c_types.h>
13
14
#include < util/config.h>
@@ -59,3 +60,23 @@ TEST_CASE("Simplify const pointer offset")
59
60
REQUIRE (!to_integer (simp, offset_value));
60
61
REQUIRE (offset_value==1234 );
61
62
}
63
+
64
+ TEST_CASE (" Simplify Java boolean -> int -> boolean casts" )
65
+ {
66
+ config.set_arch (" none" );
67
+
68
+ const exprt simplified=simplify_expr (
69
+ typecast_exprt (
70
+ typecast_exprt (
71
+ symbol_exprt (
72
+ " foo" ,
73
+ java_boolean_type ()),
74
+ java_int_type ()),
75
+ java_boolean_type ()),
76
+ namespacet (symbol_tablet ()));
77
+
78
+ REQUIRE (simplified.id ()==ID_symbol);
79
+ REQUIRE (simplified.type ()==java_boolean_type ());
80
+ const auto &symbol=to_symbol_expr (simplified);
81
+ REQUIRE (symbol.get_identifier ()==" foo" );
82
+ }
You can’t perform that action at this time.
0 commit comments