################
# 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