17 files changed, 1166 insertions, 65 deletions

diff --git a/test/Makefile b/test/Makefile
index e53dfd83..504e4c53 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -1,4 +1,9 @@
+include ../Makefile.config
+
 DIRS=c compression raytracer spass regression
+ifeq ($(CLIGHTGEN),true)
+DIRS+=clightgen
+endif
 
 all:
 	set -e; for i in $(DIRS); do $(MAKE) CCOMPOPTS='$(CCOMPOPTS)' -C $$i all; done
@@ -6,6 +11,9 @@ all:
 test:
 	set -e; for i in $(DIRS); do $(MAKE) SIMU='$(SIMU)' -C $$i test; done
 
+parallel:
+	parallel $(MAKE) SIMU='$(SIMU)' -C {} test ::: $(DIRS)
+
 bench:
 	for i in $(DIRS); do $(MAKE) -C $$i bench; done
 
diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile
new file mode 100644
index 00000000..0607e2fa
--- /dev/null
+++ b/test/clightgen/Makefile
@@ -0,0 +1,44 @@
+include ../../Makefile.config
+
+ifeq ($(wildcard ../../$(ARCH)_$(BITSIZE)),)
+ARCHDIRS=$(ARCH)
+else
+ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
+endif
+RECDIRS=lib common $(ARCHDIRS) cfrontend flocq  exportclight
+COQINCLUDES=$(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d))
+
+CLIGHTGEN=../../clightgen
+COQC=coqc
+
+# Regression tests in the current directory
+SRC=$(wildcard *.c)
+# From ../c
+SRC+=aes.c almabench.c binarytrees.c bisect.c chomp.c fannkuch.c fft.c \
+  fftsp.c fftw.c fib.c integr.c knucleotide.c lists.c mandelbrot.c \
+  nbody.c nsievebits.c nsieve.c perlin.c qsort.c sha1.c sha3.c \
+  siphash24.c spectral.c vmach.c
+# From ../raytracer
+SRC+=arrays.c eval.c gmllexer.c gmlparser.c intersect.c light.c main.c \
+  matrix.c memory.c object.c render.c simplify.c surface.c vector.c
+
+all: $(SRC:.c=.vo)
+
+test:
+
+%.v: %.c
+	$(CLIGHTGEN) $(CFLAGS) -o $@ $<
+
+%.v: ../c/%.c
+	$(CLIGHTGEN) $(CFLAGS) -o $@ $<
+
+%.v: ../raytracer/%.c
+	$(CLIGHTGEN) -I../raytracer -fall $(CFLAGS) -o $@ $<
+
+%.vo: %.v
+	$(COQC) $(COQINCLUDES) -noglob $<
+
+.SECONDARY: $(SRC:.c=.v)
+
+clean:
+	rm -f *.v *.vo .*.aux
diff --git a/test/clightgen/empty.c b/test/clightgen/empty.c
new file mode 100644
index 00000000..8f8871a7
--- /dev/null
+++ b/test/clightgen/empty.c
@@ -0,0 +1 @@
+/* The empty source file */
diff --git a/test/clightgen/issue196.c b/test/clightgen/issue196.c
new file mode 100644
index 00000000..1821fd6d
--- /dev/null
+++ b/test/clightgen/issue196.c
@@ -0,0 +1,927 @@
+#include <stdint.h>
+#include <stdlib.h>
+#include <sys/types.h>
+
+
+typedef int ASN1_BOOLEAN;
+typedef int ASN1_NULL;
+typedef struct ASN1_ITEM_st ASN1_ITEM;
+typedef struct asn1_object_st ASN1_OBJECT;
+typedef struct asn1_pctx_st ASN1_PCTX;
+typedef struct asn1_string_st ASN1_BIT_STRING;
+typedef struct asn1_string_st ASN1_BMPSTRING;
+typedef struct asn1_string_st ASN1_ENUMERATED;
+typedef struct asn1_string_st ASN1_GENERALIZEDTIME;
+typedef struct asn1_string_st ASN1_GENERALSTRING;
+typedef struct asn1_string_st ASN1_IA5STRING;
+typedef struct asn1_string_st ASN1_INTEGER;
+typedef struct asn1_string_st ASN1_OCTET_STRING;
+typedef struct asn1_string_st ASN1_PRINTABLESTRING;
+typedef struct asn1_string_st ASN1_STRING;
+typedef struct asn1_string_st ASN1_T61STRING;
+typedef struct asn1_string_st ASN1_TIME;
+typedef struct asn1_string_st ASN1_UNIVERSALSTRING;
+typedef struct asn1_string_st ASN1_UTCTIME;
+typedef struct asn1_string_st ASN1_UTF8STRING;
+typedef struct asn1_string_st ASN1_VISIBLESTRING;
+
+typedef struct AUTHORITY_KEYID_st AUTHORITY_KEYID;
+typedef struct DIST_POINT_st DIST_POINT;
+typedef struct ISSUING_DIST_POINT_st ISSUING_DIST_POINT;
+typedef struct NAME_CONSTRAINTS_st NAME_CONSTRAINTS;
+typedef struct X509_POLICY_CACHE_st X509_POLICY_CACHE;
+typedef struct X509_POLICY_LEVEL_st X509_POLICY_LEVEL;
+typedef struct X509_POLICY_NODE_st X509_POLICY_NODE;
+typedef struct X509_POLICY_TREE_st X509_POLICY_TREE;
+typedef struct X509_algor_st X509_ALGOR;
+typedef struct X509_crl_st X509_CRL;
+typedef struct X509_pubkey_st X509_PUBKEY;
+typedef struct bignum_ctx BN_CTX;
+typedef struct bignum_st BIGNUM;
+typedef struct bio_method_st BIO_METHOD;
+typedef struct bio_st BIO;
+typedef struct bn_gencb_st BN_GENCB;
+typedef struct bn_mont_ctx_st BN_MONT_CTX;
+typedef struct buf_mem_st BUF_MEM;
+typedef struct cbb_st CBB;
+typedef struct cbs_st CBS;
+typedef struct conf_st CONF;
+typedef struct dh_method DH_METHOD;
+typedef struct dh_st DH;
+typedef struct dsa_method DSA_METHOD;
+typedef struct dsa_st DSA;
+typedef struct ec_key_st EC_KEY;
+typedef struct ecdsa_method_st ECDSA_METHOD;
+typedef struct ecdsa_sig_st ECDSA_SIG;
+typedef struct engine_st ENGINE;
+typedef struct env_md_ctx_st EVP_MD_CTX;
+typedef struct env_md_st EVP_MD;
+typedef struct evp_aead_st EVP_AEAD;
+typedef struct evp_cipher_ctx_st EVP_CIPHER_CTX;
+typedef struct evp_cipher_st EVP_CIPHER;
+typedef struct evp_pkey_asn1_method_st EVP_PKEY_ASN1_METHOD;
+typedef struct evp_pkey_ctx_st EVP_PKEY_CTX;
+typedef struct evp_pkey_method_st EVP_PKEY_METHOD;
+typedef struct evp_pkey_st EVP_PKEY;
+typedef struct hmac_ctx_st HMAC_CTX;
+typedef struct md4_state_st MD4_CTX;
+typedef struct md5_state_st MD5_CTX;
+typedef struct pkcs8_priv_key_info_st PKCS8_PRIV_KEY_INFO;
+typedef struct pkcs12_st PKCS12;
+typedef struct rand_meth_st RAND_METHOD;
+typedef struct rc4_key_st RC4_KEY;
+typedef struct rsa_meth_st RSA_METHOD;
+typedef struct rsa_st RSA;
+typedef struct sha256_state_st SHA256_CTX;
+typedef struct sha512_state_st SHA512_CTX;
+typedef struct sha_state_st SHA_CTX;
+typedef struct ssl_ctx_st SSL_CTX;
+typedef struct ssl_st SSL;
+typedef struct st_ERR_FNS ERR_FNS;
+typedef struct v3_ext_ctx X509V3_CTX;
+typedef struct x509_crl_method_st X509_CRL_METHOD;
+typedef struct x509_revoked_st X509_REVOKED;
+typedef struct x509_st X509;
+typedef struct x509_store_ctx_st X509_STORE_CTX;
+typedef struct x509_store_st X509_STORE;
+typedef void *OPENSSL_BLOCK;
+ const EVP_MD *EVP_md4(void);
+ const EVP_MD *EVP_md5(void);
+ const EVP_MD *EVP_sha1(void);
+ const EVP_MD *EVP_sha224(void);
+ const EVP_MD *EVP_sha256(void);
+ const EVP_MD *EVP_sha384(void);
+ const EVP_MD *EVP_sha512(void);
+
+
+
+ const EVP_MD *EVP_md5_sha1(void);
+
+
+
+ const EVP_MD *EVP_get_digestbynid(int nid);
+
+
+
+ const EVP_MD *EVP_get_digestbyobj(const ASN1_OBJECT *obj);
+ void EVP_MD_CTX_init(EVP_MD_CTX *ctx);
+
+
+
+ EVP_MD_CTX *EVP_MD_CTX_create(void);
+
+
+
+ int EVP_MD_CTX_cleanup(EVP_MD_CTX *ctx);
+
+
+ void EVP_MD_CTX_destroy(EVP_MD_CTX *ctx);
+
+
+
+ int EVP_MD_CTX_copy_ex(EVP_MD_CTX *out, const EVP_MD_CTX *in);
+
+
+
+
+
+
+
+ int EVP_DigestInit_ex(EVP_MD_CTX *ctx, const EVP_MD *type,
+                                     ENGINE *engine);
+
+
+
+ int EVP_DigestInit(EVP_MD_CTX *ctx, const EVP_MD *type);
+
+
+
+ int EVP_DigestUpdate(EVP_MD_CTX *ctx, const void *data,
+                                    size_t len);
+ int EVP_DigestFinal_ex(EVP_MD_CTX *ctx, uint8_t *md_out,
+                                      unsigned int *out_size);
+
+
+
+ int EVP_DigestFinal(EVP_MD_CTX *ctx, uint8_t *md_out,
+                                   unsigned int *out_size);
+
+
+
+
+
+
+ int EVP_Digest(const void *data, size_t len, uint8_t *md_out,
+                              unsigned int *md_out_size, const EVP_MD *type,
+                              ENGINE *impl);
+ int EVP_MD_type(const EVP_MD *md);
+
+
+ const char *EVP_MD_name(const EVP_MD *md);
+
+
+
+ uint32_t EVP_MD_flags(const EVP_MD *md);
+
+
+ size_t EVP_MD_size(const EVP_MD *md);
+
+
+ size_t EVP_MD_block_size(const EVP_MD *md);
+ int EVP_MD_CTX_copy(EVP_MD_CTX *out, const EVP_MD_CTX *in);
+
+
+
+ int EVP_add_digest(const EVP_MD *digest);
+
+
+
+
+
+
+ const EVP_MD *EVP_MD_CTX_md(const EVP_MD_CTX *ctx);
+
+
+
+ unsigned EVP_MD_CTX_size(const EVP_MD_CTX *ctx);
+
+
+
+ unsigned EVP_MD_CTX_block_size(const EVP_MD_CTX *ctx);
+
+
+
+
+ int EVP_MD_CTX_type(const EVP_MD_CTX *ctx);
+
+
+ void EVP_MD_CTX_set_flags(EVP_MD_CTX *ctx, uint32_t flags);
+
+
+
+ void EVP_MD_CTX_clear_flags(EVP_MD_CTX *ctx, uint32_t flags);
+
+
+
+ uint32_t EVP_MD_CTX_test_flags(const EVP_MD_CTX *ctx,
+                                              uint32_t flags);
+
+
+struct evp_md_pctx_ops;
+
+struct env_md_ctx_st {
+
+  const EVP_MD *digest;
+
+  uint32_t flags;
+
+
+  void *md_data;
+
+
+
+  int (*update)(EVP_MD_CTX *ctx, const void *data, size_t count);
+
+
+
+  EVP_PKEY_CTX *pctx;
+
+
+
+  const struct evp_md_pctx_ops *pctx_ops;
+} ;
+
+ int MD4_Init(MD4_CTX *md4);
+
+
+ int MD4_Update(MD4_CTX *md4, const void *data, size_t len);
+
+
+
+
+ int MD4_Final(uint8_t *md, MD4_CTX *md4);
+
+
+
+ void MD4_Transform(MD4_CTX *md4, const uint8_t *block);
+
+struct md4_state_st {
+  uint32_t A, B, C, D;
+  uint32_t Nl, Nh;
+  uint32_t data[16];
+  unsigned int num;
+};
+ int MD5_Init(MD5_CTX *md5);
+
+
+ int MD5_Update(MD5_CTX *md5, const void *data, size_t len);
+
+
+
+
+ int MD5_Final(uint8_t *md, MD5_CTX *md5);
+
+
+
+ uint8_t *MD5(const uint8_t *data, size_t len, uint8_t *out);
+
+
+
+ void MD5_Transform(MD5_CTX *md5, const uint8_t *block);
+
+struct md5_state_st {
+  uint32_t A, B, C, D;
+  uint32_t Nl, Nh;
+  uint32_t data[16];
+  unsigned int num;
+};
+struct cbs_st {
+  const uint8_t *data;
+  size_t len;
+};
+
+
+
+ void CBS_init(CBS *cbs, const uint8_t *data, size_t len);
+
+
+
+ int CBS_skip(CBS *cbs, size_t len);
+
+
+ const uint8_t *CBS_data(const CBS *cbs);
+
+
+ size_t CBS_len(const CBS *cbs);
+
+
+
+
+
+
+ int CBS_stow(const CBS *cbs, uint8_t **out_ptr, size_t *out_len);
+ int CBS_strdup(const CBS *cbs, char **out_ptr);
+
+
+
+ int CBS_contains_zero_byte(const CBS *cbs);
+
+
+
+
+ int CBS_mem_equal(const CBS *cbs, const uint8_t *data,
+                                 size_t len);
+
+
+
+ int CBS_get_u8(CBS *cbs, uint8_t *out);
+
+
+
+ int CBS_get_u16(CBS *cbs, uint16_t *out);
+
+
+
+ int CBS_get_u24(CBS *cbs, uint32_t *out);
+
+
+
+ int CBS_get_u32(CBS *cbs, uint32_t *out);
+
+
+
+ int CBS_get_bytes(CBS *cbs, CBS *out, size_t len);
+
+
+
+
+ int CBS_get_u8_length_prefixed(CBS *cbs, CBS *out);
+
+
+
+
+ int CBS_get_u16_length_prefixed(CBS *cbs, CBS *out);
+
+
+
+
+ int CBS_get_u24_length_prefixed(CBS *cbs, CBS *out);
+ int CBS_get_asn1(CBS *cbs, CBS *out, unsigned tag_value);
+
+
+
+ int CBS_get_asn1_element(CBS *cbs, CBS *out, unsigned tag_value);
+
+
+
+
+
+
+ int CBS_peek_asn1_tag(const CBS *cbs, unsigned tag_value);
+ int CBS_get_any_asn1_element(CBS *cbs, CBS *out,
+                                            unsigned *out_tag,
+                                            size_t *out_header_len);
+
+
+
+
+
+ int CBS_get_asn1_uint64(CBS *cbs, uint64_t *out);
+
+
+
+
+
+
+ int CBS_get_optional_asn1(CBS *cbs, CBS *out, int *out_present,
+                                         unsigned tag);
+
+
+
+
+
+
+
+ int CBS_get_optional_asn1_octet_string(CBS *cbs, CBS *out,
+                                                      int *out_present,
+                                                      unsigned tag);
+
+
+
+
+
+
+ int CBS_get_optional_asn1_uint64(CBS *cbs, uint64_t *out,
+                                                unsigned tag,
+                                                uint64_t default_value);
+
+
+
+
+
+
+ int CBS_get_optional_asn1_bool(CBS *cbs, int *out, unsigned tag,
+                                              int default_value);
+struct cbb_buffer_st {
+  uint8_t *buf;
+  size_t len;
+  size_t cap;
+  char can_resize;
+
+};
+
+struct cbb_st {
+  struct cbb_buffer_st *base;
+
+
+  size_t offset;
+
+  struct cbb_st *child;
+
+
+  uint8_t pending_len_len;
+  char pending_is_asn1;
+
+
+  char is_top_level;
+};
+
+
+
+
+ int CBB_init(CBB *cbb, size_t initial_capacity);
+
+
+
+
+ int CBB_init_fixed(CBB *cbb, uint8_t *buf, size_t len);
+
+
+
+
+ void CBB_cleanup(CBB *cbb);
+ int CBB_finish(CBB *cbb, uint8_t **out_data, size_t *out_len);
+
+
+
+
+ int CBB_flush(CBB *cbb);
+
+
+
+
+ int CBB_add_u8_length_prefixed(CBB *cbb, CBB *out_contents);
+
+
+
+
+ int CBB_add_u16_length_prefixed(CBB *cbb, CBB *out_contents);
+
+
+
+
+ int CBB_add_u24_length_prefixed(CBB *cbb, CBB *out_contents);
+
+
+
+
+
+
+ int CBB_add_asn1(CBB *cbb, CBB *out_contents, uint8_t tag);
+
+
+
+ int CBB_add_bytes(CBB *cbb, const uint8_t *data, size_t len);
+
+
+
+
+
+ int CBB_add_space(CBB *cbb, uint8_t **out_data, size_t len);
+
+
+
+ int CBB_add_u8(CBB *cbb, uint8_t value);
+
+
+
+ int CBB_add_u16(CBB *cbb, uint16_t value);
+
+
+
+ int CBB_add_u24(CBB *cbb, uint32_t value);
+
+
+
+
+ int CBB_add_asn1_uint64(CBB *cbb, uint64_t value);
+ ASN1_OBJECT *OBJ_dup(const ASN1_OBJECT *obj);
+
+
+
+ int OBJ_cmp(const ASN1_OBJECT *a, const ASN1_OBJECT *b);
+
+
+
+
+
+
+ int OBJ_obj2nid(const ASN1_OBJECT *obj);
+
+
+
+ int OBJ_cbs2nid(const CBS *cbs);
+
+
+
+ int OBJ_sn2nid(const char *short_name);
+
+
+
+ int OBJ_ln2nid(const char *long_name);
+
+
+
+
+ int OBJ_txt2nid(const char *s);
+
+
+
+
+
+
+ const ASN1_OBJECT *OBJ_nid2obj(int nid);
+
+
+ const char *OBJ_nid2sn(int nid);
+
+
+ const char *OBJ_nid2ln(int nid);
+
+
+
+ int OBJ_nid2cbb(CBB *out, int nid);
+ ASN1_OBJECT *OBJ_txt2obj(const char *s, int dont_search_names);
+ int OBJ_obj2txt(char *out, int out_len, const ASN1_OBJECT *obj,
+                               int dont_return_name);
+
+
+
+
+
+
+ int OBJ_create(const char *oid, const char *short_name,
+                              const char *long_name);
+ int OBJ_find_sigid_algs(int sign_nid, int *out_digest_nid,
+                                       int *out_pkey_nid);
+
+
+
+
+
+
+ int OBJ_find_sigid_by_algs(int *out_sign_nid, int digest_nid,
+                                          int pkey_nid);
+ int SHA1_Init(SHA_CTX *sha);
+
+
+ int SHA1_Update(SHA_CTX *sha, const void *data, size_t len);
+
+
+
+
+ int SHA1_Final(uint8_t *md, SHA_CTX *sha);
+
+
+
+
+ uint8_t *SHA1(const uint8_t *data, size_t len, uint8_t *out);
+
+
+
+ void SHA1_Transform(SHA_CTX *sha, const uint8_t *block);
+
+struct sha_state_st {
+  uint32_t h0, h1, h2, h3, h4;
+  uint32_t Nl, Nh;
+  uint32_t data[16];
+  unsigned int num;
+};
+ int SHA224_Init(SHA256_CTX *sha);
+
+
+ int SHA224_Update(SHA256_CTX *sha, const void *data, size_t len);
+
+
+
+ int SHA224_Final(uint8_t *md, SHA256_CTX *sha);
+
+
+
+
+ uint8_t *SHA224(const uint8_t *data, size_t len, uint8_t *out);
+ int SHA256_Init(SHA256_CTX *sha);
+
+
+ int SHA256_Update(SHA256_CTX *sha, const void *data, size_t len);
+
+
+
+ int SHA256_Final(uint8_t *md, SHA256_CTX *sha);
+
+
+
+
+ uint8_t *SHA256(const uint8_t *data, size_t len, uint8_t *out);
+
+
+
+ void SHA256_Transform(SHA256_CTX *sha, const uint8_t *data);
+
+struct sha256_state_st {
+  uint32_t h[8];
+  uint32_t Nl, Nh;
+  uint32_t data[16];
+  unsigned int num, md_len;
+};
+ int SHA384_Init(SHA512_CTX *sha);
+
+
+ int SHA384_Update(SHA512_CTX *sha, const void *data, size_t len);
+
+
+
+ int SHA384_Final(uint8_t *md, SHA512_CTX *sha);
+
+
+
+
+ uint8_t *SHA384(const uint8_t *data, size_t len, uint8_t *out);
+
+
+
+ void SHA384_Transform(SHA512_CTX *sha, const uint8_t *data);
+ int SHA512_Init(SHA512_CTX *sha);
+
+
+ int SHA512_Update(SHA512_CTX *sha, const void *data, size_t len);
+
+
+
+ int SHA512_Final(uint8_t *md, SHA512_CTX *sha);
+
+
+
+
+ uint8_t *SHA512(const uint8_t *data, size_t len, uint8_t *out);
+
+
+
+ void SHA512_Transform(SHA512_CTX *sha, const uint8_t *data);
+
+struct sha512_state_st {
+  uint64_t h[8];
+  uint64_t Nl, Nh;
+  union {
+    uint64_t d[16];
+    uint8_t p[128];
+  } u;
+  unsigned int num, md_len;
+};
+
+struct env_md_st {
+
+
+  int type;
+
+
+  unsigned md_size;
+
+
+  uint32_t flags;
+
+
+
+  int (*init)(EVP_MD_CTX *ctx);
+
+
+  int (*update)(EVP_MD_CTX *ctx, const void *data, size_t count);
+
+
+  int (*final)(EVP_MD_CTX *ctx, uint8_t *out);
+
+
+  unsigned block_size;
+
+
+  unsigned ctx_size;
+};
+
+
+
+
+struct evp_md_pctx_ops {
+
+
+  void (*free) (EVP_PKEY_CTX *pctx);
+
+
+
+  EVP_PKEY_CTX* (*dup) (EVP_PKEY_CTX *pctx);
+
+
+
+  int (*begin_digest) (EVP_MD_CTX *ctx);
+};
+
+
+static int md4_init(EVP_MD_CTX *ctx) { return MD4_Init(ctx->md_data); }
+
+static int md4_update(EVP_MD_CTX *ctx, const void *data, size_t count) {
+  return MD4_Update(ctx->md_data, data, count);
+}
+
+static int md4_final(EVP_MD_CTX *ctx, unsigned char *out) {
+  return MD4_Final(out, ctx->md_data);
+}
+
+static const EVP_MD md4_md = {
+    257, 16, 0 , md4_init,
+    md4_update, md4_final, 64 , sizeof(MD4_CTX),
+};
+
+const EVP_MD *EVP_md4(void) { return &md4_md; }
+
+
+static int md5_init(EVP_MD_CTX *ctx) { return MD5_Init(ctx->md_data); }
+
+static int md5_update(EVP_MD_CTX *ctx, const void *data, size_t count) {
+  return MD5_Update(ctx->md_data, data, count);
+}
+
+static int md5_final(EVP_MD_CTX *ctx, unsigned char *out) {
+  return MD5_Final(out, ctx->md_data);
+}
+
+static const EVP_MD md5_md = {
+    4, 16, 0 , md5_init,
+    md5_update, md5_final, 64 , sizeof(MD5_CTX),
+};
+
+const EVP_MD *EVP_md5(void) { return &md5_md; }
+
+
+static int sha1_init(EVP_MD_CTX *ctx) { return SHA1_Init(ctx->md_data); }
+
+static int sha1_update(EVP_MD_CTX *ctx, const void *data, size_t count) {
+  return SHA1_Update(ctx->md_data, data, count);
+}
+
+static int sha1_final(EVP_MD_CTX *ctx, unsigned char *md) {
+  return SHA1_Final(md, ctx->md_data);
+}
+
+static const EVP_MD sha1_md = {
+    64, 20, 0 , sha1_init,
+    sha1_update, sha1_final, 64 , sizeof(SHA_CTX),
+};
+
+const EVP_MD *EVP_sha1(void) { return &sha1_md; }
+
+
+static int sha224_init(EVP_MD_CTX *ctx) { return SHA224_Init(ctx->md_data); }
+
+static int sha224_update(EVP_MD_CTX *ctx, const void *data, size_t count) {
+  return SHA224_Update(ctx->md_data, data, count);
+}
+
+static int sha224_final(EVP_MD_CTX *ctx, unsigned char *md) {
+  return SHA224_Final(md, ctx->md_data);
+}
+
+static const EVP_MD sha224_md = {
+    675, 28, 0 ,
+    sha224_init, sha224_update, sha224_final,
+    64 , sizeof(SHA256_CTX),
+};
+
+const EVP_MD *EVP_sha224(void) { return &sha224_md; }
+
+
+static int sha256_init(EVP_MD_CTX *ctx) { return SHA256_Init(ctx->md_data); }
+
+static int sha256_update(EVP_MD_CTX *ctx, const void *data, size_t count) {
+  return SHA256_Update(ctx->md_data, data, count);
+}
+
+static int sha256_final(EVP_MD_CTX *ctx, unsigned char *md) {
+  return SHA256_Final(md, ctx->md_data);
+}
+
+static const EVP_MD sha256_md = {
+    672, 32, 0 ,
+    sha256_init, sha256_update, sha256_final,
+    64 , sizeof(SHA256_CTX),
+};
+
+const EVP_MD *EVP_sha256(void) { return &sha256_md; }
+
+
+static int sha384_init(EVP_MD_CTX *ctx) { return SHA384_Init(ctx->md_data); }
+
+static int sha384_update(EVP_MD_CTX *ctx, const void *data, size_t count) {
+  return SHA384_Update(ctx->md_data, data, count);
+}
+
+static int sha384_final(EVP_MD_CTX *ctx, unsigned char *md) {
+  return SHA384_Final(md, ctx->md_data);
+}
+
+static const EVP_MD sha384_md = {
+    673, 48, 0 ,
+    sha384_init, sha384_update, sha384_final,
+    128 , sizeof(SHA512_CTX),
+};
+
+const EVP_MD *EVP_sha384(void) { return &sha384_md; }
+
+
+static int sha512_init(EVP_MD_CTX *ctx) { return SHA512_Init(ctx->md_data); }
+
+static int sha512_update(EVP_MD_CTX *ctx, const void *data, size_t count) {
+  return SHA512_Update(ctx->md_data, data, count);
+}
+
+static int sha512_final(EVP_MD_CTX *ctx, unsigned char *md) {
+  return SHA512_Final(md, ctx->md_data);
+}
+
+static const EVP_MD sha512_md = {
+    674, 64, 0 ,
+    sha512_init, sha512_update, sha512_final,
+    128 , sizeof(SHA512_CTX),
+};
+
+const EVP_MD *EVP_sha512(void) { return &sha512_md; }
+
+
+typedef struct {
+  MD5_CTX md5;
+  SHA_CTX sha1;
+} MD5_SHA1_CTX;
+
+static int md5_sha1_init(EVP_MD_CTX *md_ctx) {
+  MD5_SHA1_CTX *ctx = md_ctx->md_data;
+  return MD5_Init(&ctx->md5) && SHA1_Init(&ctx->sha1);
+}
+
+static int md5_sha1_update(EVP_MD_CTX *md_ctx, const void *data, size_t count) {
+  MD5_SHA1_CTX *ctx = md_ctx->md_data;
+  return MD5_Update(&ctx->md5, data, count) && SHA1_Update(&ctx->sha1, data, count);
+}
+
+static int md5_sha1_final(EVP_MD_CTX *md_ctx, unsigned char *out) {
+  MD5_SHA1_CTX *ctx = md_ctx->md_data;
+  if (!MD5_Final(out, &ctx->md5) ||
+      !SHA1_Final(out + 16, &ctx->sha1)) {
+    return 0;
+  }
+  return 1;
+}
+
+static const EVP_MD md5_sha1_md = {
+    114,
+    16 + 20,
+    0 ,
+    md5_sha1_init,
+    md5_sha1_update,
+    md5_sha1_final,
+    64 ,
+    sizeof(MD5_SHA1_CTX),
+};
+
+const EVP_MD *EVP_md5_sha1(void) { return &md5_sha1_md; }
+
+
+struct nid_to_digest {
+  int nid;
+  const EVP_MD* (*md_func)(void);
+};
+
+static const struct nid_to_digest nid_to_digest_mapping[] = {
+  { 4, EVP_md5 },
+  { 64, EVP_sha1 },
+  { 675, EVP_sha224 },
+  { 672, EVP_sha256 },
+  { 673, EVP_sha384 },
+  { 674, EVP_sha512 },
+  { 114, EVP_md5_sha1 },
+  { 66, EVP_sha1 },
+  { 113, EVP_sha1 },
+  { 416, EVP_sha1 },
+  { 8, EVP_md5 },
+  { 65, EVP_sha1 },
+  { 671, EVP_sha224 },
+  { 668, EVP_sha256 },
+  { 669, EVP_sha384 },
+  { 670, EVP_sha512 },
+};
+
+const EVP_MD* EVP_get_digestbynid(int nid) {
+  unsigned i;
+
+  for (i = 0; i < sizeof(nid_to_digest_mapping) / sizeof(struct nid_to_digest);
+       i++) {
+    if (nid_to_digest_mapping[i].nid == nid) {
+      return nid_to_digest_mapping[i].md_func();
+    }
+  }
+
+  return 
+        ((void *)0)
+            ;
+}
+
+const EVP_MD* EVP_get_digestbyobj(const ASN1_OBJECT *obj) {
+  return EVP_get_digestbynid(OBJ_obj2nid(obj));
+}
diff --git a/test/clightgen/issue216.c b/test/clightgen/issue216.c
new file mode 100644
index 00000000..796b69b4
--- /dev/null
+++ b/test/clightgen/issue216.c
@@ -0,0 +1,5 @@
+#include <stddef.h>
+
+struct list {unsigned head; struct list *tail;};
+struct list three[] = { {1, three+1}, {2, three+2}, {3, NULL} };
+int f(int x) { return x;}
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 48e2b7b3..191a2285 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -1,7 +1,9 @@
 include ../../Makefile.config
 
 CCOMP=../../ccomp
-CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dparse -dc -dclight -dasm -fall
+CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime \
+ -dparse -dc -dclight -dasm -fall \
+ -DARCH_$(ARCH) -DMODEL_$(MODEL)
 INTERPFLAGS=-stdlib ../../runtime -interp -quiet -fall
 LIBS=$(LIBMATH)
 
@@ -20,18 +22,9 @@ TESTS=int32 int64 floats floats-basics \
 
 TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
   bitfields5 bitfields6 bitfields7 bitfields8 \
-  builtins-$(ARCH) packedstruct2 alignas \
+  builtins-$(ARCH) packedstruct1 packedstruct2 alignas \
   varargs1 varargs2 sections alias
 
-# packedstruct1 makes unaligned memory accesses
-
-ifeq ($(ARCH),powerpc)
-TESTS_COMP+=packedstruct1
-endif
-ifeq ($(ARCH),x86)
-TESTS_COMP+=packedstruct1
-endif
-
 # Can run, both in compiled mode and in interpreter mode,
 # but produce processor-dependent results, so no reference output in Results
 
@@ -70,12 +63,12 @@ clean:
 
 test:
 	@echo "----------- Compiled tests -------------"
-	@for i in $(TESTS) $(TESTS_COMP); do \
+	@set -e; for i in $(TESTS) $(TESTS_COMP); do \
 	   SIMU='$(SIMU)' ./Runtest $$i ./$$i.compcert; \
          done
 	@echo "----------- Interpreted tests -------------"
