soc2c: previous changes broke programs with enumerated types.

_oasis

 OASISFormat: 0.4
 Name:        lustre-v6
-Version:     1.691
+Version:     1.692
 Synopsis:    The Lustre V6 Verimag compiler
 Description: This package contains:
    (1) lus2lic: the (current) name of the compiler (and interpreter via -exec).

arduino/led_puzlle/doc/puzzle.org

@@ -8,28 +8,63 @@
 #+DATE:  Laboratoire Verimag -- Faites de la science !
 
 
-Du Lustre pour des jolies leds
+Du Lustre aux jolies leds
 
-* Introduction
+file:arduino.jpg
 
-Au  laboratoire   =Verimag=,  on  cherche  à   aider  les  ingénieurs
+* Introduction
+ 
+Au  laboratoire   =Verimag=,  nous   cherchons  à   aider  les  ingénieurs
 informaticiens à _prouver automatiquement_ que leurs programmes sont
 _corrects_.
 
-- C'est important, en particulier pour les *systèmes embarqués*.
-- Mais c'est difficile (explosion combinatoire ; $2^{64}>18*10^{15}$).
-
-Plusieurs approches :
-- *Langages* de programmation (empêcher les programmeurs de faire des erreurs)
-- *Analyse de programme* 
-- Tests automatisés
-
-Nous allons embarquer des puzzles écrits en =Lustre= sur un =Arduino=
-
-file:arduino.jpg
+- La correction des programmes est  cruciale, en particulier pour les
+  *systèmes embarqués*, car des vies sont souvent en jeu.
+- Mais elle est difficile à cause de *l'explosion combinatoire*.  Une
+  bonne illustration  de ce  phénoméne est  donnée par  l'échiquer de
+  Sissa, comportant 1 grain  de riz sur case 1, 2  grains sur la case
+  2, 4 sur la case 3, 8 sur la case 4, etc. Un tel échiquier comporte
+  $2^{64}-1$ grains  de riz,  c'est à  dire plus  de 18\nbsp{}milliards de
+  grains, soit l'équivalent de 1000 ans de production mondiale de riz
+  actuellement. Or  un programme de  64 cases  (ou bits) est  un 
+  petit programme.
+
+Plusieurs approches sont possibles pour faire face à cette difficulté.
+Au laboratoire Verimag, les axes de recherche visant à résoudre ce type 
+de  problèmes concernent :
+
+- la  conception de  *Langages* de  programmation   empêchant les
+  programmeurs de faire certaines  erreurs;
+- l'*Analyse   de  programmes*   :   conception  d'algorithmes   (des
+  programmes aussi)  qui essaient de *prouver*  qu'un autre programme
+  est « *correct* ».
+- l'automatisation des *tests* :  conception d'algorithmes qui essaient
+  de prouver qu'un programme n'est *pas* correct.
+
+Pour illustrer tous ces axes de recherche, nous proposons une petite démonstration
+permettant de montrer
+1. quelques exemples de programmes écrit en Lustre, un langage inventé
+   au  laboratoire  et  conçu  pour  mettre  en  oeuvre  des  systèmes
+   embarqués critiques ;
+2. comment un  tel programme peut-être embarqué sur  un système (ici,
+   une carte =Arduino=) ;
+3. comment prouver automatiquement des propriétés sur ces programmes ;
+4. comment tester automatiquement ces programmes.
+
+Il s'agit  donc de valider  est donc  un petit système,  composé d'un
+programme  Lustre et  d'une  carte =Arduino=,  comportant 2  entrées,
+contrôllées par  un bouton  rouge et  un bouton  bleu, et  5 sorties,
+représentées par 5 leds.
+
+
+La propriété de sureté que l'on veut vérifier est « il est impossible
+d'allumer les 5  leds ».  Pour chaque programme  qu'on embarquera sur
+la carte, la question sera donc 
+de  savoir s'il est possible d'allumer les
+5 leds (signifiant qu'il y a  un problème) en jouant sur les entrées.
+Nous  montreront ensuite  comment des  outils peuvent  automatiser la
+preuve de correction ou de non correction.
 
-L'objectif de ces  petits puzzles programmés en  Lustre est d'allumer
-toutes les lampes (led) à l'aide de 2 boutons : un rouge, et un bleu.
 
 * Puzzle 1
 

src/lv6version.ml

 (** Automatically generated from Makefile *) 
 let tool = "lus2lic"
 let branch = "master"
-let commit = "691"
-let sha_1 = "4b986d0e2347825949ec0bb88100d125d46d14fd"
+let commit = "692"
+let sha_1 = "1adfcf741e7130599563f6c5667e829f5efad671"
 let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
 let maintainer = "jahier@imag.fr"

src/soc2c.ml

-(* Time-stamp: <modified the 05/05/2017 (at 17:04) by Erwan Jahier> *)
+(* Time-stamp: <modified the 01/06/2017 (at 16:12) by Erwan Jahier> *)
 
 
 (* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
@@ -901,13 +901,15 @@ typedef float _float;
 #define _true 1
 #endif
 // end of _SOC2C_PREDEF_TYPES
-" ^ (typedef_all licprg stbl main_soc )
-  ^ (if needs_hfile then "#include \""^ base ^"_ext.h\"" else "")^
-"// User typedef 
+// User typedef 
 #ifndef _"^base^"_TYPES
 #define _"^base^"_TYPES\n");
     output_string types_h_oc (user_typedef licprg);
-    output_string types_h_oc ("#endif // enf of  _"^base^"_TYPES\n");
+    output_string types_h_oc ("#endif // enf of  _"^base^"_TYPES
+"
+  ^ (typedef_all licprg stbl main_soc )
+  ^ (if needs_hfile then "#include \""^ base ^"_ext.h\"" else ""));
+   
     try
     let putc s = output_string occ s in
     let puth s = output_string och s in

test/lus2lic.sum

 ==> lus2lic0.sum <==
-Test Run By jahier on Fri May  5 17:11:23 
+Test Run By jahier on Thu Jun  1 16:16:10 
 Native configuration is x86_64-unknown-linux-gnu
 
 		=== lus2lic0 tests ===
@@ -64,7 +64,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
 XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
 
 ==> lus2lic1.sum <==
-Test Run By jahier on Fri May  5 17:11:25 
+Test Run By jahier on Thu Jun  1 16:16:11 
 Native configuration is x86_64-unknown-linux-gnu
 
 		=== lus2lic1 tests ===
@@ -97,7 +97,8 @@ PASS: ./lus2lic  {-2c Gyroscope.lus -n Gyroscope}
 PASS: sh Gyroscope.sh 
 PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c Gyroscope.lus  {}
 PASS: ./lus2lic  {-2c Gyroscope2.lus -n Gyroscope2}
-FAIL: Check that the generated C code compiles  : sh Gyroscope2.sh 
+PASS: sh Gyroscope2.sh 
+PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c Gyroscope2.lus  {}
 PASS: ./lus2lic  {-2c aa.lus -n aa}
 PASS: sh aa.sh 
 PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c aa.lus  {}
@@ -271,7 +272,8 @@ PASS: sh fresh_name.sh
 PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c fresh_name.lus  {}
 PASS: ./lus2lic  {-2c func_with_body.lus -n func_with_body}
 PASS: ./lus2lic  {-2c hanane.lus -n hanane}
-FAIL: Check that the generated C code compiles  : sh hanane.sh 
+PASS: sh hanane.sh 
+PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c hanane.lus  {}
 PASS: ./lus2lic  {-2c heater_control.lus -n heater_control}
 PASS: sh heater_control.sh 
 PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c heater_control.lus  {}
@@ -370,7 +372,8 @@ PASS: ./lus2lic  {-2c modes3x2_v2.lus -n modes3x2_v2}
 PASS: sh modes3x2_v2.sh 
 PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c modes3x2_v2.lus  {}
 PASS: ./lus2lic  {-2c modes3x2_v3.lus -n modes3x2_v3}
-FAIL: Check that the generated C code compiles  : sh modes3x2_v3.sh 
+PASS: sh modes3x2_v3.sh 
+PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c modes3x2_v3.lus  {}
 PASS: ./lus2lic  {-2c modes3x2_v4.lus -n modes3x2_v4}
 PASS: ./lus2lic  {-2c mouse.lus -n mouse}
 PASS: sh mouse.sh 
@@ -395,7 +398,7 @@ PASS: sh multipar.sh
 PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus  {}
 
 ==> lus2lic2.sum <==
-Test Run By jahier on Fri May  5 17:12:31 
+Test Run By jahier on Thu Jun  1 16:17:05 
 Native configuration is x86_64-unknown-linux-gnu
 
 		=== lus2lic2 tests ===
@@ -735,7 +738,7 @@ PASS: sh zzz2.sh
 PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus  {}
 
 ==> lus2lic3.sum <==
-Test Run By jahier on Fri May  5 17:13:41 
+Test Run By jahier on Thu Jun  1 16:18:03 
 Native configuration is x86_64-unknown-linux-gnu
 
 		=== lus2lic3 tests ===
@@ -1240,7 +1243,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
 
 
 ==> lus2lic4.sum <==
-Test Run By jahier on Fri May  5 17:15:38 
+Test Run By jahier on Thu Jun  1 16:19:48 
 Native configuration is x86_64-unknown-linux-gnu
 
 		=== lus2lic4 tests ===
@@ -1732,8 +1735,8 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
 
 		=== lus2lic1 Summary ===
 
-# of expected passes		311
-# of unexpected failures	8
+# of expected passes		317
+# of unexpected failures	5
 
 ==> lus2lic2.sum <==
 
@@ -1756,15 +1759,15 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
 # of expected passes		465
 # of unexpected failures	6
 ===============================
-# Total number of failures: 26
-lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 66 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 70 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 117 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 63 seconds
+# Total number of failures: 23
+lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 53 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 58 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 105 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 57 seconds
 * Ref time: 
-0.06user 0.01system 5:17.88elapsed 0%CPU (0avgtext+0avgdata 5564maxresident)k
-0inputs+0outputs (0major+6163minor)pagefaults 0swaps
+0.04user 0.02system 4:35.78elapsed 0%CPU (0avgtext+0avgdata 5672maxresident)k
+64inputs+0outputs (0major+6088minor)pagefaults 0swaps
 * Quick time (-j 4):
-0.05user 0.02system 2:08.66elapsed 0%CPU (0avgtext+0avgdata 5700maxresident)k
-160inputs+0outputs (0major+6197minor)pagefaults 0swaps
+0.04user 0.04system 2:28.15elapsed 0%CPU (0avgtext+0avgdata 5660maxresident)k
+160inputs+0outputs (0major+6123minor)pagefaults 0swaps