Closed bruggerl closed 2 months ago
This PR lifts the definition of assume statements such that impure expressions are supported.
assume
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:
inhale
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):
--printTranslatedProgram
field f: Int method test(a: Ref) { inhale perm(a.f) >= write inhale acc(a.f, write) }
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:
Gobra generates the following Viper code for the
assume
andinhale
statement in the functiontest
:This is in line with what Viper does. For example, the Viper program
gets translated to the following code (obtained with
--printTranslatedProgram
):