-	@for i in $(TESTS); do \
-           SIMU='' ./Runtest $$i $(CCOMP) $(INTERPFLAGS) $$i.c; \
+	@set -e; for i in $(TESTS); do \
+           SIMU='' INTERP=1 ./Runtest $$i $(CCOMP) $(INTERPFLAGS) $$i.c; \
          done
 	@for i in $(TESTS_DIFF); do \
            if $(CCOMP) -fall -interp -quiet $$i.c > _cinterp.log; then \
diff --git a/test/regression/Results/alignas b/test/regression/Results/alignas
index 581a4377..620b5e76 100644
--- a/test/regression/Results/alignas
+++ b/test/regression/Results/alignas
@@ -1,9 +1,10 @@
-a: size = 4, alignment = 16, address mod 16 = 0
-b: size = 12, alignment = 16, address mod 16 = 0
-bb: size = 12, alignment = 16, address mod 16 = 0
-c: size = 32, alignment = 16, address mod 16 = 0
-d: size = 32, alignment = 64, address mod 64 = 0
-e: size = 16, alignment = 16, address mod 16 = 0
-f: size = 16, alignment = 32, address mod 32 = 0
-g: size = 96, alignment = 16, address mod 16 = 0
-h: size = 192, alignment = 64, address mod 64 = 0
+a: size = 4, address mod 16 = 0
+b: size = 12, address mod 16 = 0
+bb: size = 12, address mod 16 = 0
+bbb: size = 12, address mod 16 = 0
+c: size = 32, address mod 16 = 0
+d: size = 32, address mod 64 = 0
+e: size = 16, address mod 16 = 0
+f: size = 16, address mod 32 = 0
+g: size = 96, address mod 16 = 0
+h: size = 192, address mod 64 = 0
diff --git a/test/regression/Results/bitfields9 b/test/regression/Results/bitfields9
index a1d0e9fd..e35c2414 100644
--- a/test/regression/Results/bitfields9
+++ b/test/regression/Results/bitfields9
@@ -1,10 +1,18 @@
 glob_s = { a = -12, b = 1 }
 glob_t = { c = 123, d = 1, e = -45 }
