Skip to content

Wrong error from #903 when passing _Assume_bounds_cast directly to function with itype #974

Closed
@mattmccutchen-cci

Description

@mattmccutchen-cci

In this program itype-assume-bounds-error.c:

void foo(_Ptr<int> p);
void foo_itype(int *p : itype(_Ptr<int>));

void bar() {
  int *p = 0;
  foo(_Assume_bounds_cast<_Ptr<int>>(p));
  foo_itype(_Assume_bounds_cast<_Ptr<int>>(p));

  _Ptr<int> q = _Assume_bounds_cast<_Ptr<int>>(p);
  foo(q);
  foo_itype(q);
}

After #903, clang -c -o /dev/null itype-assume-bounds-error.c gives the following error:

itype-assume-bounds-error.c:7:13: error: it is not possible to prove argument meets declared bounds for 1st parameter
  foo_itype(_Assume_bounds_cast<_Ptr<int>>(p));
            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
itype-assume-bounds-error.c:7:13: note: the expected argument bounds use the variable 'p' and there is no relational information involving 'p' and any of the expressions used by the inferred bounds
itype-assume-bounds-error.c:7:13: note: (expanded) expected argument bounds are 'bounds((_Array_ptr<int>)_Assume_bounds_cast<_Ptr<int>>p(count(1)), (_Array_ptr<int>)_Assume_bounds_cast<_Ptr<int>>p(count(1)) + 1)'
itype-assume-bounds-error.c:7:13: note: (expanded) inferred bounds are 'bounds((_Array_ptr<int>)value of p, (_Array_ptr<int>)value of p + 1)'
  foo_itype(_Assume_bounds_cast<_Ptr<int>>(p));
            ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Before #903, this was a warning.

I'm no expert on the Checked C rules, but it looks like the cause of the error is that the _Assume_bounds_cast is present in the expression for the expected bounds but not the actual bounds. The fact that the error doesn't occur when the casted value is assigned to another local variable before being passed to foo_itype leads me to believe this is a bug. It's interesting that the problem does not occur with a function foo that takes the checked type outright rather than using an itype.

This is a simplified version of a failure we saw in a recently added 3C regression test that has not yet been submitted to this repository when we tried to merge from this repository (correctcomputation#407). I'm hoping that the root cause is the same and a fix to the case above will also fix our regression test.

Metadata

Metadata

Assignees

Labels

bugThis labels issues that are bugs.priority:2This labels bugs that require immediate attention.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions