Test fix: Include uniqueness postconditions in new test of #218 (#228)

jesyspa · Jul 30, 2024 · d414900 · d414900
1 parent 872e622
commit d414900
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/...formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt b/...formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt
@@ -466,6 +466,7 @@ method class_CustomClass$constructor$fun_take$$return$T_class_global$class_Custo
   returns (ret: Ref)
   ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret), dom$RuntimeType$T_class_global$class_CustomClass())
   ensures acc(T_class_global$class_CustomClass(ret), wildcard)
+  ensures acc(Unique$T_class_global$class_CustomClass(ret), write)
 
 
 method global$fun_testCustomClass$fun_take$$return$T_Boolean()