Skip to content

Commit 06127f0

Browse files
Add tag for java_method_type
1 parent 668236c commit 06127f0

File tree

2 files changed

+28
-1
lines changed

2 files changed

+28
-1
lines changed

jbmc/src/java_bytecode/java_types.h

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -245,10 +245,36 @@ inline bool can_cast_type<java_class_typet>(const typet &type)
245245
class java_method_typet : public code_typet
246246
{
247247
public:
248-
using code_typet::code_typet;
249248
using code_typet::parameterst;
250249
using code_typet::parametert;
251250

251+
/// Constructs a new code type, i.e. function type
252+
/// \param _parameters: the vector of function parameters
253+
/// \param _return_type: the return type
254+
java_method_typet(parameterst &&_parameters, typet &&_return_type)
255+
{
256+
set(ID_C_java_method_type, true);
257+
parameters().swap(_parameters);
258+
return_type().swap(_return_type);
259+
}
260+
261+
/// Constructs a new code type, i.e. function type
262+
/// \param _parameters: the vector of function parameters
263+
/// \param _return_type: the return type
264+
java_method_typet(parameterst &&_parameters, const typet &_return_type)
265+
{
266+
set(ID_C_java_method_type, true);
267+
parameters().swap(_parameters);
268+
return_type() = _return_type;
269+
}
270+
271+
/// \deprecated
272+
DEPRECATED("Use the two argument constructor instead")
273+
java_method_typet()
274+
{
275+
set(ID_C_java_method_type, true);
276+
}
277+
252278
const std::vector<irep_idt> throws_exceptions() const
253279
{
254280
std::vector<irep_idt> exceptions;

src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -695,6 +695,7 @@ IREP_ID_ONE(r_ok)
695695
IREP_ID_ONE(w_ok)
696696
IREP_ID_ONE(super_class)
697697
IREP_ID_ONE(exceptions_thrown_list)
698+
IREP_ID_TWO(C_java_method_type, #java_method_type)
698699

699700
// Projects depending on this code base that wish to extend the list of
700701
// available ids should provide a file local_irep_ids.def in their source tree

0 commit comments

Comments
 (0)