first commit

boogie-org · Dec 2, 2024 · f01a4b9 · f01a4b9
1 parent 3a23efe
commit f01a4b9
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 2 deletions.
diff --git a/Source/Core/AST/AbsyType.cs b/Source/Core/AST/AbsyType.cs
@@ -1679,7 +1679,7 @@ public override Type ResolveType(ResolutionContext rc)
 
       // otherwise: this name is not declared anywhere
       rc.Error(this, "undeclared type: {0}", Name);
-      return this;
+      return Type.Bool; // resolve to "bool" type so that type resolution can continue safely
     }
 
     private List<Type> ResolveArguments(ResolutionContext rc)

diff --git a/Test/civl/large-samples/shared-vector.bpl b/Test/civl/large-samples/shared-vector.bpl
@@ -38,6 +38,7 @@ modifies IntArrayPool;
 }
 yield procedure {:layer 2} IntArray_Alloc(v: Vec int) returns (loc_iv: Loc)
 refines Atomic_IntArray_Alloc;
+ensures call Yield(loc_iv);
 preserves call IntArrayDom();
 {
   var {:linear} one_loc_mutex: One Loc;
@@ -56,7 +57,7 @@ preserves call IntArrayDom();
   call {:layer 2} OldMutexPool := Copy(MutexPool);
   i := 0;
   while (i < Vec_Len(v))
-  invariant {:layer 2} 0 <= i;
+  invariant {:layer 2} 0 <= i && i <= Vec_Len(v);
   invariant {:layer 2} mutexes->dom == values->dom;
   invariant {:layer 2} mutexes->dom->val == (lambda j: int :: 0 <= j && j < i);
   invariant {:layer 2} (forall j: int:: 0 <= j && j < i ==> Map_Contains(MutexPool, Map_At(mutexes, j)->val));

diff --git a/Test/civl/large-samples/treiber-stack.bpl b/Test/civl/large-samples/treiber-stack.bpl
@@ -70,6 +70,8 @@ modifies TreiberPool;
 }
 yield procedure {:layer 4} Alloc() returns (loc_t: Loc)
 refines AtomicAlloc;
+ensures call TopInStack(loc_t);
+ensures call ReachInStack(loc_t);
 preserves call StackDom();
 {
   var top: Option LocTreiberNode;