1
Vote

Legal C99 file-scope const misparsed

description

/* Today I ran into a bug which is hopefully not grave, but worth being mentioned. */

include <vcc.h>

const int i; /* References are given with respect to the C99 standard. The variable i has external linkage by 6.2.2, para 5, static storage duration by 6.2.4, para 3. Its initial value is 0 by 6.7.8, para 10. */

int main(void) {
_(assert i==0);
return 0;
}

/* The file contains a legal C99 code. Output of vcc /3:

OOPS: error in expr
Exiting with 3 (1 error(s).)

Notice that the location of the error is missing, which is a headache if the file is large.
*/

/* vcc /version returns:
Microsoft Research Vcc Version 2.1.40523.0
Microsoft Research Boogie Version 2.1.30503.0
Microsoft Research Z3 Version 2.0.41203.1
*/

comments

AlexMalkis wrote May 25, 2011 at 12:28 PM

The code seems also to be legal according to the ANSI C 1988 standard:
  • Section 3.1.2.2 says that the linkage of i is external;
  • Section 3.1.2.4 says that the storage duration is static;
  • Section 3.5.7 says that the initial value is 0.
The bug is not bothering me at all, I was just curious.

MarkHillebrand wrote May 25, 2011 at 2:56 PM

Hi Alex,

your report is valid. We don't support 0-initialization for external statics as this time, though, but at least we shouldn't OOPS on that. Be aware, that const support in VCC is also limited in other ways.

Best, Mark

AlexMalkis wrote May 25, 2011 at 4:11 PM

Mark, thank you for the warning! As long as the construction is unsupported, an OOPS is better for me (though I would prefer the line number to be displayed too) than a silent acceptance of the code. Alexander.

Sign in to add a comment or to set email notifications