+glob_u_u = { u = -3 }
+glob_u_v = { v = 6 }
 loc_s = { a = 11, b = 2 }
 loc_t = { c = 11, d = 1, e = 2 }
+loc_u_u = { u = -5 }
+loc_u_v = { v = 3 }
 compound_s = { a = 2, b = 3 }
 compound_t = { c = 2, d = 1, e = -11 }
+compound_u = { u = 2 }
 loc_s = { a = 7, b = 2 }
 loc_t = { c = 7, d = 1, e = 50 }
+loc_u_u = { u = 7 }
+loc_u_v = { v = 2 }
 compound_s = { a = -14, b = 3 }
 compound_t = { c = 50, d = 1, e = -7 }
+compound_u = { u = 2 }
diff --git a/test/regression/Results/packedstruct1-32 b/test/regression/Results/packedstruct1-32
index e4bca769..e7d1c296 100644
--- a/test/regression/Results/packedstruct1-32
+++ b/test/regression/Results/packedstruct1-32
@@ -1,25 +1,37 @@
 sizeof(struct s1) = 14
+precomputed sizeof(struct s1) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s1 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s2) = 16
+precomputed sizeof(struct s2) = 16
 &s2 mod 16 = 0
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s2 = {x = 57, y = -456, z = 3.14159}
 
 sizeof(struct s3) = 31
