Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

1 files changed, 27 insertions, 0 deletions

diff --git a/test/monniaux/k1_builtins/execute_code.c b/test/monniaux/k1_builtins/execute_code.c
new file mode 100644
index 00000000..58580ed9
--- /dev/null
+++ b/test/monniaux/k1_builtins/execute_code.c
@@ -0,0 +1,27 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+typedef int fun_type(int x);
+
+int poulet(int x) {
+  return x*2;
+}
+
+int canard(int x) {
+  return x*3;
+}
+
+#define SIZE 1024
+int main() {
+  void *buf=malloc(SIZE);
+  memcpy(buf, poulet, SIZE);
+  int rpoulet = (*((fun_type*) buf))(33);
+  memcpy(buf, canard, SIZE);
+  int rcanard = (*((fun_type*) buf))(33);
+  __builtin_k1_iinval();
+  int rcanard2 = (*((fun_type*) buf))(33);
+  free(buf);
+  printf("%d %d %d\n", rpoulet, rcanard, rcanard2);
+  return 0;
+}