translate TODO into English

src/plugins/e-acsl/TODO

@@ -2,26 +2,20 @@
 # FEATURE WISHES #
 ##################
 
-- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
-  à appeler dès qu'un behavior est activé
+- [Bernard] implement a function e_acsl_trace_behavior(char *bhv_name) {}
+  which would be called anytime a behavior is activated
 - [Yannick] Logic functions
 - [Nikolaï] temporal memory properties
 - memory profiling
-- [Guillaume] ajouter les annotations de RTE dans la table des annotations
-  	      (avec une option)
-- [David Mentré] tset
-- [Guillaume] voir les valeurs quand la spec échoue, voir Boogaloo@RV'13 à ce 
-  sujet
-- [Tout le monde] scripts de compilation du programme généré
-- [Enseignement] assigns
+- [Guillaume] add the RTE annotations generated by E-ACSL in the Frama-C 
+  annotation table (possibly through a new command line option)
+- [David Mentré] support of tset
+- [Guillaume] when a verification fails at runtime, possibility of seeing the
+  values of each involved left-values (cf Boogaloo@RV'13).
+- [Everyone] provide the compilation scripts of the generated program
+- [Teaching purpose] support of assigns
 - multithreading
-
-=====
-- Voir avec Guillaume et Nikolaï ce dont ils ont besoin comme API pour faire
-  leur génération de code pour les entrées de PathCrawler...
-  ==> problème de la connaissance de la taille des tableaux 
-  (Pathcrawler_dimension)
-=====
+- Required API for Stady
 
 #####################
 # E-ACSL CONSTRUCTS #
@@ -42,22 +36,21 @@
 ########
 
 - grep TODO *.ml*
-- Gestion du mode -lib-entry
-- générer les delete des globals dans une fonction séparée, comme pour les init.
-- generate guard for \offset, \block_length and \base_addr
+- Support of -lib-entry
+- generate 'free' statements of global in a separate function
+  (similarly to initialization).
+- generate guards for \offset, \block_length and \base_addr
   (\offset(p) must ensures that p is valid)
 - don't generate code for properties with status valid_under_hyp when we know
-  that the hyp will be generated
-- use value analysis whenever possible instead of our own imprecise analysis
+  that the hyp is (or is going to be) generated
 - use checked assigns whenever possible in the analysis
-  checked property = valid property or property for which code will be generated
-- RTE avec du code GMP
-- ne pas appeler __malloc et __free quand pas nécessaire. Nécessite d'avoir
-  malloc, __malloc, __e_acsl_malloc, __e_acsl__malloc (idem pour free)
-- analysis: optimize it by performing no join over sets anymore
-- analysis: fixed incorrectness in presence of recursive functions
-- RTE: potential duplication (e.g. with **p)
-- default output of e_acsl_assert in the format of standart error messages
+  checked = already verified or verified at runtime
+- RTE on GMP code
+- call custom __malloc et __free only when required, and use standard malloc 
+  and free in the other cases.
+- RTE: eliminate redundant checks (e.g. on **p)
+- default output of e_acsl_assert should be in the same format than standart 
+  error messages (nicer in Emacs for instance)
 - some calls to __eacsl_memory_debug are missing in debug mode
 - translate only once the assumes clause in presence of a pre- and a 
   post-condition
@@ -68,25 +61,25 @@
 
 - see BTS
 - see Chapter "Known Limitations" of the User Manual
-- variable GMP potentiellement initialisée mais non utilisée en présence de \at
-  (voir test result.i, cas -e-acsl-gmp-only)
-- comparaisons qui aboutissent à du C incorrect
-  ==> comparaison de chaînes litérales
-   (voir tests other_constants.i et comparison.i)
-    --> dépend de la sémantique d'ACSL non fixée
-    --> veut-on le transformer en égalité des caractères avec un ordre lexico 
-    ou veut-on générer une erreur (comportement non **spécifié** du C). 
-  ==> comparaison de pointeurs --> générer une erreur (merci RTE?)
-- \at incorrect si StmtLabel faisant référence au stmt courant (voir test at.i)
-- incorrect d'utiliser Pre, Post, Here, Old dans stmt contract 
-  (même problème que Jessie: cf. BTS #72)
-  (voir aussi result.i et ./at_stmt_contract.i)
-- interprétation des tableaux logiques
-[Dillon] Windows
+- GMP variables are possibly initialized but never used in presence of \at
+  (see test result.i, case -e-acsl-gmp-only)
+- ACSL comparisons may lead to generate incorrect C code
+  ==> comparison of literal strings
+   (see tests other_constants.i et comparison.i)
+    --> what is the exact ACSL semantics?
+    --> use a lexicographical ordering based on an equality over characters, or 
+generate an error (unspecified C behavior)? 
+  ==> pointer comparisons --> may generate an error (use RTE?)
+  ==> equality of logical arrays
+  ==> equality of reals --> convert into an equality of double
+  (see tests/e-acsl-runtime/bts1307.i).
+- incorrect translation of \at if the label refers to the current statement (see
+test at.i)
+- issue when using labels Pre, Post, Here, Old in a stmt contract 
+  (similar issue than Jessie, cf. BTS #72)
+  (see tests result.i and ./at_stmt_contract.i)
+- interpretation of logical arrays
 - \valid(p) is not true if p is a const pointer (depend on -const-readonly)
-- utiliser == avec des real en arguments : c'est convertit en une égalité sur 
-des floating points, qui ne fait notoirement pas ce qu'on veut 
-(voir tests/e-acsl-runtime/bts1307.i).
 
 [to be check]: no call to full_init or initialize for the assigned result of a 
 function call
@@ -101,9 +94,9 @@ function call
 # TESTS #
 #########
 
-- inclure exemple du E-ACSL Reference Manual
-- inclure exemple du E-ACSL User Manual
-- inclure exemple du E-ACSL Tutorial
+- add examples from E-ACSL Reference Manual
+- add examples from E-ACSL User Manual
+- add examples from E-ACSL Tutorial
 - currently, tests require a non-free version of Frama-C (built-ins Value)
-- [Guillaume] tests de non-régression de temps d'exécution (+ conso mémoire)
-  pour voir les dégradations/gains de performance.
+- [Guillaume] how to test execution time/memory consumption of E-ACSL in order
+  to detect regression about these behaviors?