Skip to content

Improve equivalence checking of pointer arithmetic expressions #596

Open
@dtarditi

Description

@dtarditi

The Checked C specification calls for expanding pointer arithmetic to bytewise arithmetic before checking equivalence of expressions. We're not doing that, which is causing various pointer expressions to not be considered equivalent when they are.

For example, given an expression e1 that is a pointer to T, (Array_ptr<char>) e1 + (sizeof(T) * i) is equivalent to e + i.

This kind of arithmetic arises when a programmer declared bounds for a variable using count, but a programmer does explicit size calculation as part of allocation. For example:

_Array_ptr<int> x : count(i) = malloc(sizeof(int) * i)

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions