File tree Expand file tree Collapse file tree 3 files changed +42
-0
lines changed
jbmc/unit/java_bytecode/java_bytecode_convert_method Expand file tree Collapse file tree 3 files changed +42
-0
lines changed Original file line number Diff line number Diff line change
1
+ public class ClassWithVarArgsMethod {
2
+ public int varArgsFunc (int ... args ) {
3
+ return 0 ;
4
+ }
5
+ public int nonVarArgsFunc (int [] args ) {
6
+ return 0 ;
7
+ }
8
+ }
Original file line number Diff line number Diff line change @@ -141,3 +141,37 @@ SCENARIO(
141
141
}
142
142
}
143
143
}
144
+
145
+ SCENARIO (
146
+ " java_bytecode_convert_varargs_method" ,
147
+ " [core][java_bytecode][java_bytecode_convert_method]" )
148
+ {
149
+ GIVEN (" A class with varargs and non-varargs methods" )
150
+ {
151
+ const symbol_tablet symbol_table = load_java_class (
152
+ " ClassWithVarArgsMethod" , " ./java_bytecode/java_bytecode_convert_method" );
153
+
154
+ WHEN (" When parsing a method with a variable number of arguments" )
155
+ {
156
+ const symbolt method_symbol = symbol_table.lookup_ref (
157
+ " java::ClassWithVarArgsMethod.varArgsFunc:([I)I" );
158
+ const java_method_typet &method_type =
159
+ require_type::require_java_method (method_symbol.type );
160
+ THEN (" The method should be marked as varargs" )
161
+ {
162
+ REQUIRE (method_type.get_is_varargs ());
163
+ }
164
+ }
165
+ WHEN (" When parsing a method with constant number of arguments" )
166
+ {
167
+ const symbolt method_symbol = symbol_table.lookup_ref (
168
+ " java::ClassWithVarArgsMethod.nonVarArgsFunc:([I)I" );
169
+ const java_method_typet &method_type =
170
+ require_type::require_java_method (method_symbol.type );
171
+ THEN (" The method should not be marked as varargs" )
172
+ {
173
+ REQUIRE_FALSE (method_type.get_is_varargs ());
174
+ }
175
+ }
176
+ }
177
+ }
You can’t perform that action at this time.
0 commit comments