diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-05-28 13:03:08 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-05-28 13:03:08 -0700 |
| commit | 2ce23c96bfe860cfbe5662d3565037e556700ee8 (patch) | |
| tree | 9ea94506a32f26b3fcc6fedfec8ed0c0497486c1 /BCT/RegressionTests | |
| parent | 10b8ba49602b22300746cfb770f55a0b8e115d55 (diff) | |
Translate assignments to parameters that are of a struct type correctly. Note
that this means all methods with such parameters (where the parameter is passed
by value) must have free preconditions expressing that the parameters are
disjoint (since we are representing structs as Ref).
Diffstat (limited to 'BCT/RegressionTests')
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 2 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 98dcbca4..93f3a127 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -692,6 +692,8 @@ implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref) procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref);
+ free requires this != other;
+ free ensures this != other;
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 58085075..48d2c942 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -682,6 +682,8 @@ implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref) procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref);
+ free requires this != other;
+ free ensures this != other;
|