diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-03-12 14:41:07 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-03-12 14:41:07 +0000 |
commit | 8fb2eba8404a1355d8867e0cfa0028ea941fcdaf (patch) | |
tree | eb411ce6e7dfd0eb26b5d020549a6f07ac708ab2 /test/regression/initializers.c | |
parent | b683a90f06fd10e0b0defc176a15b7272564ffd9 (diff) | |
download | compcert-8fb2eba8404a1355d8867e0cfa0028ea941fcdaf.tar.gz compcert-8fb2eba8404a1355d8867e0cfa0028ea941fcdaf.zip |
Initializers for global variables: compile-time evaluation of expressions done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'test/regression/initializers.c')
-rw-r--r-- | test/regression/initializers.c | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regression/initializers.c b/test/regression/initializers.c index 97ce99b0..73840918 100644 --- a/test/regression/initializers.c +++ b/test/regression/initializers.c @@ -35,6 +35,17 @@ int * x14 = &x2; struct { char * y; int * z; float * u; double * v; } x15 = { x4, x5, &x11, &x12 }; +unsigned char * x16[3] = { + (unsigned char *) (x4 + 1), + (unsigned char *) &x4[2], + ((unsigned char *) x4) + 3 }; + +char x17[] = "Hello!"; + +char * x18 = "Hello!"; + +char * x19[2] = { "Hello", "world!" }; + int main(int argc, char ** argv) { int i; @@ -63,6 +74,17 @@ int main(int argc, char ** argv) printf("x15 ok\n"); else printf("x15 error\n"); + if (x16[0] == (unsigned char *) x4 + 1 + && x16[1] == (unsigned char *) x4 + 2 + && x16[2] == (unsigned char *) x4 + 3) + printf("x16 ok\n"); + else + printf("x16 error\n"); + printf("x17[%d] = { ", (int) sizeof(x17)); + for (i = 0; i < sizeof(x17); i++) printf("'%c', ", x17[i]); + printf("}\n"); + printf("x18 = \"%s\"\n", x18); + printf("x19 = { \"%s\", \"%s\" }\n", x19[0], x19[1]); return 0; } |