+precomputed sizeof(struct s3) = 31
 offsetof(s) = 29
+precomputed offsetof(s) = 29
 s3 = {x = 123, y = 45678, z = 2147483649, v = -456, w = -1234567, p is ok, t = {111,222,333}, s = {'o','k'}}
 
 sizeof(struct s4) = 16
+precomputed sizeof(struct s4) = 16
 offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8
+precomputed offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8
 s4 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s5) = 14
+precomputed sizeof(struct s5) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s5 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s6) = 14
+precomputed sizeof(struct s6) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s62 = {x = 123, y = -456, z = 3.14159}
 
diff --git a/test/regression/Results/packedstruct1-64 b/test/regression/Results/packedstruct1-64
index c2a8bcd2..d255595f 100644
--- a/test/regression/Results/packedstruct1-64
+++ b/test/regression/Results/packedstruct1-64
@@ -1,25 +1,37 @@
 sizeof(struct s1) = 14
+precomputed sizeof(struct s1) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s1 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s2) = 16
+precomputed sizeof(struct s2) = 16
 &s2 mod 16 = 0
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s2 = {x = 57, y = -456, z = 3.14159}
 
 sizeof(struct s3) = 35
+precomputed sizeof(struct s3) = 35
 offsetof(s) = 33
+precomputed offsetof(s) = 33
 s3 = {x = 123, y = 45678, z = 2147483649, v = -456, w = -1234567, p is ok, t = {111,222,333}, s = {'o','k'}}
 
 sizeof(struct s4) = 16
