This project is read-only.

loops are not supported when turning statement to expression

Jan 21, 2015 at 10:11 PM
When I make a simple loop in pure ghost function such as
_(def fun()
{
for(i = 0; i < 10; ++i){
....
})

It complains the for loop line with "loops are not supported when turning statement to expression". Anyone got this issue before?
Oct 6, 2015 at 12:57 AM
when defining a function with _(def...) the axiom generated is that the function call returns a value equal to an expression computed by the first-order translation of the function body. Such an expression cannot generally be computed for a function with a loop. If you want to use a def function that iterates, you have to replace the iterations with recursion.

Note that this limitation does not exist for pure ghost functions, whose axioms are generated from the contract rather than the function body. Note however, that there are some soundness issues with pure ghost functions that will not be fixed in VCC3 (the code of which is essentially frozen).