Impure assume

[bruggerl]

This PR lifts the definition of assume statements such that impure expressions are supported.

In regards to the translation to Viper, consider the following Gobra code snippet:

type person struct { ... }

func test() {
    p := &person{...}
    assume acc(p)
    inhale acc(p)
}

Gobra generates the following Viper code for the assume and inhale statement in the function test:

// assume acc(*p_V0)
inhale (let fn$$4 ==
    (p_V0) in
    perm((ShStructget0of2(fn$$4): Ref).String$$$$_E_$$$) >= write &&
    perm((ShStructget1of2(fn$$4): Ref).Intint$$$$_E_$$$) >= write)
      
// inhale acc(*p_V0)
inhale (let fn$$5 ==
    (p_V0) in
    acc((ShStructget0of2(fn$$5): Ref).String$$$$_E_$$$, write) &&
    acc((ShStructget1of2(fn$$5): Ref).Intint$$$$_E_$$$, write))

This is in line with what Viper does. For example, the Viper program

field f: Int

method test(a: Ref)
{
    assume acc(a.f)
    inhale acc(a.f)
}

gets translated to the following code (obtained with --printTranslatedProgram):

field f: Int

method test(a: Ref)
{
  inhale perm(a.f) >= write
  inhale acc(a.f, write)
}

[jcp19]

😄 😄