+precomputed sizeof(struct s4) = 16
 offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8
+precomputed offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8
 s4 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s5) = 14
+precomputed sizeof(struct s5) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s5 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s6) = 14
+precomputed sizeof(struct s6) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s62 = {x = 123, y = -456, z = 3.14159}
 
diff --git a/test/regression/Runtest b/test/regression/Runtest
index ad2a58f1..f693219a 100755
--- a/test/regression/Runtest
+++ b/test/regression/Runtest
@@ -9,6 +9,9 @@ out="test$$.log"
 rm -f $out
 trap "rm -f $out" 0 INT QUIT
 
+# Is the test expected to fail?
+expect_fail=false
+
 # The architecture and the bitsize
 arch=`sed -n -e 's/^ARCH=//p' ../../Makefile.config`
 bits=`sed -n -e 's/^BITSIZE=//p' ../../Makefile.config`
@@ -26,10 +29,23 @@ else
   ref=""
 fi
 
+# Special conditions
+
+if test -f "$name.cond"; then
+  RUN=0 SKIP=1 EXPECT_FAIL=2 sh "$name.cond"
+  case "$?" in
+    1) echo "$name: skipped"; exit 0;;
+    2) expect_fail=true;;
+  esac
+fi
+
 # Administer the test
 if $SIMU $* > $out
 then
-  if test -n "$ref"; then
+  if $expect_fail; then
+    echo "$name: ERROR (should have failed but did not)"
+    exit 2
+  elif test -n "$ref"; then
     if cmp -s "$out" "$ref"; then
       echo "$name: passed"
       exit 0
@@ -43,7 +59,13 @@ then
     exit 0
   fi
 else
-  echo "$name: EXECUTION FAILED (status $?)"
-  exit 2
+  retcode=$?
+  if $expect_fail; then
+    echo "$name: passed (failed as expected)"
+    exit 0
+  else
+    echo "$name: EXECUTION FAILED (status $retcode)"
+    exit 2
+  fi
 fi
 
diff --git a/test/regression/alignas.c b/test/regression/alignas.c
index b3754039..777c13a5 100644
--- a/test/regression/alignas.c
+++ b/test/regression/alignas.c
@@ -2,16 +2,12 @@
 
 #include <stdio.h>
 
-#if  __STDC_VERSION__ < 201100 && defined(__GNUC__)
-#define _Alignas(x) __attribute__((aligned(x)))
-#define _Alignof(x) __alignof__(x)
-#endif
-
 #ifdef _Alignas
 #undef _Alignas
 #endif
-#ifdef _Alignof
-#undef _Alignof
+
+#if  __STDC_VERSION__ < 201100 && defined(__GNUC__)
+#define _Alignas(x) __attribute((aligned(x)))
 #endif
 
 /* Base type */
@@ -24,10 +20,9 @@ _Alignas(16) int b[3];
 typedef int int3[3];
 _Alignas(16) int3 bb;
 
-#if 0
-typedef _Alignas(16) int int16;
+/* _Alignas is not allowed in typedefs but the "aligned" attribute is */
+typedef __attribute((aligned(16))) int int16;
 int16 bbb[3];
-#endif
 
 char filler2;
 
@@ -72,28 +67,26 @@ char filler8;
 
 int main()
 {
-  printf("a: size = %u, alignment = %u, address mod 16 = %u\n",
-         (unsigned) sizeof(a), (unsigned) _Alignof(a), ((unsigned) &a) & 0xF);
-  printf("b: size = %u, alignment = %u, address mod 16 = %u\n",
-         (unsigned) sizeof(b), (unsigned) _Alignof(b), ((unsigned) &b) & 0xF);
-  printf("bb: size = %u, alignment = %u, address mod 16 = %u\n",
-         (unsigned) sizeof(bb), (unsigned) _Alignof(bb), ((unsigned) &bb) & 0xF);
-#if 0
-  printf("bbb: size = %u, alignment = %u, address mod 16 = %u\n",
-         (unsigned) sizeof(bbb), (unsigned) _Alignof(bbb), ((unsigned) &bbb) & 0xF);
-#endif
-  printf("c: size = %u, alignment = %u, address mod 16 = %u\n",
-         (unsigned) sizeof(c), (unsigned) _Alignof(c), ((unsigned) &c) & 0xF);
-  printf("d: size = %u, alignment = %u, address mod 64 = %u\n",
-         (unsigned) sizeof(d), (unsigned) _Alignof(d), ((unsigned) &d) & 0x3F);
-  printf("e: size = %u, alignment = %u, address mod 16 = %u\n",
-         (unsigned) sizeof(e), (unsigned) _Alignof(e), ((unsigned) &e) & 0xF);
-  printf("f: size = %u, alignment = %u, address mod 32 = %u\n",
-         (unsigned) sizeof(f), (unsigned) _Alignof(f), ((unsigned) &f) & 0x1F);
-  printf("g: size = %u, alignment = %u, address mod 16 = %u\n",
-         (unsigned) sizeof(g), (unsigned) _Alignof(g), ((unsigned) &g) & 0xF);
-  printf("h: size = %u, alignment = %u, address mod 64 = %u\n",
-         (unsigned) sizeof(h), (unsigned) _Alignof(h), ((unsigned) &h) & 0x3F);
+  printf("a: size = %u, address mod 16 = %u\n",
+         (unsigned) sizeof(a), ((unsigned) &a) & 0xF);
+  printf("b: size = %u, address mod 16 = %u\n",
+         (unsigned) sizeof(b), ((unsigned) &b) & 0xF);
+  printf("bb: size = %u, address mod 16 = %u\n",
+         (unsigned) sizeof(bb), ((unsigned) &bb) & 0xF);
+  printf("bbb: size = %u, address mod 16 = %u\n",
+         (unsigned) sizeof(bbb), ((unsigned) &bbb) & 0xF);
+  printf("c: size = %u, address mod 16 = %u\n",
+         (unsigned) sizeof(c), ((unsigned) &c) & 0xF);
+  printf("d: size = %u, address mod 64 = %u\n",
+         (unsigned) sizeof(d), ((unsigned) &d) & 0x3F);
+  printf("e: size = %u, address mod 16 = %u\n",
+         (unsigned) sizeof(e), ((unsigned) &e) & 0xF);
+  printf("f: size = %u, address mod 32 = %u\n",
+         (unsigned) sizeof(f), ((unsigned) &f) & 0x1F);
+  printf("g: size = %u, address mod 16 = %u\n",
+         (unsigned) sizeof(g), ((unsigned) &g) & 0xF);
+  printf("h: size = %u, address mod 64 = %u\n",
+         (unsigned) sizeof(h), ((unsigned) &h) & 0x3F);
   return 0;
 }
 
diff --git a/test/regression/bitfields9.c b/test/regression/bitfields9.c
index be87057b..eef20168 100644
--- a/test/regression/bitfields9.c
+++ b/test/regression/bitfields9.c
@@ -11,6 +11,12 @@ struct t {
   unsigned int c: 16;
   _Bool d: 1;
   short e: 8;
+  int : 10;
+};
+
+union u {
+  int u: 4;
+  unsigned int v: 3;
 };
 
 void print_s(char * msg, struct s p)
@@ -23,25 +29,45 @@ void print_t(char * msg, struct t p)
   printf("%s = { c = %d, d = %d, e = %d }\n", msg, p.c, p.d, p.e);
 }
 
+void print_u_u(char * msg, union u p)
+{
+  printf("%s = { u = %d }\n", msg, p.u);
+}
+
+void print_u_v(char * msg, union u p)
+{
+  printf("%s = { v = %u }\n", msg, p.v);
+}
+
+
 /* Global initialization */
 struct s glob_s = { -12, 1 };
 struct t glob_t = { 123, 2, -45 };
+union u glob_u_u = { -3 };
+union u glob_u_v = { .v = 6 };
 
 /* Local initialization */
 void f(int x, int y, int z)
 {
   struct s loc_s = { x, y };
   struct t loc_t = { x, z, y };
+  union u loc_u_u = { .u = x };
+  union u loc_u_v = { .v = z };
   print_s("loc_s", loc_s);
   print_t("loc_t", loc_t);
+  print_u_u("loc_u_u", loc_u_u);
+  print_u_v("loc_u_v", loc_u_v);
   print_s("compound_s", (struct s) { y, x });
   print_t("compound_t", (struct t) { y, ~z, -x });
+  print_u_u("compound_u", (union u) { y });
 }
 
 int main()
 {
   print_s("glob_s", glob_s);
   print_t("glob_t", glob_t);
+  print_u_u("glob_u_u", glob_u_u);
+  print_u_v("glob_u_v", glob_u_v);
   f(11, 2, 3);
   f(7, 50, 2);
   return 0;
diff --git a/test/regression/extasm.c b/test/regression/extasm.c
index a41c4202..babc57f1 100644
--- a/test/regression/extasm.c
+++ b/test/regression/extasm.c
@@ -18,7 +18,10 @@ int clobbers(int x, int z)
   return y + z;
 }
 
