diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 2dfe89528a82bccef033b2254a533c0e8ba259d9..05803bf20200ba35b968f4e3a9c805e738c91d3c 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -146,34 +146,49 @@ let fmake ulp value = match ulp with
| Float64 -> F.e_fun ~result:t64 fq64 [F.e_float value]
let qmake ulp q = fmake ulp (Q.to_float q)
-let re_mantissa = "\\([-+]?[0-9]*\\)"
-let re_comma = "\\(.\\(\\(0*[1-9]\\)*\\)0*\\)?"
-let re_exponent = "\\([eE]\\([-+]?[0-9]*\\)\\)?"
-let re_suffix = "\\([flFL]\\)?"
-let re_real =
- Str.regexp (re_mantissa ^ re_comma ^ re_exponent ^ re_suffix ^ "$")
+
+let re_float = Str.regexp ".*[fldFLD]$"
+let re_mantissa = Str.regexp "[-+]?[0-9]*"
+let re_decimal = Str.regexp "\\.[0-9]*"
+let re_exponent = Str.regexp "[eE][-+]?[0-9]*"
let parse_literal ~model v r =
try
- if Str.string_match re_real r 0 then
- let has_suffix =
- try ignore (Str.matched_group 7 r) ; true
- with Not_found -> false in
- if has_suffix && model = Float then
- Q.of_float v
- else
- let ma = Str.matched_group 1 r in
- let mb = try Str.matched_group 3 r with Not_found -> "" in
- let me = try Str.matched_group 6 r with Not_found -> "0" in
- let n = int_of_string me - String.length mb in
- let d n =
- let s = Bytes.make (succ n) '0' in
- Bytes.set s 0 '1' ; Q.of_string (Bytes.to_string s) in
- let m = Q.of_string (ma ^ mb) in
- if n < 0 then Q.div m (d (-n)) else
- if n > 0 then Q.mul m (d n) else m
- else Q.of_float v
- with Failure _ ->
+ if model = Float && Str.string_match re_float r 0 then Q.of_float v
+ else
+ begin
+ if not @@ Str.string_match re_mantissa r 0 then
+ raise Not_found ;
+ let mantissa = Str.matched_string r in
+ let p = Str.match_end () in (* length mantissa = p *)
+ let q, decimal =
+ if Str.string_match re_decimal r p then
+ let q = Str.match_end () in
+ q, String.sub r (p + 1) (q - p - 1)
+ else
+ p, "" in
+ let n, exponent =
+ if Str.string_match re_exponent r q then
+ let n = Str.match_end () in
+ n, String.sub r (q + 1) (n - q - 1)
+ else
+ q, "0" in
+ if n <> String.length r && not @@ Str.string_match re_float r n then
+ raise Not_found ;
+ let digits = Z.of_string @@ mantissa ^ decimal in
+ let decades = int_of_string exponent - String.length decimal in
+ let power n =
+ let s = Bytes.make (n+1) '0' in Bytes.set s 0 '1' ;
+ Z.of_string (String.of_bytes s) in
+ if decades < 0 then
+ Q.make digits @@ power (-decades)
+ else
+ if decades > 0 then
+ Q.of_bigint (Z.mul digits @@ power decades)
+ else
+ Q.of_bigint digits
+ end
+ with Failure _ | Not_found | Invalid_argument _ ->
Warning.error "Unexpected constant literal %S" r
let acsl_lit l =
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index fd106bfdd805723459da066371407fc91ed51114..303cbaecda2f4dd3c6fdcb11de0957c2eab4c1c8 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,8 @@
Plugin WP <next-release>
###############################################################################
+* WP [2024-07-02] Fixed parsing of decimal literals
+
###############################################################################
Plugin WP 29.0 (Copper)
###############################################################################
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/real.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/real.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6078845907f28839066740cc1b008c16b9e35618
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/real.res.oracle
@@ -0,0 +1,46 @@
+# frama-c -wp [...]
+[kernel] Parsing real.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal add_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal add_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function add
+------------------------------------------------------------
+
+Goal Check 'A' (file real.c, line 6):
+Prove: P_EQ(1234567.0, to_f64(1234567.0)).
+
+------------------------------------------------------------
+
+Goal Check 'B' (file real.c, line 8):
+Prove: P_EQ((1234567.0/100000), to_f64((6949994351454889.0/562949953421312))).
+
+------------------------------------------------------------
+
+Goal Check 'C' (file real.c, line 10):
+Prove: P_EQ((1234567.0/10), to_f64((8483879823553331.0/68719476736))).
+
+------------------------------------------------------------
+
+Goal Check 'C' (file real.c, line 12):
+Prove: P_EQ((1234567.0/1000000000),
+ to_f64((5693435372711845.0/4611686018427387904))).
+
+------------------------------------------------------------
+
+Goal Check 'D' (file real.c, line 14):
+Prove: P_EQ((1234567.0/1000), to_f64((1357420771768533.0/1099511627776))).
+
+------------------------------------------------------------
+
+Goal Check 'E' (file real.c, line 16):
+Prove: P_EQ((1234567.0/100000000000),
+ to_f64((3643798638535581.0/295147905179352825856))).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'add':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/real.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/real.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..caf23e8b061177dc25022f1cf0fa576faaa19d5d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/real.res.oracle
@@ -0,0 +1,23 @@
+# frama-c -wp [...]
+[kernel] Parsing real.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal add_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal add_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 7 goals scheduled
+[wp] [Valid] typed_add_check_A (Alt-Ergo) (Cached)
+[wp] [Valid] typed_add_check_B (Alt-Ergo) (Cached)
+[wp] [Valid] typed_add_check_C (Alt-Ergo) (Cached)
+[wp] [Valid] typed_add_check_C_2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_add_check_D (Alt-Ergo) (Cached)
+[wp] [Valid] typed_add_check_E (Alt-Ergo) (Cached)
+[wp] [Valid] typed_add_assigns (Qed)
+[wp] Proved goals: 9 / 9
+ Terminating: 1
+ Unreachable: 1
+ Qed: 1
+ Alt-Ergo: 6
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ add 1 6 7 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/real.c b/src/plugins/wp/tests/wp_acsl/real.c
new file mode 100644
index 0000000000000000000000000000000000000000..992b46f548b2794a9138b5e310cfa7944ba948a6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/real.c
@@ -0,0 +1,19 @@
+//@ predicate EQ(real a, double b) = \abs(a-b) < \max(a,b) * 1e-16 ;
+
+/*@ assigns \nothing; */
+void add(double x, double y)
+{
+ /*@ check A: EQ( 1234567,
+ 1234567.0d ); */
+ /*@ check B: EQ( 12.345670,
+ 12.345670d ); */
+ /*@ check C: EQ( 12.345670e4,
+ 12.345670e4d ); */
+ /*@ check C: EQ( 12.345670e-4,
+ 12.345670e-4d ); */
+ /*@ check D: EQ( .1234567e4,
+ .1234567e4d ); */
+ /*@ check E: EQ( .1234567e-4,
+ .1234567e-4d ); */
+ return ;
+}