TODO

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

- [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
   appeler ds 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)

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

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

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

- grep TODO *.ml*
- Gestion du mode -lib-entry
- gnrer les delete des globals dans une fonction spare, 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 ncessaire. Ncessite 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 initialise mais non utilise en prsence de \at
  (voir test result.i, cas -e-acsl-gmp-only)
- comparaisons qui aboutissent  du C incorrect
  ==> comparaison de chanes litrales
   (voir tests other_constants.i et comparison.i)
    --> dpend de la smantique d'ACSL non fixe
    --> veut-on le transformer en galit des caractres avec un ordre lexico 
    ou veut-on gnrer une erreur (comportement non **spcifi** du C). 
  ==> comparaison de pointeurs --> gnrer une erreur (merci RTE?)
- \at incorrect si StmtLabel faisant rfrence au stmt courant (voir test at.i)
- incorrect d'utiliser Pre, Post, Here, Old dans stmt contract 
  (mme problme que Jessie: cf. BTS #72)
  (voir aussi result.i et ./at_stmt_contract.i)
- interprtation des tableaux logiques
[Dillon] Windows

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

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

- E_ACSL_MACHDEP with gcc -D
- check of runtime error in combination with RTE

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

- inclure exemple du E-ACSL Reference Manual
- inclure exemple du E-ACSL User Manual
- test arith.i: mettre les exemples du ACSL manual about div and modulo
- currently, tests require a non-free version of Frama-C