diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 3ed3c866fe394ec15a07f840495937eeb709eaec..81842f01a2eb694506b55e6640baba76d03a7870 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -45,7 +45,7 @@ let ftau = function
| Float32 -> t32
| Float64 -> t64
-let suffix fmt = function
+let pp_suffix fmt = function
| Float32 -> Format.pp_print_string fmt "f32"
| Float64 -> Format.pp_print_string fmt "f64"
@@ -55,9 +55,9 @@ let link phi = Lang.infoprover (Qed.Engine.F_call phi)
let fq32 = extern_f ~library ~result:t32 ~link:(link "to_f32") "q32"
let fq64 = extern_f ~library ~result:t64 ~link:(link "to_f64") "q64"
-let f_model ft = extern_f ~library ~result:(ftau ft) "model_%a" suffix ft
-let f_delta ft = extern_f ~library ~result:(ftau ft) "delta_%a" suffix ft
-let f_epsilon ft = extern_f ~library ~result:(ftau ft) "epsilon_%a" suffix ft
+let f_model ft = extern_f ~library ~result:(ftau ft) "model_%a" pp_suffix ft
+let f_delta ft = extern_f ~library ~result:(ftau ft) "delta_%a" pp_suffix ft
+let f_epsilon ft = extern_f ~library ~result:(ftau ft) "epsilon_%a" pp_suffix ft
(* -------------------------------------------------------------------------- *)
(* --- Model Setting --- *)
@@ -138,35 +138,42 @@ let qmake ulp q = fmake ulp (Transitioning.Q.to_float q)
let mantissa = "\\([-+]?[0-9]*\\)"
let comma = "\\(.\\(\\(0*[1-9]\\)*\\)0*\\)?"
let exponent = "\\([eE]\\([-+]?[0-9]*\\)\\)?"
-let real = Str.regexp (mantissa ^ comma ^ exponent ^ "$")
+let suffix = "\\([flFL]\\)?"
+let real = Str.regexp (mantissa ^ comma ^ exponent ^ suffix ^ "$")
-let parse_literal v r =
+let parse_literal ~model v r =
try
if Str.string_match real r 0 then
- 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
+ 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 _ ->
Warning.error "Unexpected constant literal %S" r
let acsl_lit l =
let open Cil_types in
- F.e_real (parse_literal l.r_nearest l.r_literal)
+ F.e_real (parse_literal ~model:(Context.get model) l.r_nearest l.r_literal)
let code_lit ulp value original =
match Context.get model , ulp , original with
| Float , Float32 , _ -> F.e_fun fq32 [F.e_float value]
| Float , Float64 , _ -> F.e_fun fq64 [F.e_float value]
| Real , _ , None -> F.e_float value
- | Real , _ , Some r -> F.e_real (parse_literal value r)
+ | Real , _ , Some r -> F.e_real (parse_literal ~model:Real value r)
(* -------------------------------------------------------------------------- *)
(* --- Computations --- *)
@@ -199,13 +206,13 @@ let compute op ulp xs =
let make_fun_float ?result name op ft =
let result = match result with None -> ftau ft | Some r -> r in
- let phi = extern_f ~library ~result "%s_%a" name suffix ft in
+ let phi = extern_f ~library ~result "%s_%a" name pp_suffix ft in
Lang.F.set_builtin phi (compute op ft) ;
REGISTRY.define phi (op,ft) ; phi
let make_pred_float name op ft =
- let prop = Pretty_utils.sfprintf "%s_%a" name suffix ft in
- let bool = Pretty_utils.sfprintf "%s_%ab" name suffix ft in
+ let prop = Pretty_utils.sfprintf "%s_%a" name pp_suffix ft in
+ let bool = Pretty_utils.sfprintf "%s_%ab" name pp_suffix ft in
let phi = extern_p ~library ~bool ~prop () in
Lang.F.set_builtin phi (compute op ft) ;
REGISTRY.define phi (op,ft) ; phi
diff --git a/src/plugins/wp/tests/wp_plugin/float_model.i b/src/plugins/wp/tests/wp_plugin/float_model.i
new file mode 100644
index 0000000000000000000000000000000000000000..bef36ee872e1caeed67ad71211630cd9239c7e28
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/float_model.i
@@ -0,0 +1,32 @@
+/* run.config
+ OPT: -wp-model +real
+ OPT: -wp-model +float
+*/
+
+/* run.config_qualif
+ DONTRUN:
+*/
+
+//@ predicate P(real x);
+
+float FD,FF ;
+double DD,DF ;
+
+/*@
+ ensures ACSL_R: P( 2.1 );
+ ensures ACSL_F: P( 2.1f );
+ ensures ACSL_FR: P( (float) 2.1 );
+ ensures ACSL_DR: P( (double) 2.1 );
+ ensures ACSL_DF: P( (double) 2.1f );
+ ensures C_FD: P( FD );
+ ensures C_FF: P( FF );
+ ensures C_DD: P( DD );
+ ensures C_DF: P( DF );
+ */
+void job(void)
+{
+ FD = 2.1 ;
+ FF = 2.1f ;
+ DD = 2.1 ;
+ DF = 2.1f ;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a711e372d35c558c31793e43e593b585c74d4731
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_model.0.res.oracle
@@ -0,0 +1,58 @@
+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing tests/wp_plugin/float_model.i (no preprocessing)
+[kernel] tests/wp_plugin/float_model.i:10: Warning:
+ parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
+[kernel:parser:decimal-float] tests/wp_plugin/float_model.i:28: Warning:
+ Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function job
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_R' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_F' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_FR' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_DR' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_DF' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'C_FD' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'C_FF' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'C_DD' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'C_DF' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..55eefc41f89dc07ca8ef43882bed889ce252e363
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_model.1.res.oracle
@@ -0,0 +1,58 @@
+# frama-c -wp -wp-model 'Typed' [...]
+[kernel] Parsing tests/wp_plugin/float_model.i (no preprocessing)
+[kernel] tests/wp_plugin/float_model.i:10: Warning:
+ parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
+[kernel:parser:decimal-float] tests/wp_plugin/float_model.i:28: Warning:
+ Floating-point constant 2.1 is not represented exactly. Will use 0x1.0cccccccccccdp1.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function job
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_R' in 'job':
+Prove: P_P((21.0/10)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_F' in 'job':
+Prove: P_P((4404019.0/2097152)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_FR' in 'job':
+Prove: P_P((4404019.0/2097152)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_DR' in 'job':
+Prove: P_P((4728779608739021.0/2251799813685248)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'ACSL_DF' in 'job':
+Prove: P_P((4404019.0/2097152)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'C_FD' in 'job':
+Prove: P_P((4404019.0/2097152)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'C_FF' in 'job':
+Prove: P_P((4404019.0/2097152)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'C_DD' in 'job':
+Prove: P_P((4728779608739021.0/2251799813685248)).
+
+------------------------------------------------------------
+
+Goal Post-condition 'C_DF' in 'job':
+Prove: P_P((4404019.0/2097152)).
+
+------------------------------------------------------------