TODO

##################
# FEATURE WISHES #
##################

- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
  à appeler dès qu'un behavior est activé
- [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

=====
- 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)
=====

#####################
# E-ACSL CONSTRUCTS #
#####################

- assigns, loop assigns
- predicates
- logic functions
- disjoint and complete behaviors (cf. Bernard's feature wish)
- loop variant
- logical shift (at least in non GMP mode)
- let-in
- tset
- grep "not_yet" *.ml

########
# CODE #
########

- 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
  (\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
- 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
- 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

##############
# KNOWN BUGS #
##############

- 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
- \valid(p) is not true if p is a const pointer (depend on -const-readonly)

[to be check]: no call to full_init or initialize for the assigned result of a 
function call

#######
# DOC #
#######

- check of runtime error in combination with RTE

#########
# TESTS #
#########

- inclure exemple du E-ACSL Reference Manual
- inclure exemple du E-ACSL User Manual
- inclure exemple du E-ACSL Tutorial
- currently, tests require a non-free version of Frama-C (built-ins Value)