VCC: Recognize $result

1 files changed, 6 insertions, 1 deletions

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 10e4db10..4354ddc3 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -422,6 +422,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         return name.Substring(5);

       }

 

+      if (name == "$result") {

+        kind = "function return value";

+        return "\\result";

+      }

+

       if (name.StartsWith("res__") && viewOpts.ViewLevel >= 1) {

         kind = "call result";

         return name; 

@@ -686,7 +691,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var fldName = tpl.Func.Name.Substring(3);

         var idx = fldName.LastIndexOf('.');

         if (idx > 0) {

-          return fldName.Substring(0, idx).Replace("_vcc_math_type_", "");
+          return fldName.Substring(0, idx).Replace("_vcc_math_type_", "");

         }

       }