TODO

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

- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
  à appeler dès qu'un behavior est activé
- utiliser Rte pour tous les overflows potentiels
  (get_rte_annotations dans Oxygen)
- [Yannick] Logic functions

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

- grep TODO *.ml*
- gestion des initialiseurs des globals: requiert un main
- mkcall ne devrait pas générer de nouvelles variables pour une même fonction

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

- \at incorrect si StmtLabel faisant référence au stmt courant (voir test at.i)
- incorrect d'utiliser un \old dans le post-state si pre-state == post-state
  (même raison que ci-dessus)
- incorrect d'utiliser Pre, Post, Here, Old dans stmt contract 
  (même problème que Jessie: cf. BTS #72)

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

- améliorer test "integer_constant.i" quand bug fixed #745
- inclure exemple du E-ACSL Reference Manual
- test arith.i: mettre les exemples du ACSL manual about div and modulo
- test lazy.i: en attente d'un fix dans l'analyse de valeurs