This PR adds support for (some) ACSL-Ghost-Statements, specifically:
//@ ghost T x; (local or global context)
//@ ghost T x = expr; (local or global context)
//@ ghost x = expr; (local context only)
This new language feature can then also help to validate witnesses with ghost variables (see here; a PR of that will be created this one is merged 🙂).
In our translation we create and declare a new Boogie-Variable #ghost~x and handle the assignment accordingly. Additionally we make sure that only ghost-variables are assigned in ghost-statements (so it should not have any side-effects on program-variables).
However, we need to handle the declaration of global variables (parsed as GlobalGhostDeclaration) and local variables (parsed as GhostDeclaration) slightly different, because the first is handled by CHandler and the latter by ACSLHandler. This leads to some duplicate code, but the handling is also slightly different.
This PR adds support for (some) ACSL-Ghost-Statements, specifically:
//@ ghost T x;(local or global context)//@ ghost T x = expr;(local or global context)//@ ghost x = expr;(local context only)This new language feature can then also help to validate witnesses with ghost variables (see here; a PR of that will be created this one is merged 🙂).
In our translation we create and declare a new Boogie-Variable
#ghost~xand handle the assignment accordingly. Additionally we make sure that only ghost-variables are assigned in ghost-statements (so it should not have any side-effects on program-variables).However, we need to handle the declaration of global variables (parsed as
GlobalGhostDeclaration) and local variables (parsed asGhostDeclaration) slightly different, because the first is handled byCHandlerand the latter byACSLHandler. This leads to some duplicate code, but the handling is also slightly different.