Chopper: added logic for opaque functions - Githubissues

viperproject / silver

Definition of the Viper intermediate verification language.

Mozilla Public License 2.0

78 stars 40 forks source link

Chopper: added logic for opaque functions #779

Closed Felalolf closed 5 months ago

Felalolf commented 5 months ago

Function vertices are now split into FunctionSpec vertices, representing a function spec, and Function vertices, representing the entire function.

Dependencies have changed as follows:

For non-opaque functions, we have FunctionSpec -> Function
Function applications without reveal point to FunctionSpec
Function applications with reveal point to Function

@Dspil @jcp19 Please check whether the chopper works as intended by connecting Gobra to it.