Skip to content

fix-846: Gobra crashes when trying to return the value of a field from a hyper function #962

@henriman

Description

@henriman

The following two hyper function definitions cause Gobra to crash:

type UDPAddr struct { Port int }

ghost
hyper
decreases
pure func (a UDPAddr) GetPortHyper1() int {
    return a.Port
}

ghost
hyper
requires acc(a)
decreases
pure func (a *UDPAddr) GetPortHyper2() int {
    return a.Port
}

GetPortHyper2 crashes before generating the Viper encoding. The Viper encoding of GetPortHyper1 is the following (referencing undefined a_V0):

function GetPortHyper1_fbe47909_MUDPAddr(a_V00: Tuple1[Int], a_V01: Tuple1[Int]): Int
  decreases
{
  (get0of1(a_V0): Int)
}

While the two function definitions are erroneous, Gobra should report the problem instead of crashing. (These functions could be implemented properly using a relational operator, cf. #963.)

(@jcp19)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions