diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index d52e1c85a3f34072a30b3769eacd7454a82971ea..799deee59a666d88dbde48077cfbcd64d7cd0634 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -19,13 +19,13 @@
 - constante entière longue: utiliser la représentation sous forme de string et 
   rechercher la base appropriée.
 - arithmetic overflows
-[Bernard] avoir une fonction 
+- [Bernard] avoir une fonction 
   e_acsl_assert(int guard, char *msg, char *kind) {
     if (guard) e_acsl_fail(msg, kind);
   }
 à appeler au lieu de générer la garde. La kind est le type de l'annotation 
 (assert, requires, ensures, RTE? ...)
-[Bernard] avoir une fonction
+- [Bernard] avoir une fonction
   e_acsl_trace_behavior(char *bhv_name) {}
 à appeler dès qu'un behavior est activé
 - meilleur schéma de compilation des assumes:
@@ -35,6 +35,10 @@
     run_function;
     ensures_bhv;
   }
+- utiliser Rte (get_rte_annotations dans Oxygen)
+- [Yannick] Logic functions
+- type system for generating C int/float when possible 
+  (generalisation of current Visit.principal_type)
 
 ##############
 # KNOWN BUGS #
@@ -47,7 +51,6 @@
 #########
 
 - fonction sans code
-- exécuter rte
 - tester plusieurs fonctions contenant des annotations
 - améliorer test "integer_constant.i" quand bug fixed #745
 - test sizeof.i devraient être plus précis quand logic_typing plus précis
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index ba7dde236b707863f04d68838bac67590690d622..d76d6369f19646da925429be340f4b5600e72e49 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -6,7 +6,7 @@ PROJECT_FILE.i:136:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
 /* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 7d10e2a3f562dbd515f55e4cccb837c7135c5e38..667ac7338dc0c32ea4b6bb5427c989563f69f67b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -808,9 +808,9 @@ PROJECT_FILE.i:521:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {-3}
           y ∈ {2}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index 71c56e656d7fc3abdacefa078621cb0c73c2ec80..60f253ae3c0e5413a03af16febf4b8a2af109cf3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -37,9 +37,9 @@ PROJECT_FILE.i:157:[value] Assertion got status unknown.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           T1[0] ∈ {0; 2}
             [1..2] ∈ {0; 1; 2}
           T2[0] ∈ {0; 2}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index 0b57da4f8feb6c582fec30b67f2f094a51cd40c0..84ff027948641741aaab5279b4f6f3fa5c4eea16 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -346,9 +346,9 @@ PROJECT_FILE.i:256:[value] Assertion got status unknown.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function f:
+[value] Values at end of function f:
           A ∈ {3}
           e_acsl_1 ∈ {0}
           e_acsl_5 ∈ {1}
@@ -356,7 +356,7 @@ PROJECT_FILE.i:256:[value] Assertion got status unknown.
           e_acsl_13 ∈ {0}
           e_acsl_14 ∈ {0}
           e_acsl_18 ∈ {3}
-[value] Values for function g:
+[value] Values at end of function g:
           A ∈ {4}
           e_acsl_1 ∈ {0}
           e_acsl_2 ∈ {2}
@@ -365,7 +365,7 @@ PROJECT_FILE.i:256:[value] Assertion got status unknown.
           x ∈ {1}
           t[0] ∈ {2}
            [1] ∈ {3}
-[value] Values for function main:
+[value] Values at end of function main:
           A ∈ {4}
           __retres ∈ {0}
           x ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 04fedcf0e6436a0b04d2c2b98a206799fe40588b..419b294f37933487cdd3fb79b8ca191664e2e763 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -52,9 +52,9 @@ PROJECT_FILE.i:100:[value] Function __gmpz_get_ui: precondition got status valid
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
           y ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index edd0696c274c938329b5c6648dfba03de3dd828f..d5ae506c57df93798da9909919ac86d33bec0778 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -279,9 +279,9 @@ PROJECT_FILE.i:285:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
           y ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index beab2cdef0da74bf81e7583e86996957ea1f24f4..ef3b4b4c178ad80a36b4868217852482458f2767 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -5,7 +5,7 @@
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
 /* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index 81b033ed0e004316a740cce92de16afc8fbb3aa5..28f4cda1b750eae8ea882e0ac89f60c6cf3cf769 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -539,22 +539,22 @@ PROJECT_FILE.i:410:[value] Function l: postcondition got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function f:
+[value] Values at end of function f:
           X ∈ {1}
-[value] Values for function g:
+[value] Values at end of function g:
           X ∈ {2}
-[value] Values for function h:
+[value] Values at end of function h:
           X ∈ {3}
-[value] Values for function i:
+[value] Values at end of function i:
           X ∈ {5}
-[value] Values for function j:
+[value] Values at end of function j:
           X ∈ {3}
-[value] Values for function k:
+[value] Values at end of function k:
           X ∈ {5}
-[value] Values for function l:
-[value] Values for function main:
+[value] Values at end of function l:
+[value] Values at end of function main:
           X ∈ {5}
           __retres ∈ {0}
 /* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index 06d34e6faeb48fbef2e412ea87666c53c1242093..92fbba223015347539e93e6fadf426789ae51ab1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -32,9 +32,9 @@ PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
 /* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index fb826c17cb217d1e087d080788cd605b48b778d6..2744a9206e558d003b120329674a7ad5b162fc10 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -194,9 +194,9 @@ PROJECT_FILE.i:297:[value] Assertion got status invalid (stopping propagation).
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
           y ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index 132e58469233fc1d8bb57fa60560227ac6f4fa81..c19d36b485ad639adc74bebad41da6c1c839ab5f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -161,9 +161,9 @@ PROJECT_FILE.i:43:[value] Function __gmpz_clear: precondition got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {2}
           y ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index b31bf4205960abf0091a47260dcdc7de397950f2..c48528acf5d31df349e76d28a5d89fb07d3b2d7e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -6,7 +6,7 @@ PROJECT_FILE.i:136:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
 /* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
index a7721d393d56ab5de28bbac8443c1a5d314d72c3..265e6cabe408e1e5807edd16b71090057dd80f16 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
@@ -6,7 +6,7 @@ PROJECT_FILE.i:134:[value] Assertion got status unknown.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
 /* Generated by Frama-C */
 /*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index bd930837970fa6a638fbe65a217fe7a1ab996ab8..9b6270007a983f5c7ab5d08c60c99522ba94bbc6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -32,9 +32,9 @@ PROJECT_FILE.i:152:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
 /* Generated by Frama-C */
 struct __anonstruct___mpz_struct_1 {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index 2a420a7925665366a84e3eafe75ee5f1ef3c1f08..972b05cce496b8d9b0011cd0953883a0176f98ca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -514,9 +514,9 @@ PROJECT_FILE.i:310:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {1}
           t[0] ∈ {2}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index 7e8190c259ba6dff237cd1c625824f2b179ffaaf..5f62bd3b13f1000bf00d6716cdee18562062a5f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -85,16 +85,16 @@ PROJECT_FILE.i:165:[value] Function h: postcondition got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function g:
-[value] Values for function e_acsl_fail:
+[value] Values at end of function g:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function f:
+[value] Values at end of function f:
           x ∈ {0}
           e_acsl_1 ∈ {1}
           e_acsl_3 ∈ {1}
-[value] Values for function h:
+[value] Values at end of function h:
           __retres ∈ {0}
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
 /* Generated by Frama-C */
 struct __anonstruct___mpz_struct_1 {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 5bb1671625b0973cdade87c838a1b262e8e88fc1..098bbf627fb776f0679b4c14307040ce21eef969 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -62,9 +62,9 @@ PROJECT_FILE.i:150:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
 /* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index fdd4bffc1e3f7f22cba70cce273bee4d83e939f9..ebe5dc9303af0122365f52851f77aac6beaceaf3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -543,9 +543,9 @@ PROJECT_FILE.i:312:[value] assigning non deterministic value for the first time
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
+[value] Values at end of function e_acsl_fail:
           NON TERMINATING FUNCTION
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {7}
           y ∈ {2}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index 540c8f0d05956a94a501f1efb0ef80425052dda5..6f641f5decb77daf87f1771014102011b6451df5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -6,7 +6,7 @@ PROJECT_FILE.i:136:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function main:
+[value] Values at end of function main:
           __retres ∈ {0}
           x ∈ {0}
 /* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a02d675b0943aa3cb01c5a9dd86ca00b6f43e151..4016f2918eb3a8286ea5e9d5bef337fb9e291fce 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -103,8 +103,9 @@ let principal_type_from_term t1 t2 =
       Linteger
     | TConst (CInt64(_, k, _)), _ -> 
       (* C-representable constant *)
-      Ctype (TInt (k, []))  
+      Ctype (TInt (k, []))
     | _, _ -> 
+      (* for direct C terms, should be able to infer the corresponding C type *)
       ty
   in
   principal_type (typ t1) (typ t2)