(phone bct) nav graph building (mostly) automated

2 files changed, 8 insertions, 0 deletions

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 59d9be9b..0ea68d94 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -324,6 +324,7 @@ procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boole
 

 implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool)

 {

+    $Exception:=null;

     isControlEnabled[$this] := value$in;

 }

 

@@ -337,6 +338,7 @@ implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns
 {

   var enabledness: bool;

 

+    $Exception:=null;

     enabledness := isControlEnabled[$this];

     $result := Box2Ref(Bool2Box(enabledness));

 }

@@ -351,6 +353,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$Sys
 {

   var check: bool;

 

+    $Exception:=null;

     check := Box2Bool(Ref2Box(value$in));

     isControlChecked[$this] := check;

 }

@@ -365,6 +368,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($th
 {

   var isChecked: bool;

 

+    $Exception:=null;

     isChecked := isControlChecked[$this];

     $result := Box2Ref(Bool2Box(isChecked));

 }

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index d93b6815..6c7ba975 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -322,6 +322,7 @@ procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boole
 

 implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool)

 {

+    $Exception:=null;

     isControlEnabled[$this] := value$in;

 }

 

@@ -335,6 +336,7 @@ implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns
 {

   var enabledness: bool;

 

+    $Exception:=null;

     enabledness := isControlEnabled[$this];

     $result := Box2Ref(Bool2Box(enabledness));

 }

@@ -349,6 +351,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$Sys
 {

   var check: bool;

 

+    $Exception:=null;

     check := Box2Bool(Ref2Box(value$in));

     isControlChecked[$this] := check;

 }

@@ -363,6 +366,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($th
 {

   var isChecked: bool;

 

+    $Exception:=null;

     isChecked := isControlChecked[$this];

     $result := Box2Ref(Bool2Box(isChecked));

 }