Fixed rerouting of object___eq__ calls

marcoeilers · Feb 6, 2024 · 4ce4ceb · 4ce4ceb
1 parent 7adee38
commit 4ce4ceb
Showing 1 changed file with 11 additions and 9 deletions.
diff --git 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