In the example, neither loop can be perforated, despite the annotations. Is this expected?
On a related note, it would be very helpful if accept told you where the loop exit was, the same way it tells you what line an assignment to a precise value or an impure function call is.
#include <assert.h>
#include <enerc.h>
int main() {
APPROX int x_approx = 0;
for (int i = 0; i < 1000; ++i) {
assert(x_approx <= 2000); // ACCEPT_PERMIT
x_approx += 1;
}
for (int i = 0; i < 1000; ++i) {
if (i > 557) // ACCEPT_PERMIT
break; // ACCEPT_PERMIT
x_approx += 1;
}
return ENDORSE(x_approx);
}
In the example, neither loop can be perforated, despite the annotations. Is this expected?
On a related note, it would be very helpful if accept told you where the loop exit was, the same way it tells you what line an assignment to a precise value or an impure function call is.