Skip to content

Bounds context: validate [4/n] #853

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.

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

Merged
merged 69 commits into from
Jul 9, 2020
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
69 commits
Select commit Hold shift + click to select a range
58a610b
Update GetRValueVariable comment
Apr 11, 2020
fb5f2b6
Fix ReplaceVariableHelper::TransformImplicitCastExpr to preserve impl…
Apr 11, 2020
2e54863
Clear G before checking a top-level CFG statement
Apr 11, 2020
62df1c7
Account for value-preserving casts when getting the original variable…
Apr 11, 2020
f87e9e2
Replace GetEqualExprSetContainingVariable with GetEqualExprSetContain…
Apr 11, 2020
c6b7527
Add RecordEqualityWithTarget method
Apr 12, 2020
729bc4b
Add target to G in RecordEqualityWithTarget
Apr 12, 2020
ed05ad9
Add initial EqualExprsContainsAllVars method
Apr 13, 2020
c62d669
Add GetRValueVariable call to EqualExprsContainsAllVars
Apr 13, 2020
4a08f34
Don't record equality with NullToPointer casts
Apr 17, 2020
a2eca86
Add value-preserving cast tests
Apr 17, 2020
2dba020
Allow equality with NullToPointer casts and add type compatibility ch…
Apr 25, 2020
2bc7be0
Revert "Allow equality with NullToPointer casts and add type compatib…
Apr 27, 2020
74f922f
Merge branch 'master' of https://github.com/Microsoft/checkedc-clang …
Apr 27, 2020
a21de03
Add type compatibility check (while not allowing NullToPointer casts …
Apr 28, 2020
dc8a382
Account for value-preserving operations in type compatibility check
May 1, 2020
b0eaf9f
Allow NullToPointer casts to be included in UEQ
May 1, 2020
554fd9b
Add test for type compatibility check in original value
May 1, 2020
e6b7e78
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
May 6, 2020
227ef68
Use the observed bounds as the rvalue bounds of an array pointer cast
May 7, 2020
3e95dc6
Update ObservedBounds in UpdateAfterAssignment
May 7, 2020
fb5fdd0
Set observed bounds for a variable to the updated source bounds
May 8, 2020
f935961
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
May 12, 2020
aaa2d67
Add test for assignment to a variable used in the RHS bounds
May 12, 2020
33ece55
Add tests for multiple assignments
May 13, 2020
87bc8d0
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
May 13, 2020
8e79c9a
Account for value-preserving operations in GetLValueVariable
May 13, 2020
882eab2
Account for nested assignment equality facts in assignments and initi…
May 14, 2020
4fe16e8
Return updated source bounds from UpdateAfterAssignment
May 14, 2020
4055cff
Use updated source bounds in CheckBinaryOperator
May 14, 2020
2743c63
Use updated result bounds for inc/dec operators
May 14, 2020
b802a39
Add tests for using updated result bounds
May 14, 2020
c2cea3e
Create an integer literal for inc/dec operators on non-integer pointers
May 15, 2020
23fa801
Check bounds at increment/decrement operators on variables
May 15, 2020
c2ed1c5
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
May 15, 2020
b3c1411
Pass Src to UpdateAfterAssignment instead of OriginalValue and Origin…
May 15, 2020
7b1ffc8
Fix VariableDecl declaration
May 15, 2020
ae1b9a4
Pass State.EquivExprs to CheckBoundsDeclAtCallArg
May 15, 2020
7291cc8
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
May 29, 2020
b2d9293
Shorten CheckBoundsDeclAtInitializer comment
Jun 3, 2020
e89867c
Call GetLValueVariable from GetRValueVariable
Jun 3, 2020
217750c
Fix test comments
Jun 3, 2020
3838939
Return target-dependent integer for pointers from CreateIntegerLiteral
Jun 3, 2020
19b045f
Add LostVariables, UnknownSrcBounds, and WidenedVariables to Checking…
Jun 10, 2020
7f862ef
Modify ResetKilledBounds and UpdateCtxWithWidenedBounds to update Che…
Jun 10, 2020
095f1d5
Add Reset method to CheckingState
Jun 10, 2020
73c674e
Update LostVariables and UnknownSrcBounds in UpdateAfterAssignment
Jun 10, 2020
77ab627
Update diagnostic messages to be used to validate bounds
Jun 10, 2020
635f4cd
Add ValidateBoundsContext, DiagnoseUnknownObservedBounds, and CheckOb…
Jun 10, 2020
64dca20
Only check bounds in CheckBinaryOperator for assignments to non-varia…
Jun 11, 2020
122e03b
Add CheckBounds parameter to CheckVarDecl for top-level VarDecls
Jun 11, 2020
6bb4c23
Remove CheckBoundsDeclAtIncrementDecrement
Jun 11, 2020
b62c7af
Modify tests to reflect new and updated diagnostic messages
Jun 11, 2020
66d7776
Modify tests to reflect errors caused by not recording target-source …
Jun 11, 2020
a1a03b0
Merge branch 'bounds-context-assignments' of https://github.com/micro…
Jun 11, 2020
a89125a
Add missing braces
Jun 12, 2020
cfc98a0
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
Jun 12, 2020
048117a
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
Jun 12, 2020
2998505
Merge branch 'bounds-context-assignments' of https://github.com/micro…
Jun 12, 2020
1308612
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
Jun 16, 2020
74e50ed
Merge branch 'bounds-context-assignments' of https://github.com/micro…
Jun 16, 2020
9108beb
Use Sema::NormalizeBounds to get declared bounds in ValidateBoundscon…
Jun 16, 2020
e7402a5
Record equality between target and source (#857)
kkjeer Jun 25, 2020
42cbbf5
Use equivalent expression sets to check memory accesses (#856)
kkjeer Jun 26, 2020
5dda1a6
Merge branch 'master' of https://github.com/microsoft/checkedc-clang …
Jun 30, 2020
821cee2
Add TODO comment with widened bounds issue 867
Jul 2, 2020
373cfc5
Update comments
Jul 7, 2020
29a8658
Add TODOs
Jul 7, 2020
8beae62
Move logic for non-variable assignments to one block
Jul 7, 2020
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
Prev Previous commit
Next Next commit
Update ObservedBounds in UpdateAfterAssignment
  • Loading branch information
kakje committed May 7, 2020
commit 3e95dc671cbd6656ca026a533d42a8546cb6bf09
24 changes: 24 additions & 0 deletions clang/lib/Sema/SemaBounds.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3678,6 +3678,12 @@ namespace {
CheckedScopeSpecifier CSS,
const CheckingState PrevState,
CheckingState &State) {
// Adjust ObservedBounds to account for any uses of V in the bounds
// in PrevState.ObservedBounds.
for (auto Pair : State.ObservedBounds)
State.ObservedBounds[Pair.first] =
ReplaceVariableInBounds(Pair.second, V, OV, CSS);

// Adjust UEQ to account for any uses of V in PrevState.UEQ.
State.UEQ.clear();
for (auto I = PrevState.UEQ.begin(); I != PrevState.UEQ.end(); ++I) {
Expand Down Expand Up @@ -3746,6 +3752,24 @@ namespace {
State.UEQ.push_back(State.G);
}

// If Bounds uses the value of v and an original value is provided,
// ReplaceVariableInBounds will return a bounds expression where the uses
// of v are replaced with the original value.
// If Bounds uses the value of v and no original value is provided,
// ReplaceVariableInBounds will return bounds(unknown).
BoundsExpr *ReplaceVariableInBounds(BoundsExpr *Bounds, DeclRefExpr *V,
Expr *OriginalValue,
CheckedScopeSpecifier CSS) {
Expr *Replaced = ReplaceVariableReferences(S, Bounds, V,
OriginalValue, CSS);
if (!Replaced)
return CreateBoundsUnknown();
else if (BoundsExpr *AdjustedBounds = dyn_cast<BoundsExpr>(Replaced))
return AdjustedBounds;
else
return CreateBoundsUnknown();
}

// UpdateG updates the set G of expressions that produce
// the same value as e.
// e is an expression with exactly one subexpression.
Expand Down
257 changes: 251 additions & 6 deletions clang/test/CheckedC/inferred-bounds/bounds-context.c
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,12 @@

#include <stdchecked.h>

////////////////////////////////////////////////
// No assignments to variables used in bounds //
////////////////////////////////////////////////

// Parameter and local variables with declared count bounds
void f1(array_ptr<int> arr : count(len), int len, int size) {
void declared1(array_ptr<int> arr : count(len), int len, int size) {
// Observed bounds context: { a => bounds(a, a + 5), arr => bounds(arr, arr + len) }
array_ptr<int> a : count(5) = 0;
// CHECK: Statement S:
Expand All @@ -32,11 +36,11 @@ void f1(array_ptr<int> arr : count(len), int len, int size) {
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: IntegerLiteral {{.*}} 5
// CHECK-NEXT: Variable:
// CHECK-NEXT: VarDecl {{.*}} arr
// CHECK-NEXT: ParmVarDecl {{.*}} arr
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK: Bounds:
// CHECK-NEXT: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'arr'
Expand Down Expand Up @@ -72,11 +76,11 @@ void f1(array_ptr<int> arr : count(len), int len, int size) {
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: IntegerLiteral {{.*}} 5
// CHECK-NEXT: Variable:
// CHECK-NEXT: VarDecl {{.*}} arr
// CHECK-NEXT: ParmVarDecl {{.*}} arr
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK: Bounds:
// CHECK-NEXT: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'arr'
Expand All @@ -103,7 +107,7 @@ void f1(array_ptr<int> arr : count(len), int len, int size) {
}

// If statement, redeclared variable
void f2(int flag, int x, int y) {
void declared2(int flag, int x, int y) {
// Observed bounds context: { a => bounds(a, a + x) }
array_ptr<int> a : count(x) = 0;
// CHECK: Statement S:
Expand Down Expand Up @@ -274,3 +278,244 @@ void f2(int flag, int x, int y) {
// CHECK-NEXT: DeclRefExpr {{.*}} 'x'
// CHECK-NEXT: }
}

/////////////////////////////////////////////
// Assignments to variables used in bounds //
/////////////////////////////////////////////

// Assignment to a variable used in its own bounds
void assign1(array_ptr<int> arr : count(1)) {
// Original value of arr: arr - 2
// Observed bounds context: { arr => bounds(arr - 2, (arr - 2) + 1) }
arr = arr + 2;
// CHECK: Statement S:
// CHECK-NEXT: BinaryOperator {{.*}} '='
// CHECK-NEXT: DeclRefExpr {{.*}} 'arr'
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'arr'
// CHECK-NEXT: IntegerLiteral {{.*}} 2
// CHECK-NEXT: Observed bounds context after checking S:
// CHECK-NEXT: {
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} arr
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: IntegerLiteral {{.*}} 1
// CHECK-NEXT: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: BinaryOperator {{.*}} '-'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'arr'
// CHECK-NEXT: IntegerLiteral {{.*}} 2
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: BinaryOperator {{.*}} '-'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'arr'
// CHECK-NEXT: IntegerLiteral {{.*}} 2
// CHECK-NEXT: IntegerLiteral {{.*}} 1
// CHECK-NEXT: }
}

// Assignment to a variable used in other variables' bounds
void assign2(array_ptr<int> a : count(len - 1), char b nt_checked[0] : count(len), unsigned len) {
// Original value of len: len + 3
// Observed bounds context: { a => bounds(a, a + ((len + 3) - 1)), b => bounds(b, b + (len + 3)) }
len = len - 3;
// CHECK: Statement S:
// CHECK-NEXT: BinaryOperator {{.*}} '='
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: BinaryOperator {{.*}} '-'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: ImplicitCastExpr {{.*}} 'unsigned int' <IntegralCast>
// CHECK-NEXT: IntegerLiteral {{.*}} 3
// CHECK-NEXT: Observed bounds context after checking S:
// CHECK-NEXT: {
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} a
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: BinaryOperator {{.*}} '-'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: ImplicitCastExpr {{.*}} 'unsigned int' <IntegralCast>
// CHECK-NEXT: IntegerLiteral {{.*}} 1
// CHECK: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: BinaryOperator {{.*}} '-'
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: ImplicitCastExpr {{.*}} 'unsigned int' <IntegralCast>
// CHECK-NEXT: IntegerLiteral {{.*}} 3
// CHECK-NEXT: ImplicitCastExpr {{.*}} 'unsigned int' <IntegralCast>
// CHECK-NEXT: IntegerLiteral {{.*}} 1
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} b
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'b'
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'b'
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: ImplicitCastExpr {{.*}} 'unsigned int' <IntegralCast>
// CHECK-NEXT: IntegerLiteral {{.*}} 3
// CHECK-NEXT: }
}

// Assignment to a variable doesn't affect bounds that don't use the variable
void assign3(array_ptr<int> a : bounds(unknown), nt_array_ptr<char> b : count(1), int len) {
// Observed bounds context: { a => bounds(unknown), b => bounds(b, b + 1) }
len = 0;
// CHECK: Statement S:
// CHECK-NEXT: BinaryOperator {{.*}} '='
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: IntegerLiteral {{.*}} 0
// CHECK-NEXT: Observed bounds context after checking S:
// CHECK-NEXT: {
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} a
// CHECK-NEXT: NullaryBoundsExpr {{.*}} Unknown
// CHECK-NEXT: Bounds:
// CHECK-NEXT: NullaryBoundsExpr {{.*}} Unknown
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} b
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: IntegerLiteral {{.*}} 1
// CHECK-NEXT: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'b'
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'b'
// CHECK-NEXT: IntegerLiteral {{.*}} 1
// CHECK-NEXT: }
}

// Multiple assignments to variables used in bounds
void assign4(array_ptr<int> a : count(len), unsigned len) {
// Original value of a: a - 1, original value of len: len + 1
// Observed bounds context: { a => bounds(a - 1, (a - 1) + (len + 1)) }
++a, len--;
// CHECK: Statement S:
// CHECK-NEXT: BinaryOperator {{.*}} ','
// CHECK-NEXT: UnaryOperator {{.*}} prefix '++'
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: UnaryOperator {{.*}} postfix '--'
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: Observed bounds context after checking S:
// CHECK-NEXT: {
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} a
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: BinaryOperator {{.*}} '-'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: IntegerLiteral {{.*}} 1
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: BinaryOperator {{.*}} '-'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: IntegerLiteral {{.*}} 1
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: IntegerLiteral {{.*}} 1
}

// Original value of variable used in bounds is another variable
void assign5(array_ptr<int> a : count(len), int len, int size) {
// Observed bounds context: { a => bounds(a, a + len) }
size = len;
// CHECK: Statement S:
// CHECK-NEXT: BinaryOperator {{.*}} '='
// CHECK-NEXT: DeclRefExpr {{.*}} 'size'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: Observed bounds context after checking S:
// CHECK-NEXT: {
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} a
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: }

// Original value of len: size
// Observed bounds context: { a => bounds(a, a + size) }
len = len * 2;
// CHECK: Statement S:
// CHECK-NEXT: BinaryOperator {{.*}} '='
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: BinaryOperator {{.*}} '*'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: IntegerLiteral {{.*}} 2
// CHECK-NEXT: Observed bounds context after checking S:
// CHECK-NEXT: {
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} a
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: Bounds:
// CHECK-NEXT: RangeBoundsExpr
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: BinaryOperator {{.*}} '+'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'a'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'size'
// CHECK-NEXT: }
}

// Assignment to a variable with no original value sets the observed bounds
// that use the variable to unknown
void assign6(array_ptr<int> a : count(len), int len) {
// Original value of len: null
// Observed bounds context: { a => bounds(unknown) }
len = len * 2;
// CHECK: Statement S:
// CHECK-NEXT: BinaryOperator {{.*}} '='
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: BinaryOperator {{.*}} '*'
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: IntegerLiteral {{.*}} 2
// CHECK-NEXT: Observed bounds context after checking S:
// CHECK-NEXT: {
// CHECK-NEXT: Variable:
// CHECK-NEXT: ParmVarDecl {{.*}} a
// CHECK-NEXT: CountBoundsExpr {{.*}} Element
// CHECK-NEXT: ImplicitCastExpr {{.*}} <LValueToRValue>
// CHECK-NEXT: DeclRefExpr {{.*}} 'len'
// CHECK-NEXT: Bounds:
// CHECK-NEXT: NullaryBoundsExpr {{.*}} Unknown
// CHECK-NEXT: }
}