Ghost code is very nice for making abstract specifications and for verification of complex code. Currently, there seems to be a lack of support for ghost annotations in Tricera. For example, the following example can not be parsed:
//@ ghost int v;
/*@ requires v <= 0;
requires v >= 1000;
assigns v;
ensures v - \old(v) == 1;
*/
void main() {
//@ ghost v = v + 1;
}This example fails with the following error message:
'Syntax Error, trying to recover and continue parse... for input symbol "" spanning from unknown:1/5(4) to unknown:1/10(9)
(error "Unrecoverable Syntax Error")
Other Error: Unrecoverable Syntax Error'
Ghost code is very nice for making abstract specifications and for verification of complex code. Currently, there seems to be a lack of support for ghost annotations in Tricera. For example, the following example can not be parsed:
This example fails with the following error message:
'Syntax Error, trying to recover and continue parse... for input symbol "" spanning from unknown:1/5(4) to unknown:1/10(9)
(error "Unrecoverable Syntax Error")
Other Error: Unrecoverable Syntax Error'