I'm writing this to report a simple code fragment that does not compile :-)
Replace mem_naive_micro.c with the following:
void compute(struct In *input, struct Out *output) {
int zeroth = input->in[0];
int first = input->in[1];
int second = input->in[2];
int third = input->in[3];
output->out[0] = zeroth;
output->out[1] = first;
output->out[2] = second;
output->out[3] = third;
}
The following, however, does not error on proving:
/*
Microbenchmark to measure the cost of naive RAM
*/
void compute(struct In *input, struct Out *output) {
int i;
for (i = 0; i < NUMACC; i++) {
output->out[i] = input->in[i] * input->addr[i];
}
}
And this fragment does error on proving:
```cpp
/*
Microbenchmark to measure the cost of naive RAM
*/
void compute(struct In *input, struct Out *output) {
int i;
for (i = 0; i < NUMACC; i++) {
output->out[i] = input->in[i] * input->addr[i];
}
}
So, I believe that the reason the above does not compile is (probably) because there are no multiplications, and therefore no constraints.
I think this could potentially be dealt with by giving a better error message when there are no constraints that come from the code.
Hello Pequin Maintainers,
I'm writing this to report a simple code fragment that does not compile :-)
Replace mem_naive_micro.c with the following:
compile and prove:
it will fail with the following:
The following, however, does not error on proving:
And this fragment does error on proving:
So, I believe that the reason the above does not compile is (probably) because there are no multiplications, and therefore no constraints.
I think this could potentially be dealt with by giving a better error message when there are no constraints that come from the code.
Thank you :-)