From 4ce4cebdf02c8a41ce68f00ac9e657868f211c89 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 6 Feb 2024 17:07:10 +0100 Subject: [PATCH] Fixed rerouting of object___eq__ calls --- src/nagini_translation/translators/common.py | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/nagini_translation/translators/common.py b/src/nagini_translation/translators/common.py index 425708cb..9660d35d 100644 --- a/src/nagini_translation/translators/common.py +++ b/src/nagini_translation/translators/common.py @@ -700,9 +700,9 @@ def get_function_call(self, receiver: PythonType, guard = self.type_check(args[0], cls, position, ctx) # Translate the function call on this particular receiver's class - function = self._get_function_call(cls, func_name, args, - arg_types, node, ctx, - position) + function = self.get_function_call(cls, func_name, args, + arg_types, node, ctx, + position) # Stores guard and translated function call as tuple in a list guarded_functions.append((guard, function)) @@ -711,13 +711,15 @@ def get_function_call(self, receiver: PythonType, # expression return chain_cond_exp(guarded_functions, self.viper, position, self.no_info(ctx), ctx) - elif func_name == '__eq__' and receiver.python_class.name == OBJECT_TYPE: - assert len(args) == 2 - arg1 = self.to_ref(args[0], ctx) - arg2 = self.to_ref(args[1], ctx) - return self.viper.DomainFuncApp('object___eq__', [arg1, arg2], self.viper.Bool, position, - self.no_info(ctx), '__ObjectEquality') else: + if func_name == '__eq__': + func_cls = receiver.get_function(func_name).cls + if func_cls.name == OBJECT_TYPE: + assert len(args) == 2 + arg1 = self.to_ref(args[0], ctx) + arg2 = self.to_ref(args[1], ctx) + return self.viper.DomainFuncApp('object___eq__', [arg1, arg2], self.viper.Bool, position, + self.no_info(ctx), '__ObjectEquality') if receiver.python_class.name == FLOAT_TYPE: if ctx.float_encoding is None: import logging