Return

the virgin formal methods

1 Name: Anonymous 2017-12-19 20:58
https://github.com/AbsInt/CompCert/issues/211

We found a run-time error with SuperTest for the program below. The program should print 100 for the value of 'press', but when compiled with CompCert 3.1 on an x86 Apple Mac, it prints 3. It looks like CompCert is confused about the scopes of the two variables called 'press'.

===========================================

#include <stdio.h>

int press = 100;
int valve = 0;

int main (void) {
for (int press = 0; press < 3; press++) {
valve++;
}
printf ("Value of 'press' should be 100, is: %d\n", press);
return valve - 3;
}


* Do not pass the env back from for stmt decls.

This is the source of issue #211, the environment from the elaboration of
the declaration and expressions in the for loop should not be passed back.
2 Name: Anonymous 2017-12-20 01:12
http://compcert.inria.fr/man/manual001.html#sec10 shows the project structure, and claims the parser is in fact verified.

Edit: https://xavierleroy.org/publi/validated-parser.pdf has the full story on the verified parser. In brief, it’s verified with respect to an input grammar. Which, in this case, contained an error.
3 Name: Anonymous 2017-12-25 09:38
4 Name: Anonymous 2017-12-28 13:47

Return
Name:
Leave this field blank: