Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fixed type resolution crash #992

Merged
merged 3 commits into from
Dec 2, 2024
Merged

Fixed type resolution crash #992

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f01a4b9
first commit
shazqadeer Dec 2, 2024
4fa978c
second commit
shazqadeer Dec 2, 2024
60e7ad8
third commit
shazqadeer Dec 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Source/Core/AST/AbsyType.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1678,8 +1678,8 @@ public override Type ResolveType(ResolutionContext rc)
}

// otherwise: this name is not declared anywhere
rc.Error(this, "undeclared type: {0}", Name);
return this;
rc.Error(this, "undeclared type: {0} (replacing with \"bool\" to continue resolving)", Name);
return Type.Bool;
}

private List<Type> ResolveArguments(ResolutionContext rc)
Expand Down
2 changes: 1 addition & 1 deletion Test/bitvectors/bv2.bpl.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
bv2.bpl(6,13): Error: bitvector bounds in illegal position
bv2.bpl(8,13): Error: undeclared type: x
bv2.bpl(8,13): Error: undeclared type: x (replacing with "bool" to continue resolving)
bv2.bpl(9,14): Error: bitvector bounds in illegal position
3 name resolution errors detected in bv2.bpl
3 changes: 2 additions & 1 deletion Test/civl/large-samples/shared-vector.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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));
Expand Down
2 changes: 2 additions & 0 deletions Test/civl/large-samples/treiber-stack.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions Test/test0/Types1.bpl.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
Types1.bpl(8,11): Error: undeclared type: x
Types1.bpl(9,11): Error: undeclared type: x
Types1.bpl(9,14): Error: undeclared type: x
Types1.bpl(8,11): Error: undeclared type: x (replacing with "bool" to continue resolving)
Types1.bpl(9,11): Error: undeclared type: x (replacing with "bool" to continue resolving)
Types1.bpl(9,14): Error: undeclared type: x (replacing with "bool" to continue resolving)
3 name resolution errors detected in Types1.bpl
4 changes: 2 additions & 2 deletions Test/test20/Prog0.bpl.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Prog0.bpl(19,10): Error: type variable must occur in map arguments: a
Prog0.bpl(31,27): Error: more than one declaration of type variable: beta
Prog0.bpl(34,22): Error: undeclared type: alpha
Prog0.bpl(35,35): Error: undeclared type: alpha
Prog0.bpl(34,22): Error: undeclared type: alpha (replacing with "bool" to continue resolving)
Prog0.bpl(35,35): Error: undeclared type: alpha (replacing with "bool" to continue resolving)
4 name resolution errors detected in Prog0.bpl
4 changes: 2 additions & 2 deletions Test/test20/TypeDecls0.bpl.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ TypeDecls0.bpl(15,12): Error: more than one declaration of type variable: a
TypeDecls0.bpl(16,18): Error: more than one declaration of type variable: a
TypeDecls0.bpl(20,17): Error: type variable must occur in map arguments: b
TypeDecls0.bpl(24,9): Error: type constructor received wrong number of arguments: C
TypeDecls0.bpl(26,9): Error: undeclared type: A0
TypeDecls0.bpl(27,9): Error: undeclared type: F
TypeDecls0.bpl(26,9): Error: undeclared type: A0 (replacing with "bool" to continue resolving)
TypeDecls0.bpl(27,9): Error: undeclared type: F (replacing with "bool" to continue resolving)
TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E
TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E
TypeDecls0.bpl(34,9): Error: type constructor received wrong number of arguments: E
Expand Down
Loading