-#if defined(__x86_64__) || __riscv_xlen == 64
+#if (defined(ARCH_x86) && defined(MODEL_64)) \
+ || (defined(ARCH_riscV) && defined(MODEL_64)) \
+ || (defined(ARCH_powerpc) && defined(MODEL_ppc64)) \
+ || (defined(ARCH_powerpc) && defined(MODEL_e5500))
 #define SIXTYFOUR
 #else
 #undef SIXTYFOUR
diff --git a/test/regression/funptr2.cond b/test/regression/funptr2.cond
new file mode 100644
index 00000000..ab460efb
--- /dev/null
+++ b/test/regression/funptr2.cond
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if test -n "$INTERP"
+then exit $EXPECT_FAIL
+else exit $RUN
+fi
diff --git a/test/regression/interop1.cond b/test/regression/interop1.cond
new file mode 100644
index 00000000..77904189
--- /dev/null
+++ b/test/regression/interop1.cond
@@ -0,0 +1,10 @@
+#!/bin/sh
+arch=`sed -n -e 's/^ARCH=//p' ../../Makefile.config`
+model=`sed -n -e 's/^MODEL=//p' ../../Makefile.config`
+system=`sed -n -e 's/^SYSTEM=//p' ../../Makefile.config`
+
+case "$arch,$model,$system" in
+  *,*,cygwin)  exit $SKIP;;
+  x86,32sse2,*|arm,*,*|powerpc,*,*)  exit $RUN;;
+  *) exit $SKIP;;
+esac
diff --git a/test/regression/packedstruct1.c b/test/regression/packedstruct1.c
index 8b138dd4..5d3e7124 100644
--- a/test/regression/packedstruct1.c
+++ b/test/regression/packedstruct1.c
@@ -2,8 +2,18 @@
 
 #include <stdio.h>
 
+/* offsetof is the offset computed by the verified front-end (cfrontend/) */
 #define offsetof(s,f) (int)&(((struct s *)0)->f)
 
+/* boffsetof is the offset computed by the elaborator (cparser/) */
+#define boffsetof(s,f) (int)__builtin_offsetof(struct s, f)
+
+/* szof is the size computed by the verified front-end (cfrontend/) */
+#define szof(s) (int) sizeof(struct s)
+
+/* bszof is the size computed by the elaborator (cparser/) */
+#define bszof(s) (int) sizeof(char [sizeof(struct s)])
+
 /* Simple packing */
 
 struct __packed__(1) s1 { unsigned short x; int y; double z; };
@@ -11,9 +21,12 @@ struct __packed__(1) s1 { unsigned short x; int y; double z; };
 void test1(void)
 {
   struct s1 s1;
-  printf("sizeof(struct s1) = %d\n", sizeof(struct s1));
+  printf("sizeof(struct s1) = %d\n", szof(s1));
+  printf("precomputed sizeof(struct s1) = %d\n", bszof(s1));
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s1,x), offsetof(s1,y), offsetof(s1,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s1,x), boffsetof(s1,y), boffsetof(s1,z));
   s1.x = 123; s1.y = -456; s1.z = 3.14159;
   printf("s1 = {x = %d, y = %d, z = %.5f}\n\n", s1.x, s1.y, s1.z);
 }
@@ -28,10 +41,13 @@ struct s2 s2;
 
 void test2(void)
 {
-  printf("sizeof(struct s2) = %d\n", sizeof(struct s2));
+  printf("sizeof(struct s2) = %d\n", szof(s2));
+  printf("precomputed sizeof(struct s2) = %d\n", bszof(s2));
   printf("&s2 mod 16 = %d\n", ((int) &s2) & 0xF);
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s2,x), offsetof(s2,y), offsetof(s2,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s2,x), boffsetof(s2,y), boffsetof(s2,z));
   s2.x = 12345; s2.y = -456; s2.z = 3.14159;
   printf("s2 = {x = %d, y = %d, z = %.5f}\n\n", s2.x, s2.y, s2.z);
 }
@@ -55,8 +71,10 @@ void test3(void)
 {
   char xx;
 
-  printf("sizeof(struct s3) = %d\n", sizeof(struct s3));
+  printf("sizeof(struct s3) = %d\n", szof(s3));
+  printf("precomputed sizeof(struct s3) = %d\n", bszof(s3));
   printf("offsetof(s) = %d\n", offsetof(s3,s));
+  printf("precomputed offsetof(s) = %d\n", boffsetof(s3,s));
   s3.x = 123;
   s3.y = 45678;
   s3.z = 0x80000001U;
@@ -82,9 +100,13 @@ struct s4 { unsigned short x; int y; double z; };
 void test4(void)
 {
   struct s4 s4;
-  printf("sizeof(struct s4) = %d\n", sizeof(struct s4));
+
+  printf("sizeof(struct s4) = %d\n", szof(s4));
+  printf("precomputed sizeof(struct s4) = %d\n", bszof(s4));
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s4,x), offsetof(s4,y), offsetof(s4,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s4,x), boffsetof(s4,y), boffsetof(s4,z));
   s4.x = 123; s4.y = -456; s4.z = 3.14159;
   printf("s4 = {x = %d, y = %d, z = %.5f}\n\n", s4.x, s4.y, s4.z);
 }
@@ -96,9 +118,13 @@ struct __attribute((packed)) s5 { unsigned short x; int y; double z; };
 void test5(void)
 {
   struct s5 s5;
-  printf("sizeof(struct s5) = %d\n", sizeof(struct s5));
+
+  printf("sizeof(struct s5) = %d\n", szof(s5));
+  printf("precomputed sizeof(struct s5) = %d\n", bszof(s5));
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s5,x), offsetof(s5,y), offsetof(s5,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s5,x), boffsetof(s5,y), boffsetof(s5,z));
   s5.x = 123; s5.y = -456; s5.z = 3.14159;
   printf("s5 = {x = %d, y = %d, z = %.5f}\n\n", s5.x, s5.y, s5.z);
 }
@@ -110,9 +136,13 @@ struct s6 { unsigned short x; int y; double z; }  __attribute((packed)) const s6
 void test6(void)
 {
   struct s6 s62;
-  printf("sizeof(struct s6) = %d\n", sizeof(struct s6));
+
+  printf("sizeof(struct s6) = %d\n", szof(s6));
+  printf("precomputed sizeof(struct s6) = %d\n", bszof(s6));
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s6,x), offsetof(s6,y), offsetof(s6,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s6,x), boffsetof(s6,y), boffsetof(s6,z));
   s62.x = 123; s62.y = -456; s62.z = 3.14159;
   printf("s62 = {x = %d, y = %d, z = %.5f}\n\n", s62.x, s62.y, s62.z);
 }