Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass

1 files changed, 23 insertions, 0 deletions

diff --git a/test/monniaux/reduced_picosat/reduced_picosat.c b/test/monniaux/reduced_picosat/reduced_picosat.c
new file mode 100644
index 00000000..eb9fdaf8
--- /dev/null
+++ b/test/monniaux/reduced_picosat/reduced_picosat.c
@@ -0,0 +1,23 @@
+typedef struct b b;
+b *a;
+struct b {
+  int c;
+  int d, **clshead;
+  int **ahead;
+  unsigned h;
+} glob;
+int k();
+int main() {
+  a = &glob;
+  k(a);
+}
+#define e(f) f - g->c
+static void m(b *g, int *l) {
+  if (g)
+    *g->ahead = l;
+}
+int k(b *g) {
+  if (g->d)
+    m(g, e(g->clshead[-1]));
+  return g->h;
+}