remove TODO: moved on gitlab

src/plugins/e-acsl/TODO

-##################
-# FEATURE WISHES #
-##################
-
-- [Bernard] implement a function e_acsl_trace_behavior(char *bhv_name) {}
-  which would be called anytime a behavior is activated
-- [Yannick] Logic functions
-- [Nikolaï] temporal memory properties
-- memory profiling
-- [Guillaume] add the RTE annotations generated by E-ACSL in the Frama-C
-  annotation table (possibly through a new command line option)
-- [David Mentré] support of tset
-- [Guillaume] when a verification fails at runtime, possibility of seeing the
-  values of each involved left-values (cf Boogaloo@RV'13).
-- [Everyone] provide the compilation scripts of the generated program
-- [Teaching purpose] support of assigns
-- multithreading
-- Required API for Stady
-
-#####################
-# 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*
-- Support of -lib-entry
-- generate 'free' statements of global in a separate function
-  (similarly to initialization).
-- generate guards 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 is (or is going to be) generated
-- use checked assigns whenever possible in the analysis
-  checked = already verified or verified at runtime
-- RTE on GMP code
-- call custom __malloc et __free only when required, and use standard malloc
-  and free in the other cases.
-- RTE: eliminate redundant checks (e.g. on **p)
-- default output of e_acsl_assert should be in the same format than standart
-  error messages (nicer in Emacs for instance)
-- 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
-- GMP variables are possibly initialized but never used in presence of \at
-  (see test result.i, case -e-acsl-gmp-only)
-- ACSL comparisons may lead to generate incorrect C code
-  ==> comparison of literal strings
-   (see tests other_constants.i et comparison.i)
-    --> what is the exact ACSL semantics?
-    --> use a lexicographical ordering based on an equality over characters, or
-generate an error (unspecified C behavior)?
-  ==> pointer comparisons --> may generate an error (use RTE?)
-  ==> equality of logical arrays
-  ==> equality of reals --> convert into an equality of double
-  (see tests/runtime/bts1307.i).
-- incorrect translation of \at if the label refers to the current statement (see
-test at.i)
-- issue when using labels Pre, Post, Here, Old in a stmt contract
-  (similar issue than Jessie, cf. BTS #72)
-  (see tests result.i and ./at_stmt_contract.i)
-- interpretation of logical arrays
-- \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 #
-#########
-
-- add examples from E-ACSL Reference Manual
-- add examples from E-ACSL User Manual
-- add examples from E-ACSL Tutorial
-- currently, tests require a non-free version of Frama-C (built-ins Value)
-- [Guillaume] how to test execution time/memory consumption of E-ACSL in order
-  to detect regression about these behaviors?