Skip to content

Cannot Dereference Dynamically Sized (Template) Type #1144

@DavePearce

Description

@DavePearce

Test 001137 is as follows:

method assign<T>(&T x, &T y, T v1, T v2)
ensures *x == v1
ensures *y == v2:
    // Broken if x == y
    *x = v1
    *y = v2

This doesn't allow the dereference. I think to make this work, we need some information about T --- namely that it is statically sized. This is evident from the fact that it is passed as a parameter.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions