diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
new file mode 100644
index 0000000000000000000000000000000000000000..7d5b6038a8e3e309da18f0febc2d62661a9fffb9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/lazy.i
@@ -0,0 +1,15 @@
+/* run.config
+ COMMENT: predicate using lazy operators
+ EXECNOW: LOG gen_lazy.c BIN gen_lazy.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/lazy.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_lazy.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_lazy.out -lgmp ./tests/e-acsl-runtime/result/gen_lazy.c && ./tests/e-acsl-runtime/result/gen_lazy.out
+*/
+
+int main(void) {
+ int x = 0, y = 1;
+ /*@ assert x == 0 && y == 1; */
+ /*@ assert ! (x != 0 && y == 1/0); */
+ /*@ assert x == 1 || y == 1; */
+ /*@ assert x == 0 || y == 1/0; */
+ /*@ assert x == 0 ==> y == 1; */
+ /*@ assert x == 1 ==> y == 1/0; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_string_literal.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
similarity index 94%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_string_literal.c
rename to src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index d6ef85ef079b4bef6292672ab4273da6e93e48a7..e3ce7f6a71b72f01cb41ca7c2add20309c11a42d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_string_literal.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -7,6 +7,7 @@ struct __anonstruct___mpz_struct_6 {
mp_limb_t *_mp_d ;
};
typedef struct __anonstruct___mpz_struct_6 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
typedef mp_limb_t *mp_ptr;
typedef mp_limb_t const *mp_srcptr;
typedef long mp_size_t;
@@ -19,11 +20,24 @@ typedef __mpz_struct const *mpz_srcptr;
typedef __mpz_struct *mpz_ptr;
typedef __mpq_struct const *mpq_srcptr;
typedef __mpq_struct *mpq_ptr;
+enum bool {
+ false = 0,
+ true = 1
+};
/* compiler builtin:
long __builtin_expect(long, long); */
/*@ assigns \nothing; */
extern int printf(char const * __restrict __format , ...);
__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2) __attribute__((
+__pure__));
__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
@@ -35,6 +49,9 @@ __pure__));
__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
mp_size_t __gmp_n) __attribute__((
__pure__));
+/*@ ensures \valid(\old(z));
+ assigns *z; */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
@@ -555,6 +572,20 @@ int main(void)
/*@ assert "toto" ≢ "titi"; */ ;
if (! ("toto" != "titi")) { e_acsl_fail((char *)"(\"toto\" != \"titi\")");
}
+ /*@ assert 'c' ≡ 'c'; */ ;
+ { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)'c');
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)'c');
+ e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_2));
+ if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(\'c\' == \'c\')"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ __gmpz_clear((__mpz_struct *)(e_acsl_2));
+ }
+
+ /*@ assert false ≢ true; */ ;
+ if (! ((int)false != (int)true)) { e_acsl_fail((char *)"(false != true)");
+ }
__retres = 0;
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.err.oracle
rename to src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.err.oracle
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
new file mode 100644
index 0000000000000000000000000000000000000000..2835d90b3ff9d7c3592f4175229af296d7f0aa52
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -0,0 +1,121 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+PROJECT_FILE.i:124:[value] Assertion got status valid.
+PROJECT_FILE.i:127:[value] Assertion got status valid.
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:129.
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:129.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:130.
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:46:[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.i:131.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+PROJECT_FILE.i:105:[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.i:132.
+PROJECT_FILE.i:39:[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.i:132.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:135:[value] Assertion got status valid.
+[value] Recording results for main
+[value] done for function main
+[from] Computing for function mpz_init_set_si
+[from] Done for function mpz_init_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 printf <-e_acsl_fail
+[from] Done for function printf
+PROJECT_FILE.i:115:[from] warning: variadic call detected. Using only 1 argument(s).
+[from] Computing for function exit <-e_acsl_fail
+[from] Done for function exit
+PROJECT_FILE.i:115:[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:
+ __retres ∈ {0}
+/* 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];
+enum bool {
+ false = 0,
+ true = 1
+};
+/*@ ensures \valid(\old(z));
+ assigns *z; */
+extern void mpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void mpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int mpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+/*@ assigns \nothing; */
+extern int printf(char const * , ...);
+void e_acsl_fail(char *msg)
+{
+ printf("%s\n",msg);
+ exit(1);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ /*@ assert "toto" ≢ "titi"; */ ;
+ if (! ("toto" != "titi")) { e_acsl_fail((char *)"(\"toto\" != \"titi\")");
+ }
+ /*@ assert 'c' ≡ 'c'; */ ;
+ { mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)'c');
+ mpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)'c');
+ e_acsl_3 = mpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_2));
+ if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(\'c\' == \'c\')"); }
+ mpz_clear((__mpz_struct *)(e_acsl_1));
+ mpz_clear((__mpz_struct *)(e_acsl_2));
+ }
+
+ /*@ assert false ≢ true; */ ;
+ if (! ((int)false != (int)true)) { e_acsl_fail((char *)"(false != true)");
+ }
+ __retres = 0;
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
deleted file mode 100644
index ad4b417cca10295f129d6ef3756158ce62da72c8..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
+++ /dev/null
@@ -1,37 +0,0 @@
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value] Values of globals at initialization
-PROJECT_FILE.i:120:[value] Assertion got status valid.
-[value] Recording results for main
-[value] done for function main
-[dominators] computing for function main
-[dominators] done for function main
-[value] ====== VALUES COMPUTED ======
-[value] Values for function main:
- __retres ∈ {0}
-/* Generated by Frama-C */
-/*@ terminates \false;
- ensures \false;
- assigns \nothing; */
-extern void exit(int status);
-/*@ assigns \nothing; */
-extern int printf(char const * , ...);
-void e_acsl_fail(char *msg)
-{
- printf("%s\n",msg);
- exit(1);
- return;
-}
-
-int main(void)
-{
- int __retres;
- /*@ assert "toto" ≢ "titi"; */ ;
- if (! ("toto" != "titi")) { e_acsl_fail((char *)"(\"toto\" != \"titi\")");
- }
- __retres = 0;
- return (__retres);
-}
-
-
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i b/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i
new file mode 100644
index 0000000000000000000000000000000000000000..b901be8d453eefde6613cc129719ba834a2fc42b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/other_constants.i
@@ -0,0 +1,13 @@
+/* run.config
+ COMMENT: non integer constants
+ EXECNOW: LOG gen_other_constants.c BIN gen_other_constants.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/other_constants.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_other_constants.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_other_constants.out -lgmp ./tests/e-acsl-runtime/result/gen_other_constants.c && ./tests/e-acsl-runtime/result/gen_other_constants.out
+*/
+
+enum bool { false, true };
+
+int main(void) {
+ /*@ assert "toto" != "titi"; */
+ /*@ assert 'c' == 'c'; */
+ /*@ assert false != true; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i b/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i
deleted file mode 100644
index 2ab8aa953abf78ee8ada641f5bda0b3df5263d93..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i
+++ /dev/null
@@ -1,8 +0,0 @@
-/* run.config
- COMMENT: string literal
- EXECNOW: LOG gen_string_literal.c BIN gen_string_literal.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/string_literal.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_string_literal.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_string_literal.out ./tests/e-acsl-runtime/result/gen_string_literal.c && ./tests/e-acsl-runtime/result/gen_string_literal.out
-*/
-int main(void) {
- /*@ assert "toto" != "titi"; */
- return 0;
-}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index e66555125949336a1063eb7d75d4d3c5c281d677..4677d7dc5b5e4fdc06be8ab2adc74a1aaab5522a 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -237,11 +237,7 @@ let constant_to_exp ?(loc=Location.unknown) = function
kinteger64_repr ?loc k n s
| ILongLong | IULongLong ->
mkString ?loc (Int64.to_string n))
- | CStr _ as c -> new_exp ?loc (Const c)
- | CWStr _ -> not_yet "wide character string constant"
- | CChr _ -> not_yet "character constant"
- | CReal _ -> not_yet "floating point constant"
- | CEnum _ -> not_yet "enum constant"
+ | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c -> new_exp ?loc (Const c)
let tlval_to_lval = function
| TVar { lv_origin = Some v }, TNoOffset -> Var v, NoOffset