TODO

################
# NEXT RELEASE #
################

- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
  à appeler dès qu'un behavior est activé
- [Yannick] Logic functions

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

- grep TODO *.ml*
- Gestion du mode -lib-entry
- variable GMP potentiellement initialisé mais non utilisé en présence de \at
  (voir test result.i, cas -e-acsl-gmp-only)
- générer les delete des globals dans une fonction séparée, comme pour les init.
- do not analyse library function in pre-analysis
- variadic functions are not yet duplicated
- generate guard for \offset & co (\offset(p) must ensures that p is valid)

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

- see BTS
- 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
- \valid (or other memory-model constructs) in ensures of functions without code

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

- inclure exemple du E-ACSL Reference Manual
- test arith.i: mettre les exemples du ACSL manual about div and modulo