search

gradual-verification / silicon-gv

Mozilla Public License 2.0
0 stars 3 forks source link

The translator should always return the shortest available field name #33

Closed hgouni closed 2 years ago

hgouni commented 2 years ago

For example, consider the aliased receivers x and y.z of sort Ref. If we want to indicate that we have access to some field 'a' in the heap location those receivers point to, then we have two options, x.a and y.z.a. The translator should obtain both of these possibilities and pick the shortest one. Not doing so results in a subtle soundness bug. This has been fixed in e88bde52ddda.

hgouni commented 2 years ago

This was resolved by the referenced commit.