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

6 files changed, 596 insertions, 0 deletions

diff --git a/test/monniaux/lustrev4_lustrec_heater_control/Makefile b/test/monniaux/lustrev4_lustrec_heater_control/Makefile
new file mode 100644
index 00000000..df7c9e0a
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/Makefile
@@ -0,0 +1,3 @@
+TARGET=lustrec_heater_control
+
+include ../rules.mk
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/arrow.h b/test/monniaux/lustrev4_lustrec_heater_control/arrow.h
new file mode 100644
index 00000000..802057da
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/arrow.h
@@ -0,0 +1,34 @@
+
+#ifndef _ARROW
+#define _ARROW
+
+struct _arrow_mem {struct _arrow_reg {_Bool _first; } _reg; };
+
+extern struct _arrow_mem *_arrow_alloc ();
+
+extern void _arrow_dealloc (struct _arrow_mem *);
+
+#define _arrow_DECLARE(attr, inst)\
+  attr struct _arrow_mem inst;
+  
+#define _arrow_LINK(inst) do {\
+  ;\
+} while (0)
+
+#define _arrow_ALLOC(attr, inst)\
+  _arrow_DECLARE(attr, inst);\
+  _arrow_LINK(inst)
+
+#define _arrow_init(self) {}
+
+#define _arrow_clear(self) {}
+
+#define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y))
+
+#define _arrow_reset(self) {(self)->_reg._first = 1;}
+
+/* Step macro for specialized arrows of the form: (true -> false) */
+
+#define _once_step(output,self) { *output = (self)->_reg._first; if ((self)->_reg._first) { (self)->_reg._first=0; }; }
+
+#endif
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c
new file mode 100644
index 00000000..6025cd13
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c
@@ -0,0 +1,342 @@
+#include <assert.h>
+#include "heater_control.h"
+
+/* C code generated by lustrec
+   Version number 1.6-@GITBRANCH@
+   Code is C99 compliant
+   Using (double) floating-point numbers */
+   
+/* Import dependencies */
+
+/* Global constants (definitions) */
+double FAILURE = -999.0;
+double TMIN = 6.0;
+double TMAX = 9.0;
+double DELTA = 0.5;
+
+/* Struct definitions */
+struct not_a_sauna2_mem {struct not_a_sauna2_reg {double __not_a_sauna2_2;
+                                                  } _reg; 
+                         struct _arrow_mem *ni_0;
+                         };
+struct heater_control_mem {struct heater_control_reg {_Bool __heater_control_16;
+                                                      } _reg; 
+                           struct _arrow_mem *ni_1;
+                           };
+struct not_a_sauna_mem {struct not_a_sauna_reg {double __not_a_sauna_2;
+                                                } _reg; 
+                        struct _arrow_mem *ni_2;
+                        };
+
+
+void not_a_sauna2_reset (struct not_a_sauna2_mem *self) {
+  
+  _arrow_reset(self->ni_0);
+  return;
+}
+
+void not_a_sauna2_step (double T, double T1, double T2, double T3,
+                        _Bool Heat_on, 
+                        _Bool (*ok),
+                        struct not_a_sauna2_mem *self) {
+  _Bool __not_a_sauna2_1;
+  
+  
+  _arrow_step (1, 0, &__not_a_sauna2_1, self->ni_0);
+  if (__not_a_sauna2_1) {
+    *ok = 1;
+  } else {
+    *ok = (self->_reg.__not_a_sauna2_2 < (9.0 - 6.0));
+  }
+  self->_reg.__not_a_sauna2_2 = T;
+  
+  return;
+}
+
+void heater_control_reset (struct heater_control_mem *self) {
+  
+  _arrow_reset(self->ni_1);
+  return;
+}
+
+void heater_control_step (double T, double T1, double T2, double T3, 
+                          _Bool (*Heat_on),
+                          struct heater_control_mem *self) {
+  double Median_42_max2_150_m;
+  double Median_42_max2_152_m;
+  double Median_42_min2_141_m;
+  double Median_42_min2_143_m;
+  double Median_52_max2_150_m;
+  double Median_52_max2_152_m;
+  double Median_52_min2_141_m;
+  double Median_52_min2_143_m;
+  double Tguess;
+  _Bool V12;
+  _Bool V13;
+  _Bool V23;
+  _Bool __heater_control_12;
+  double abs_15_a;
+  double abs_15_v;
+  double abs_23_a;
+  double abs_23_v;
+  double abs_7_a;
+  double abs_7_v;
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  abs_7_v = (T1 - T2);
+  if ((abs_7_v >= 0.0)) {
+    abs_7_a = abs_7_v;
+  } else {
+    abs_7_a = (- abs_7_v);
+  }
+  abs_23_v = (T2 - T3);
+  if ((abs_23_v >= 0.0)) {
+    abs_23_a = abs_23_v;
+  } else {
+    abs_23_a = (- abs_23_v);
+  }
+  abs_15_v = (T1 - T3);
+  if ((abs_15_v >= 0.0)) {
+    abs_15_a = abs_15_v;
+  } else {
+    abs_15_a = (- abs_15_v);
+  }
+  V23 = (abs_23_a < 0.5);
+  V13 = (abs_15_a < 0.5);
+  V12 = (abs_7_a < 0.5);
+  if ((T2 < T3)) {
+    Median_52_min2_141_m = T2;
+  } else {
+    Median_52_min2_141_m = T3;
+  }
+  if ((T2 > T3)) {
+    Median_42_max2_150_m = T2;
+  } else {
+    Median_42_max2_150_m = T3;
+  }
+  if ((T2 < T3)) {
+    Median_42_min2_141_m = T2;
+  } else {
+    Median_42_min2_141_m = T3;
+  }
+  if ((T2 > T3)) {
+    Median_52_max2_150_m = T2;
+  } else {
+    Median_52_max2_150_m = T3;
+  }
+  if ((T1 < Median_52_min2_141_m)) {
+    Median_52_min2_143_m = T1;
+  } else {
+    Median_52_min2_143_m = Median_52_min2_141_m;
+  }
+  if ((T1 > Median_52_max2_150_m)) {
+    Median_52_max2_152_m = T1;
+  } else {
+    Median_52_max2_152_m = Median_52_max2_150_m;
+  }
+  if ((T1 < Median_42_min2_141_m)) {
+    Median_42_min2_143_m = T1;
+  } else {
+    Median_42_min2_143_m = Median_42_min2_141_m;
+  }
+  if ((T1 > Median_42_max2_150_m)) {
+    Median_42_max2_152_m = T1;
+  } else {
+    Median_42_max2_152_m = Median_42_max2_150_m;
+  }
+  if ((((!V12) && (!V13)) && (!V23))) {
+    Tguess = -999.0;
+  } else {
+    if (((((V12 && (!V13)) && (!V23)) || ((V13 && (!V12)) && (!V23))) || ((V23 && (!V12)) && (!V13)))) {
+      Tguess = ((((T1 + T2) + T3) - Median_42_min2_143_m) - Median_42_max2_152_m);
+    } else {
+      if (((V12 && V13) && V23)) {
+        Tguess = ((((T1 + T2) + T3) - Median_52_min2_143_m) - Median_52_max2_152_m);
+      } else {
+        if (V12) {
+          Tguess = ((T1 + T2) / 2.0);
+        } else {
+          if (V13) {
+            Tguess = ((T1 + T3) / 2.0);
+          } else {
+            Tguess = ((T2 + T3) / 2.0);
+          }
+        }
+      }
+    }
+  }
+  _arrow_step (1, 0, &__heater_control_12, self->ni_1);
+  if (__heater_control_12) {
+    *Heat_on = 1;
+  } else {
+    if ((Tguess == -999.0)) {
+      *Heat_on = 0;
+    } else {
+      if ((Tguess < 6.0)) {
+        *Heat_on = 1;
+      } else {
+        if ((Tguess > 9.0)) {
+          *Heat_on = 0;
+        } else {
+          *Heat_on = self->_reg.__heater_control_16;
+        }
+      }
+    }
+  }
+  self->_reg.__heater_control_16 = *Heat_on;
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  
+  return;
+}
+
+void not_a_sauna_reset (struct not_a_sauna_mem *self) {
+  
+  _arrow_reset(self->ni_2);
+  return;
+}
+
+void not_a_sauna_step (double T, double T1, double T2, double T3,
+                       _Bool Heat_on, 
+                       _Bool (*ok),
+                       struct not_a_sauna_mem *self) {
+  _Bool __not_a_sauna_1;
+  
+  
+  _arrow_step (1, 0, &__not_a_sauna_1, self->ni_2);
+  if (__not_a_sauna_1) {
+    *ok = 1;
+  } else {
+    *ok = (self->_reg.__not_a_sauna_2 < (9.0 + 1.0));
+  }
+  self->_reg.__not_a_sauna_2 = T;
+  
+  return;
+}
+
+void oneoftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                     _Bool (*r)
+                     ) {
+  
+  *r = ((((f1 && (!f2)) && (!f3)) || ((f2 && (!f1)) && (!f3))) || ((f3 && (!f1)) && (!f2)));
+  return;
+}
+
+void noneoftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                      _Bool (*r)
+                      ) {
+  
+  *r = (((!f1) && (!f2)) && (!f3));
+  return;
+}
+
+void alloftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                     _Bool (*r)
+                     ) {
+  
+  *r = ((f1 && f2) && f3);
+  return;
+}
+
+void abs_step (double v, 
+               double (*a)
+               ) {
+  
+  if ((v >= 0.0)) {
+    *a = v;
+  } else {
+    *a = (- v);
+  }
+  return;
+}
+
+void Median_step (double a, double b, double c, 
+                  double (*z)
+                  ) {
+  double __Median_1;
+  double __Median_2;
+  double __Median_3;
+  double __Median_4;
+  
+  
+  
+  
+  
+  min2_step (b, c, &__Median_3);
+  min2_step (a, __Median_3, &__Median_4);
+  max2_step (b, c, &__Median_1);
+  max2_step (a, __Median_1, &__Median_2);
+  *z = ((((a + b) + c) - __Median_4) - __Median_2);
+  
+  
+  
+  
+  return;
+}
+
+void Average_step (double a, double b, 
+                   double (*z)
+                   ) {
+  
+  *z = ((a + b) / 2.0);
+  return;
+}
+
+void min2_step (double one, double two, 
+                double (*m)
+                ) {
+  
+  if ((one < two)) {
+    *m = one;
+  } else {
+    *m = two;
+  }
+  return;
+}
+
+void max2_step (double one, double two, 
+                double (*m)
+                ) {
+  
+  if ((one > two)) {
+    *m = one;
+  } else {
+    *m = two;
+  }
+  return;
+}
+
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h
new file mode 100644
index 00000000..405f9a74
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h
@@ -0,0 +1,96 @@
+/* C code generated by lustrec
+   Version number 1.6-@GITBRANCH@
+   Code is C99 compliant
+   Using (double) floating-point numbers */
+   
+#ifndef _HEATER_CONTROL
+#define _HEATER_CONTROL
+
+/* Imports standard library */
+#include <stdint.h>
+#include "arrow.h"
+
+
+/* Import dependencies */
+
+/* Types definitions */
+
+/* Global constant (declarations, definitions are in C file) */
+extern double FAILURE;
+extern double TMIN;
+extern double TMAX;
+extern double DELTA;
+
+/* Structs declarations */
+struct not_a_sauna2_mem;
+struct heater_control_mem;
+struct not_a_sauna_mem;
+
+/* Nodes declarations */
+extern void not_a_sauna2_reset (struct not_a_sauna2_mem *self);
+
+extern void not_a_sauna2_init (struct not_a_sauna2_mem *self);
+
+extern void not_a_sauna2_clear (struct not_a_sauna2_mem *self);
+
+extern void not_a_sauna2_step (double T, double T1, double T2, double T3,
+                               _Bool Heat_on, 
+                               _Bool (*ok),
+                               struct not_a_sauna2_mem *self);
+
+extern void heater_control_reset (struct heater_control_mem *self);
+
+extern void heater_control_init (struct heater_control_mem *self);
+
+extern void heater_control_clear (struct heater_control_mem *self);
+
+extern void heater_control_step (double T, double T1, double T2, double T3, 
+                                 _Bool (*Heat_on),
+                                 struct heater_control_mem *self);
+
+extern void not_a_sauna_reset (struct not_a_sauna_mem *self);
+
+extern void not_a_sauna_init (struct not_a_sauna_mem *self);
+
+extern void not_a_sauna_clear (struct not_a_sauna_mem *self);
+
+extern void not_a_sauna_step (double T, double T1, double T2, double T3,
+                              _Bool Heat_on, 
+                              _Bool (*ok),
+                              struct not_a_sauna_mem *self);
+
+extern void oneoftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                            _Bool (*r)
+                            );
+
+extern void noneoftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                             _Bool (*r)
+                             );
+
+extern void alloftree_step (_Bool f1, _Bool f2, _Bool f3, 
+                            _Bool (*r)
+                            );
+
+extern void abs_step (double v, 
+                      double (*a)
+                      );
+
+extern void Median_step (double a, double b, double c, 
+                         double (*z)
+                         );
+
+extern void Average_step (double a, double b, 
+                          double (*z)
+                          );
+
+extern void min2_step (double one, double two, 
+                       double (*m)
+                       );
+
+extern void max2_step (double one, double two, 
+                       double (*m)
+                       );
+
+
+#endif
+
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h
new file mode 100644
index 00000000..270ed4a3
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h
@@ -0,0 +1,73 @@
+/* C code generated by lustrec
+   Version number 1.6-@GITBRANCH@
+   Code is C99 compliant
+   Using (double) floating-point numbers */
+   
+#ifndef _HEATER_CONTROL_alloc
+#define _HEATER_CONTROL_alloc
+
+/* Import header from heater_control */
+#include "heater_control.h"
+
+/* Import dependencies */
+
+/* Struct definitions */
+struct not_a_sauna2_mem {struct not_a_sauna2_reg {double __not_a_sauna2_2;
+                                                  } _reg; 
+                         struct _arrow_mem *ni_0;
+                         };
+struct heater_control_mem {struct heater_control_reg {_Bool __heater_control_16;
+                                                      } _reg; 
+                           struct _arrow_mem *ni_1;
+                           };
+struct not_a_sauna_mem {struct not_a_sauna_reg {double __not_a_sauna_2;
+                                                } _reg; 
+                        struct _arrow_mem *ni_2;
+                        };
+
+/* Node allocation function/macro prototypes */
+#define not_a_sauna2_DECLARE(attr, inst)\
+  attr struct not_a_sauna2_mem inst;\
+  _arrow_DECLARE(attr, inst ## _ni_0);
+  
+#define not_a_sauna2_LINK(inst) do {\
+  _arrow_LINK(inst ## _ni_0);\
+  inst.ni_0 = &inst ## _ni_0;\
+} while (0)
+
+#define not_a_sauna2_ALLOC(attr, inst)\
+  not_a_sauna2_DECLARE(attr, inst);\
+  not_a_sauna2_LINK(inst);
+
+
+#define heater_control_DECLARE(attr, inst)\
+  attr struct heater_control_mem inst;\
+  _arrow_DECLARE(attr, inst ## _ni_1);
+  
+#define heater_control_LINK(inst) do {\
+  _arrow_LINK(inst ## _ni_1);\
+  inst.ni_1 = &inst ## _ni_1;\
+} while (0)
+
+#define heater_control_ALLOC(attr, inst)\
+  heater_control_DECLARE(attr, inst);\
+  heater_control_LINK(inst);
+
+
+#define not_a_sauna_DECLARE(attr, inst)\
+  attr struct not_a_sauna_mem inst;\
+  _arrow_DECLARE(attr, inst ## _ni_2);
+  
+#define not_a_sauna_LINK(inst) do {\
+  _arrow_LINK(inst ## _ni_2);\
+  inst.ni_2 = &inst ## _ni_2;\
+} while (0)
+
+#define not_a_sauna_ALLOC(attr, inst)\
+  not_a_sauna_DECLARE(attr, inst);\
+  not_a_sauna_LINK(inst);
+
+
+
+#endif
+
diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c
new file mode 100644
index 00000000..d0298840
--- /dev/null
+++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c
@@ -0,0 +1,48 @@
+#include <stdio.h>
+#include <unistd.h>
+#include <stdlib.h>
+#include <assert.h>
+#include "heater_control_alloc.h"
+#include "../clock.h"
+#include "../dm_random.c"
+
+static double _get_double(void) {
+  return (dm_random_uint32()%70000U) * 1E-3 -20.0;
+}
+
+static void _put_bool(const char *name, _Bool b) {
+  printf("%s: %d\n", name, b);
+}
+
+/* C code generated by lustrec
+   Version number 1.6-@GITBRANCH@
+   Code is C99 compliant
+   Using (double) floating-point numbers */
+   
+int main (int argc, char *argv[]) {
+  
+  /* Main memory allocation */
+  heater_control_ALLOC(static,main_mem);
+
+  clock_prepare();
+  clock_start();
+  
+  /* Initialize the main memory */
+  heater_control_reset(&main_mem);
+  
+  /* Infinite loop */
+  for(int loop_count=0; loop_count<1000; loop_count++){
+    double T = _get_double();
+    double T1 = _get_double();
+    double T2 = _get_double();
+    double T3 = _get_double();
+    _Bool Heat_on;
+    heater_control_step (T, T1, T2, T3, &Heat_on, &main_mem);
+    // _put_bool("Heat_on", Heat_on);
+  }
+  
+  clock_stop();
+  print_total_clock();
+  
+  return 1;
+}