diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
new file mode 100644
index 0000000000000000000000000000000000000000..338f53cea472f49e4fd1ab8b557942e9a083530b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i
@@ -0,0 +1,17 @@
+/* run.config
+ COMMENT: TODO: this test is incomplete
+ COMMENT: comparison operators */
+void main() {
+ /* /\*@ assert "toto" < "titi"; *\/ */
+ /* /\*@ assert "toto" > "titi"; *\/ */
+ /* /\*@ assert "toto" <= "titi"; *\/ */
+ /* /\*@ assert "toto" >= "titi"; *\/ */
+ /* /\*@ assert "toto" == "titi"; *\/ */
+ /*@ assert "toto" != "titi"; */
+ /*@ assert 5 < 18; */
+ /*@ assert 32 > 3; */
+ /*@ assert 12 <= 13; */
+ /*@ assert 123 >= 12; */
+ /*@ assert 0xff == 0xff; */
+ /*@ assert 1 != 2; */
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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
new file mode 100644
index 0000000000000000000000000000000000000000..59295f93360e45505e2d70ab01aa85c3b3d1c119
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -0,0 +1,366 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+PROJECT_FILE:73:[value] Assertion got status valid.
+PROJECT_FILE:80:[value] Assertion got status valid.
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:82.
+PROJECT_FILE:82:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:82.
+PROJECT_FILE:82:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:83.
+PROJECT_FILE:83:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:83.
+PROJECT_FILE:83:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:84.
+PROJECT_FILE:84:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:85.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+PROJECT_FILE:69:[value] Function exit: postcondition got status invalid
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:86.
+PROJECT_FILE:86:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:86.
+[value] Done for function mpz_clear
+PROJECT_FILE:89:[value] Assertion got status valid.
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:91.
+PROJECT_FILE:91:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:91.
+PROJECT_FILE:91:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:92.
+PROJECT_FILE:92:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:92.
+PROJECT_FILE:92:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:93.
+PROJECT_FILE:93:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:94.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:95.
+PROJECT_FILE:95:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:95.
+[value] Done for function mpz_clear
+PROJECT_FILE:98:[value] Assertion got status valid.
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:100.
+PROJECT_FILE:100:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:100.
+PROJECT_FILE:100:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:101.
+PROJECT_FILE:101:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:101.
+PROJECT_FILE:101:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:102.
+PROJECT_FILE:102:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:103.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:104.
+PROJECT_FILE:104:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:104.
+[value] Done for function mpz_clear
+PROJECT_FILE:107:[value] Assertion got status valid.
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:109.
+PROJECT_FILE:109:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:109.
+PROJECT_FILE:109:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:110.
+PROJECT_FILE:110:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:110.
+PROJECT_FILE:110:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:111.
+PROJECT_FILE:111:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:112.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:113.
+PROJECT_FILE:113:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:113.
+[value] Done for function mpz_clear
+PROJECT_FILE:116:[value] Assertion got status valid.
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:117.
+PROJECT_FILE:117:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:118.
+PROJECT_FILE:118:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:119.
+PROJECT_FILE:119:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:120.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:121.
+PROJECT_FILE:121:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+PROJECT_FILE:124:[value] Assertion got status valid.
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:126.
+PROJECT_FILE:126:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:126.
+PROJECT_FILE:126:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_init <-main.
+ Called from PROJECT_FILE:127.
+PROJECT_FILE:127:[value] Function mpz_init: postcondition got status unknown
+[value] Done for function mpz_init
+[value] computing for function mpz_set_si <-main.
+ Called from PROJECT_FILE:127.
+PROJECT_FILE:127:[value] Function mpz_set_si: precondition got status valid
+[value] Done for function mpz_set_si
+[value] computing for function mpz_cmp <-main.
+ Called from PROJECT_FILE:128.
+PROJECT_FILE:128:[value] Function mpz_cmp: precondition got status valid
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <-main.
+ Called from PROJECT_FILE:129.
+[value] computing for function eprintf <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function eprintf
+[value] computing for function exit <-e_acsl_fail <-main.
+ Called from PROJECT_FILE:69.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:130.
+PROJECT_FILE:130:[value] Function mpz_clear: precondition got status valid
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <-main.
+ Called from PROJECT_FILE:130.
+[value] Done for function mpz_clear
+[value] Recording results for main
+[value] done for function main
+[from] Computing for function mpz_init
+[from] Done for function mpz_init
+[from] Computing for function mpz_set_si
+[from] Done for function mpz_set_si
+[from] Computing for function mpz_cmp
+[from] Done for function mpz_cmp
+[from] Computing for function e_acsl_fail
+[from] Computing for function eprintf <-e_acsl_fail
+[from] Done for function eprintf
+[from] Computing for function exit <-e_acsl_fail
+[from] Done for function exit
+PROJECT_FILE:69:[from] Non terminating function (no dependencies)
+[from] Done for function e_acsl_fail
+[from] Computing for function mpz_clear
+[from] Done for function mpz_clear
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function e_acsl_fail:
+ NON TERMINATING FUNCTION
+[value] Values for function main:
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\at(x,Old));
+ assigns *x; */
+extern void mpz_init(__mpz_struct * /*[1]*/ x ) ;
+/*@ requires \valid(x);
+ assigns *x; */
+extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
+/*@ requires \valid(z);
+ assigns *z; */
+extern void mpz_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int mpz_cmp(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ) ;
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status ) ;
+/*@ assigns \nothing; */
+extern void eprintf(char * ) ;
+void e_acsl_fail(char *msg )
+{
+ eprintf(msg);
+ exit(1);
+ return;
+}
+
+void main(void)
+{
+ /*@ assert ("toto" ≢ "titi"); */ ;
+ if ("toto" == "titi") {
+ e_acsl_fail((char *)"((\"toto\" \342\211\242 \"titi\"))");
+ }
+ /*@ assert (5 < 18); */ ;
+ { mpz_t e_acsl_cst_1 ; mpz_t e_acsl_cst_2 ; int e_acsl_cst_3 ;
+ mpz_init((__mpz_struct *)(e_acsl_cst_1));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_1),(long )5);
+ mpz_init((__mpz_struct *)(e_acsl_cst_2));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_2),(long )18);
+ e_acsl_cst_3 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
+ (__mpz_struct *)(e_acsl_cst_2));
+ if (e_acsl_cst_3 >= 0) { e_acsl_fail((char *)"((5 < 18))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_2));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_1));
+ }
+
+ /*@ assert (32 > 3); */ ;
+ { mpz_t e_acsl_cst_4 ; mpz_t e_acsl_cst_5 ; int e_acsl_cst_6 ;
+ mpz_init((__mpz_struct *)(e_acsl_cst_4));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_4),(long )32);
+ mpz_init((__mpz_struct *)(e_acsl_cst_5));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_5),(long )3);
+ e_acsl_cst_6 = mpz_cmp((__mpz_struct *)(e_acsl_cst_4),
+ (__mpz_struct *)(e_acsl_cst_5));
+ if (e_acsl_cst_6 <= 0) { e_acsl_fail((char *)"((32 > 3))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_5));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_4));
+ }
+
+ /*@ assert (12 ≤ 13); */ ;
+ { mpz_t e_acsl_cst_7 ; mpz_t e_acsl_cst_8 ; int e_acsl_cst_9 ;
+ mpz_init((__mpz_struct *)(e_acsl_cst_7));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_7),(long )12);
+ mpz_init((__mpz_struct *)(e_acsl_cst_8));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_8),(long )13);
+ e_acsl_cst_9 = mpz_cmp((__mpz_struct *)(e_acsl_cst_7),
+ (__mpz_struct *)(e_acsl_cst_8));
+ if (e_acsl_cst_9 > 0) { e_acsl_fail((char *)"((12 \342\211\244 13))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_8));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_7));
+ }
+
+ /*@ assert (123 ≥ 12); */ ;
+ { mpz_t e_acsl_cst_10 ; mpz_t e_acsl_cst_11 ; int e_acsl_cst_12 ;
+ mpz_init((__mpz_struct *)(e_acsl_cst_10));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_10),(long )123);
+ mpz_init((__mpz_struct *)(e_acsl_cst_11));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_11),(long )12);
+ e_acsl_cst_12 = mpz_cmp((__mpz_struct *)(e_acsl_cst_10),
+ (__mpz_struct *)(e_acsl_cst_11));
+ if (e_acsl_cst_12 < 0) { e_acsl_fail((char *)"((123 \342\211\245 12))");
+ } mpz_clear((__mpz_struct *)(e_acsl_cst_11));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_10));
+ }
+
+ /*@ assert (0xff ≡ 0xff); */ ;
+ { mpz_t e_acsl_cst_13 ; int e_acsl_cst_14 ;
+ mpz_init((__mpz_struct *)(e_acsl_cst_13));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_13),(long )0xff);
+ e_acsl_cst_14 = mpz_cmp((__mpz_struct *)(e_acsl_cst_13),
+ (__mpz_struct *)(e_acsl_cst_13));
+ if (e_acsl_cst_14 != 0) {
+ e_acsl_fail((char *)"((0xff \342\211\241 0xff))");
+ } mpz_clear((__mpz_struct *)(e_acsl_cst_13));
+ }
+
+ /*@ assert (1 ≢ 2); */ ;
+ { mpz_t e_acsl_cst_15 ; mpz_t e_acsl_cst_16 ; int e_acsl_cst_17 ;
+ mpz_init((__mpz_struct *)(e_acsl_cst_15));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_15),(long )1);
+ mpz_init((__mpz_struct *)(e_acsl_cst_16));
+ mpz_set_si((__mpz_struct *)(e_acsl_cst_16),(long )2);
+ e_acsl_cst_17 = mpz_cmp((__mpz_struct *)(e_acsl_cst_15),
+ (__mpz_struct *)(e_acsl_cst_16));
+ if (e_acsl_cst_17 == 0) { e_acsl_fail((char *)"((1 \342\211\242 2))"); }
+ mpz_clear((__mpz_struct *)(e_acsl_cst_16));
+ mpz_clear((__mpz_struct *)(e_acsl_cst_15));
+ }
+
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 16b895cae939eafed8fccb0788df05bfca4d0372..21c58fad18df918b4d871101f685d53342492b99 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -229,7 +229,6 @@ let rec term_to_exp is_global t = match t.term_node with
| Trange _ -> not_yet "range"
| Tlet _ -> not_yet "let binding"
-(* [TODO] not fully test *)
let relation_to_revbinop = function
| Rlt -> Ge
| Rgt -> Le