aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/reduced_picosat/reduced_picosat.c
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-12-02 12:25:31 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-12-02 12:25:31 +0100
commit73a83b969dbb6f4c419ebdcc663f463509b6d6e3 (patch)
tree259852cd3272f2f31a09d75ac24e31ec1aaa8d9e /test/monniaux/reduced_picosat/reduced_picosat.c
parent3570ba2827908b280315c922ba7e43289f6d802a (diff)
parent035a1a9f4b636206acbae4506c5fc4ef322de0c1 (diff)
downloadcompcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.tar.gz
compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.zip
Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3
Diffstat (limited to 'test/monniaux/reduced_picosat/reduced_picosat.c')
-rw-r--r--test/monniaux/reduced_picosat/reduced_picosat.c23
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;
+}