fix bug in global procedures: always prepend self reference

p-org · Nov 1, 2024 · f27e546 · f27e546
1 parent 60f804f
commit f27e546
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs
@@ -1195,7 +1195,7 @@ private void GenerateGlobalProcedures(IEnumerable<Function> functions, List<Inva
         // TODO: these should be side-effect free and we should enforce that
         foreach (var f in functions)
         {
-            var ps = f.Signature.Parameters.Select(p => $"{GetLocalName(p)}: {TypeToString(p.Type)}");
+            var ps = f.Signature.Parameters.Select(p => $"{GetLocalName(p)}: {TypeToString(p.Type)}").Prepend($"this: {MachineRefT}");
 
             if (f.Body is null)
             {
@@ -1568,7 +1568,7 @@ private void GenerateStmt(IPStmt stmt, Machine specMachine, List<Invariant> goal
                     fargs = fargs.Prepend("this");
                 }
 
-                EmitLine($"call ({v}) = {f}({string.Join(", ", fargs)});");
+                EmitLine($"call ({v}) = {f}({string.Join(", ", fargs.Prepend("this"))});");
                 return;
             case AssignStmt { Value: ChooseExpr, Location: VariableAccessExpr } cstmt:
                 var chooseExpr = (ChooseExpr)cstmt.Value;