diff options
| author |  Unknown <mbarnett@MIKE-SONY.redmond.corp.microsoft.com> | 2012-07-31 16:22:49 -0700 |
|---|---|---|
| committer | Unknown <mbarnett@MIKE-SONY.redmond.corp.microsoft.com> | 2012-07-31 16:22:49 -0700 |
| commit | 4afe0b60ef0a72161a1d37d0ddf266d52e36d186 (patch) | |
| tree | e5f6dc2fbd3dd4721ba0179094e98d539b719877 /BCT/RegressionTests | |
| parent | c3f4fae804fe07942cc1f0e4fc6e40b2542de645 (diff) | |
Add an option to model exceptional control flow or not. When it is false:
method calls are not followed by a test to see if an exception was thrown
"throw e" is translated as "assume false"
"try S catch C finally F" is translated as "S; F"
Diffstat (limited to 'BCT/RegressionTests')
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 30 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 30 |
2 files changed, 60 insertions, 0 deletions
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 0fe003ae..0a2a515a 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -997,6 +997,36 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: +implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)
+{
+ var xs: Ref;
+ var $localExc: Ref;
+ var $label: int;
+
+ xs := xs$in;
+ assume {:breadcrumb 13} true;
+ if (xs != null)
+ {
+ }
+ else
+ {
+ }
+
+ if ((if xs != null then $ArrayLength(xs) > 0 else false))
+ {
+ assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ assume $this != null;
+ assume xs != null;
+ $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];
+ }
+ else
+ {
+ }
+}
+
+
+
procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);
free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 5dfc582e..b552ee36 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -983,6 +983,36 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: +implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)
+{
+ var xs: Ref;
+ var $localExc: Ref;
+ var $label: int;
+
+ xs := xs$in;
+ assume {:breadcrumb 13} true;
+ if (xs != null)
+ {
+ }
+ else
+ {
+ }
+
+ if ((if xs != null then $ArrayLength(xs) > 0 else false))
+ {
+ assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ assume $this != null;
+ assume xs != null;
+ $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];
+ }
+ else
+ {
+ }
+}
+
+
+
procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);
free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);
|