diff --git a/.Makefile.lint b/.Makefile.lint
index bf8a261de3b4350032ffd4d9c79c36e0868f2dbd..0fffac31e24ee1c965b48ae26c1f899d18068c78 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -13,7 +13,6 @@ ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
ML_LINT_KO+=src/kernel_internals/typing/asm_contracts.ml
ML_LINT_KO+=src/kernel_internals/typing/frontc.mli
ML_LINT_KO+=src/kernel_internals/typing/infer_annotations.ml
-ML_LINT_KO+=src/kernel_internals/typing/logic_builtin.ml
ML_LINT_KO+=src/kernel_internals/typing/mergecil.mli
ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.ml
ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.mli
diff --git a/share/libc/math.h b/share/libc/math.h
index 58f24428a0798d832c59fd09103d514169c1198c..6ae90331c2e87b965357c3ab315858a8558aae2b 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -539,6 +539,7 @@ extern long double powl(long double x, long double y);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result >= -0.;
+ ensures result_value: \result == sqrt(x);
*/
extern double sqrt(double x);
@@ -547,6 +548,7 @@ extern double sqrt(double x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result >= -0.;
+ ensures result_value: \result == sqrtf(x);
*/
extern float sqrtf(float x);
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index 3f01fbad458ebcad39e2f7929e74af758f8c4b0e..02d4a73809ef420d1086071a9ec7a73b68321e04 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -25,7 +25,7 @@
open Cil_types
let add = Logic_env.add_builtin_logic_function_gen
- Logic_utils.is_same_builtin_profile
+ Logic_utils.is_same_builtin_profile
let float_type = Ctype Cil.floatType
let double_type = Ctype Cil.doubleType
@@ -40,7 +40,7 @@ let init =
(* Since hooks are not projectified this function must be added exactly
once per session, otherwise we might end up with several built-ins with
the same name.
- *)
+ *)
fun () ->
if !called then (fun () -> ())
else begin
@@ -74,15 +74,15 @@ let init =
List.iter
(fun (typename, constrs) ->
let l =
- List.map
- (fun cname ->
+ List.map
+ (fun cname ->
let c =
{ ctor_name = cname; ctor_type = typename;
ctor_params = [] }
in
- Logic_env.add_builtin_logic_ctor cname c;
- c)
- constrs
+ Logic_env.add_builtin_logic_ctor cname c;
+ c)
+ constrs
in
typename.lt_def <- Some (LTsum l))
[ boolean, ["\\true"; "\\false"];
@@ -91,7 +91,7 @@ let init =
rounding_mode, [ "\\Up"; "\\Down"; "\\ToZero"; "\\NearestAway";
"\\NearestEven" ];
];
- (* logic types used by the builtins *)
+ (* logic types used by the builtins *)
let a_name, a_type = polymorphic_type "a" in
let boolean = Ltype(boolean,[]) in
let sign = Ltype(sign,[]) in
@@ -99,7 +99,7 @@ let init =
let rounding_mode = Ltype(rounding_mode,[]) in
let set_of_integer = Ltype (set, [Linteger]) in
let set_of_a_type = Ltype (set, [a_type]) in
- (* "\list" logic type with its constructors *)
+ (* "\list" logic type with its constructors *)
let list =
{ lt_name="\\list"; lt_params=[a_name]; lt_def=None; lt_attr=[]}
in
@@ -153,22 +153,22 @@ let init =
"\\no_overflow_single", [], [], ["m", rounding_mode; "x", Lreal] ;
"\\no_overflow_double", [], [], ["m", rounding_mode; "x", Lreal] ;
"\\subset", [a_name], [], ["s1", set_of_a_type;
- "s2", set_of_a_type];
+ "s2", set_of_a_type];
"\\pointer_comparable", [], [], [("p1", object_ptr);
- ("p2", object_ptr)];
+ ("p2", object_ptr)];
"\\pointer_comparable", [], [], [("p1", fun_ptr);
- ("p2", fun_ptr)];
+ ("p2", fun_ptr)];
"\\pointer_comparable", [], [], [("p1", fun_ptr);
- ("p2", object_ptr)];
+ ("p2", object_ptr)];
"\\pointer_comparable", [], [], [("p1", object_ptr);
- ("p2", fun_ptr)];
+ ("p2", fun_ptr)];
];
(* functions *)
List.iter
(fun (f,tparams,params,ret_type) ->
add { bl_name = f; bl_params = tparams; bl_profile = params;
bl_type = Some ret_type; bl_labels = []})
- [
+ [
"\\min", [], ["x",Linteger;"y",Linteger], Linteger ;
"\\max", [], ["x",Linteger;"y",Linteger], Linteger ;
"\\min", [], ["x",Lreal;"y",Lreal], Lreal ;
@@ -210,10 +210,12 @@ let init =
"\\pow", [], ["x",Lreal;"y",Lreal], Lreal ;
"\\fmod", [], ["x",Lreal;"y",Lreal], Lreal ;
+ "sqrt", [], ["x",double_type], double_type ;
"atan2", [], ["x",double_type;"y",double_type], double_type ;
"pow", [], ["x",double_type;"y",double_type], double_type ;
"fmod", [], ["x",double_type;"y",double_type], double_type ;
+ "sqrtf", [], ["x",float_type], float_type ;
"atan2f", [], ["x",float_type;"y",float_type], float_type ;
"powf", [], ["x",float_type;"y",float_type], float_type ;
"fmodf", [], ["x",float_type;"y",float_type], float_type ;
@@ -221,41 +223,41 @@ let init =
(* TODO ?
* div() frexp() ldexp()
* ldiv() modf() modf()
- *)
+ *)
"\\sum", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Linteger))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Linteger))], Linteger ;
"\\sum", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Lreal))], Lreal ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\product", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Linteger))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Linteger))], Linteger ;
"\\product", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Lreal))], Lreal ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\min", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Linteger))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Linteger))], Linteger ;
"\\min", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Lreal))], Lreal ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\max", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Linteger))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Linteger))], Linteger ;
"\\max", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Lreal))], Lreal ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\numof", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],boolean))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],boolean))], Linteger ;
(* for floats special values *)
- "\\round_float", [],
- ["f", float_format; "m", rounding_mode; "x", Lreal], Lreal ;
+ "\\round_float", [],
+ ["f", float_format; "m", rounding_mode; "x", Lreal], Lreal ;
"\\sign", [], ["x",float_type], sign ;
"\\sign", [], ["x",double_type], sign ;
@@ -281,27 +283,27 @@ let init =
"\\relative_error", [], ["x",double_type], Lreal;
(*"\\relative_error", [], ["x",long_double_type], Lreal;*)
- "\\round_float", [],
- ["m", rounding_mode; "x", Lreal], float_type;
- "\\round_double", [],
- ["m", rounding_mode ; "x", Lreal], double_type;
+ "\\round_float", [],
+ ["m", rounding_mode; "x", Lreal], float_type;
+ "\\round_double", [],
+ ["m", rounding_mode ; "x", Lreal], double_type;
"\\plus_infinity", [], [], float_type;
"\\minus_infinity", [], [], float_type;
"\\NaN", [], [], float_type;
- (*"\\round_quad", [],
+ (*"\\round_quad", [],
["m", rounding_mode; "x", Lreal], long_double_type;*)
"\\min", [], ["s", set_of_integer], Linteger;
"\\max", [], ["s", set_of_integer], Linteger;
"\\nth", [a_name],
- ["l", list_of_a_type; "n", Linteger], a_type;
+ ["l", list_of_a_type; "n", Linteger], a_type;
"\\length", [a_name],
- ["l", list_of_a_type], Linteger;
+ ["l", list_of_a_type], Linteger;
"\\concat", [a_name],
- ["l1", list_of_a_type; "l2", list_of_a_type], list_of_a_type;
- "\\repeat", [a_name],
- ["l", list_of_a_type; "n", Linteger], list_of_a_type;
+ ["l1", list_of_a_type; "l2", list_of_a_type], list_of_a_type;
+ "\\repeat", [a_name],
+ ["l", list_of_a_type; "n", Linteger], list_of_a_type;
]
end
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index a94bd7902e7d33bded1bd99e826ecc1820bc4190..5c3fedbea06163aeee9666481f76a5801d276d6c 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,9 @@
# configure configure
###############################################################################
+-* E-ACSL [2020/03/24] Fix automatic deactivation of plug-in Variadic when
+ E-ACSL is directly called from Frama-C without using
+ e-acsl-gcc.sh.
- E-ACSL [2020/03/10] Call E-ACSL's free functions for globals in a
separate function at the end of main.
- E-ACSL [2020/03/10] Call `__e_acsl_memory_init` only if the memory
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 3c606f3bbdf6348c9abc21e64ffd2e28db872d91..c8027aa8d6f690b468b5aae66a1e98e8e957fdfc 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -45,7 +45,7 @@ let unmemoized_extend_ast () =
(Kernel.Machdep.get ())
Datatype.Filepath.pp_abs share);
Kernel.Keep_unused_specified_functions.off ();
- if Plugin.is_present "variadic-translation" then
+ if Plugin.is_present "variadic" then
Dynamic.Parameter.Bool.off "-variadic-translation" ();
let ppc, ppk = File.get_preprocessor_command () in
let register s =
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 8ee13e2c4fef29c60271f4cafe77da9f08021d23..cb9450bce91d295514451eb251dd97f45eb31443 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -715,6 +715,8 @@ let known_logic_funs = [
"powf", ACSL;
"fmod", ACSL;
"fmodf", ACSL;
+ "sqrt", ACSL;
+ "sqrtf", ACSL;
"\\sign", ACSL;
"\\min", ACSL;
"\\max", ACSL;
@@ -1356,6 +1358,9 @@ and eval_known_logic_function ~alarm_mode env li labels args =
_, _, [arg1; arg2] ->
eval_float_builtin_arity2 ~alarm_mode env lvi.lv_name arg1 arg2
+ | ("sqrt" | "sqrtf"),_,_, [arg] ->
+ eval_float_builtin_arity1 ~alarm_mode env lvi.lv_name arg
+
| "\\sign", _, _, [arg] ->
begin
let r = eval_term ~alarm_mode env arg in
@@ -1423,6 +1428,23 @@ and eval_float_builtin_arity2 ~alarm_mode env name arg1 arg2 =
let ldeps = join_logic_deps r1.ldeps r2.ldeps in
{ etype = r1.etype; eunder; eover = v; ldeps; empty = r1.empty || r2.empty; }
+and eval_float_builtin_arity1 ~alarm_mode env name arg =
+ let fcaml = match name with
+ | "sqrt" -> Fval.sqrt Fval.Double
+ | "sqrtf" -> Fval.sqrt Fval.Single
+ | _ -> assert false
+ in
+ let r = eval_term ~alarm_mode env arg in
+ let v =
+ try
+ let i = Cvalue.V.project_ival r.eover in
+ let f = Ival.project_float i in
+ Cvalue.V.inject_float (fcaml f)
+ with Cvalue.V.Not_based_on_null ->
+ Cvalue.V.topify_arith_origin r.eover
+ in
+ let eunder = under_from_over v in
+ { etype = r.etype; eunder; eover = v; ldeps=r.ldeps; empty = r.empty; }
(* Computes the max (resp. the min) between the evaluation results [r1] and [r2]
according to [backward_left v1 v2] that reduces [v1] by assuming it is
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index acff66339965de84f233d2dec64f456ec06cf6f2..39c437ff77f71ad07bd77057f2652d8c9e10f289 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -57,6 +57,7 @@ let fq64 = extern_f ~library ~result:t64 ~link:(link "to_f64") "q64"
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
+let f_sqrt ft = extern_f ~library ~result:(ftau ft) "sqrt_%a" pp_suffix ft
(* -------------------------------------------------------------------------- *)
(* --- Model Setting --- *)
@@ -275,7 +276,11 @@ let compute_float op ulp xs =
| NEG , [ x ] -> qmake ulp (Q.neg (exact x))
| ADD , [ x ; y ] -> qmake ulp (Q.add (exact x) (exact y))
| MUL , [ x ; y ] -> qmake ulp (Q.mul (exact x) (exact y))
- | DIV , [ x ; y ] -> qmake ulp (Q.div (exact x) (exact y))
+ | DIV , [ x ; y ] ->
+ let res = match Q.div (exact x) (exact y) with
+ | x when Q.classify x = Q.NZERO -> x
+ | _ -> raise Not_found (* let Why3 take care of the division*)
+ in qmake ulp res
| ROUND , [ x ] -> round ulp x
| REAL , [ x ] -> F.e_real (exact x)
| LE , [ x ; y ] -> F.e_bool (Q.leq (exact x) (exact y))
@@ -381,12 +386,20 @@ let () = Context.register
(* --- Models --- *)
(* -------------------------------------------------------------------------- *)
+let register_c_acsl_builtin name lfun ft =
+ let name = match ft with
+ | Float32 -> name ^ "f"
+ | Float64 -> name
+ in
+ LogicBuiltins.add_builtin name [F ft] (lfun ft)
+
let () =
let open LogicBuiltins in
let register_builtin ft =
add_builtin "\\model" [F ft] (f_model ft) ;
add_builtin "\\delta" [F ft] (f_delta ft) ;
add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
+ register_c_acsl_builtin "sqrt" f_sqrt ft
in
register_builtin Float32 ;
register_builtin Float64
diff --git a/src/plugins/wp/Cfloat.mli b/src/plugins/wp/Cfloat.mli
index 8d3752605675482828518848fe4e6b346b8dd549..344ddbc093e210b08c1b87114f4252cd21da307d 100644
--- a/src/plugins/wp/Cfloat.mli
+++ b/src/plugins/wp/Cfloat.mli
@@ -34,6 +34,9 @@ val f64 : adt
val t32 : tau
val t64 : tau
+val fq32 : lfun
+val fq64 : lfun
+
type model = Real | Float
val configure : model -> WpContext.rollback
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index bf5c0054260a2191d2c4347ab095a4bff4c634dc..40f7cf42aeb0cd3a2aecd03c5dfeb61326bb5327 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -197,17 +197,18 @@ let rec varpoly k x = function
| y::ys -> if x = y then k else varpoly (succ k) x ys
type t_builtin = E_mdt of mdt | E_poly of (tau list -> tau)
+let builtin_types = Context.create "Wp.Lang.builtin_types"
-let builtins = Hashtbl.create 131
+let find_builtin name = Context.get builtin_types name
let adt lt =
- try match Hashtbl.find builtins lt.lt_name with
+ try match find_builtin lt.lt_name with
| E_mdt m -> Mtype m
| E_poly _ -> assert false
with Not_found -> Atype lt
let atype lt ts =
- try match Hashtbl.find builtins lt.lt_name with
+ try match find_builtin lt.lt_name with
| E_mdt m -> Logic.Data(Mtype m,ts)
| E_poly ftau -> ftau ts
with Not_found -> Logic.Data(Atype lt,ts)
@@ -279,30 +280,21 @@ end
(* --- Datatypes --- *)
(* -------------------------------------------------------------------------- *)
-let get_builtin_type ~name ~link ~library =
- try match Hashtbl.find builtins name with
- | E_mdt m -> Mtype m
- | E_poly _ -> assert false
- with Not_found ->
- let m = new_extern ~link ~library ~debug:name in
- Hashtbl.add builtins name (E_mdt m) ; Mtype m
-
-let set_builtin_type ~name ~link ~library =
- let m = new_extern ~link ~library ~debug:name in
- Hashtbl.add builtins name (E_mdt m)
-
-let set_builtin_poly ~name f =
- Hashtbl.add builtins name (E_poly f)
+let get_builtin_type ~name =
+ match find_builtin name with
+ | E_mdt m -> Mtype m
+ | E_poly _ -> assert false
let mem_builtin_type ~name =
- Hashtbl.mem builtins name
+ try ignore (find_builtin name) ; true
+ with Not_found -> false
-let is_builtin lt = Hashtbl.mem builtins lt.lt_name
+let is_builtin lt = mem_builtin_type lt.lt_name
let is_builtin_type ~name = function
| Data(Mtype m,_) ->
begin
- try match Hashtbl.find builtins name with
+ try match find_builtin name with
| E_mdt m0 -> m == m0
| _ -> false
with Not_found -> false
@@ -527,6 +519,9 @@ let generated_p ?context name =
m_source = generated ?context name
}
+let extern_t name ~link ~library =
+ new_extern ~link ~library ~debug:name
+
module Fun =
struct
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 96c978a24930266759ef828cf87daa3cb0ff5bf8..3a469eb93f6d2ae03392de145c08447b2b00a873 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -73,6 +73,7 @@ and field =
| Cfield of fieldinfo
and tau = (field,adt) Logic.datatype
+type t_builtin = E_mdt of mdt | E_poly of (tau list -> tau)
type lfun =
| ACSL of Cil_types.logic_info (** Registered in Definition.t,
@@ -94,11 +95,9 @@ and source =
| Extern of Engine.link extern
val mem_builtin_type : name:string -> bool
-val set_builtin_poly : name:string -> (tau list -> tau) -> unit
-val set_builtin_type : name:string -> link:string infoprover -> library:string -> unit
-val get_builtin_type : name:string -> link:string infoprover -> library:string -> adt
val is_builtin : logic_type_info -> bool
val is_builtin_type : name:string -> tau -> bool
+val get_builtin_type : name:string -> adt
val datatype : library:string -> string -> adt
val record :
link:string infoprover -> library:string -> (string * tau) list -> adt
@@ -151,6 +150,9 @@ val generated_f : ?context:bool -> ?category:lfun category ->
val generated_p : ?context:bool -> string -> lfun
+val extern_t:
+ string -> link:string infoprover -> library:library -> mdt
+
(** {2 Sorting and Typing} *)
val tau_of_comp : compinfo -> tau
@@ -174,6 +176,7 @@ val t_datatype : adt -> tau list -> tau
val pointer : (typ -> tau) Context.value (** type of pointers *)
val floats : (c_float -> tau) Context.value (** type of floats *)
val poly : string list Context.value (** polymorphism *)
+val builtin_types: (string -> t_builtin) Context.value (* builtin types *)
val parameters : (lfun -> sort list) -> unit (** definitions *)
val name_of_lfun : lfun -> string
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 23138d3e16679e8a7f7572beab592b6d09d78b4b..e713b74ade46db3ccab2d7746acc4c613061270b 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -106,6 +106,7 @@ type driver = {
description : string;
includes : string list;
hlogic : (string , sigfun list) Hashtbl.t;
+ htypes : (string , t_builtin) Hashtbl.t;
hdeps : (string, string list) Hashtbl.t;
hoptions :
(string (* library *) * string (* group *) * string (* name *), string list)
@@ -140,7 +141,9 @@ let lookup_driver name kinds =
else Warning.error "Builtin %s undefined with signature %a" name
pp_kinds kinds
with Not_found ->
- if name.[0] == '\\' then
+ if Logic_env.is_builtin_logic_function name
+ || Logic_env.is_builtin_logic_ctor name
+ then
Warning.error "Builtin %s%a not defined" name pp_kinds kinds
else
ACSLDEF
@@ -168,6 +171,12 @@ let register ?source name kinds link =
let entry = (kinds,link) in
Hashtbl.add driver.hlogic name (entry::sigs)
+let register_type ?source name builtin =
+ let driver = cdriver_rw () in
+ if Hashtbl.mem driver.htypes name then
+ Wp_parameters.warning ?source "Redifinition of type %s" name ;
+ Hashtbl.add driver.htypes name builtin
+
let iter_table f =
let items = ref [] in
Hashtbl.iter
@@ -239,12 +248,12 @@ let add_ctor ~source name kinds ~library ~link () =
let lfun = Lang.extern_s ~library ~category ~params ~link name in
register ~source name kinds (LFUN lfun)
-let add_type ~source name ~library ?(link=Lang.infoprover name) () =
- if Lang.mem_builtin_type ~name then
- Wp_parameters.warning ~source "Redefinition of type '%s'" name ;
- Lang.set_builtin_type ~name ~library ~link
+let add_type ?source name ~library ?(link=Lang.infoprover name) () =
+ let mdt = Lang.extern_t name ~link ~library in
+ register_type ?source name (E_mdt mdt)
-let hack_type name poly = Lang.set_builtin_poly ~name poly
+let hack_type name poly =
+ register_type name (E_poly poly)
type sanitizer = driver_dir:string -> string -> string
let sanitizers : ( string * string , sanitizer ) Hashtbl.t = Hashtbl.create 10
@@ -298,6 +307,7 @@ let builtin_driver = {
description = "builtin driver";
includes = [];
hlogic = Hashtbl.create 131;
+ htypes = Hashtbl.create 131;
hdeps = Hashtbl.create 31;
hoptions = Hashtbl.create 131;
locked = false
@@ -310,6 +320,25 @@ let add_builtin name kinds lfun =
else
Context.bind driver builtin_driver (register name kinds) phi
+let add_type ?source name ~library ?link () =
+ if Context.defined driver then
+ add_type ?source name ~library ?link ()
+ else
+ Context.bind driver builtin_driver
+ (add_type ?source name ~library ?link) ()
+
+let hack_type name poly =
+ if Context.defined driver then hack_type name poly
+ else Context.bind driver builtin_driver hack_type name poly
+
+let find_type name =
+ Hashtbl.find (cdriver_ro ()).htypes name
+let find_type name =
+ if Context.defined driver then find_type name
+ else Context.bind driver builtin_driver find_type name
+
+let () = Context.set Lang.builtin_types find_type
+
let new_driver ~id ?(base=builtin_driver)
?(descr=id) ?(includes=[]) ?(configure=fun () -> ()) () =
lock base ;
@@ -318,6 +347,7 @@ let new_driver ~id ?(base=builtin_driver)
description = descr ;
includes = includes @ base.includes ;
hlogic = Hashtbl.copy base.hlogic ;
+ htypes = Hashtbl.copy base.htypes ;
hdeps = Hashtbl.copy base.hdeps ;
hoptions = Hashtbl.copy base.hoptions ;
locked = false
diff --git a/src/plugins/wp/LogicBuiltins.mli b/src/plugins/wp/LogicBuiltins.mli
index c4e8968dd46e252dcefd9fbb82527e60dd4f15fc..eb0c6d9045dd42be3f14bf07e440d8c4b3e1da23 100644
--- a/src/plugins/wp/LogicBuiltins.mli
+++ b/src/plugins/wp/LogicBuiltins.mli
@@ -77,7 +77,7 @@ val add_library : string -> string list -> unit
val add_alias : source:Filepath.position -> string -> kind list -> alias:string -> unit -> unit
-val add_type : source:Filepath.position -> string -> library:string ->
+val add_type : ?source:Filepath.position -> string -> library:string ->
?link:string infoprover -> unit -> unit
val add_ctor : source:Filepath.position -> string -> kind list ->
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 865e02c4717236e7ba3495854deb7de8da5686e7..520183929b0cc69aedd532df1ccfc4dbd2f812e2 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -113,39 +113,6 @@ let t_app ~cnv ~f ~l ~p tl =
let t_app' ~cnv ~f ~l ~p tl ty =
Why3.Term.t_app (get_ls ~cnv ~f ~l ~p) tl ty
-(** Conversion *)
-
-(* why3 1.3 *)
-let const_int (z:Z.t) =
- Why3.(Term.t_const Constant.(int_const (BigInt.of_string (Z.to_string z)))) Why3.Ty.ty_int
-
-let const_real ~cnv (q:Q.t) =
- let mk_real_int z =
- let c = Why3.Constant.real_const (Why3.BigInt.of_string (Z.to_string z)) in
- Why3.(Term.t_const c) Why3.Ty.ty_real
- in
- if Z.equal Z.one q.den
- then mk_real_int q.num
- else
- t_app ~cnv ~f:["real"] ~l:"Real" ~p:["infix /"] [mk_real_int q.num;mk_real_int q.den]
-
- (*
-let const_int (z:Z.t) =
- Why3.(Term.t_const Number.(const_of_big_int (BigInt.of_string (Z.to_string z)))) Why3.Ty.ty_int
-
-let const_real ~cnv (q:Q.t) =
- let mk_real_int z =
- let rc_negative = Z.sign z < 0 in
- let z = Z.abs z in
- let rc_abs = Why3.Number.real_const_dec (Z.to_string z) "" None in
- let c = Why3.Number.ConstReal { Why3.Number.rc_negative; rc_abs } in
- Why3.(Term.t_const c) Why3.Ty.ty_real
- in
- if Z.equal Z.one q.den
- then mk_real_int q.num
- else
- t_app ~cnv ~f:["real"] ~l:"Real" ~p:["infix /"] [mk_real_int q.num;mk_real_int q.den]
- *)
(** fold map list of at least one element *)
let fold_map map fold = function
| [] -> assert false (** absurd: forbidden by qed *)
@@ -269,6 +236,68 @@ let rec of_tau ~cnv (t:Lang.F.tau) =
| Record _ ->
why3_failure "Type %a not (yet) convertible" Lang.F.pp_tau t
+module Literal = struct
+ let const_int (z:Z.t) =
+ Why3.(Term.t_const Constant.(const_of_big_int (BigInt.of_string (Z.to_string z)))) Why3.Ty.ty_int
+
+ let why3_real ty ~use_hex sign integer decimal exp =
+ let rc = Why3.Number.ConstReal {
+ rc_negative = sign ;
+ rc_abs =
+ if use_hex then Why3.Number.real_const_hex integer decimal exp
+ else Why3.Number.real_const_dec integer decimal exp
+ } in
+ Why3.Term.t_const rc ty
+
+ let const_real ~cnv (q:Q.t) =
+ let mk_real_int z =
+ let use_hex = false in
+ let str = Z.to_string (Z.abs z) in
+ why3_real Why3.Ty.ty_real ~use_hex (Z.sign z < 0) str "" None
+ in
+ if Z.equal Z.one q.den
+ then mk_real_int q.num
+ else
+ t_app ~cnv ~f:["real"] ~l:"Real" ~p:["infix /"] [mk_real_int q.num;mk_real_int q.den]
+
+ let cfloat_of_tau tau =
+ if Lang.F.Tau.equal tau Cfloat.t32 then Ctypes.Float32
+ else if Lang.F.Tau.equal tau Cfloat.t64 then Ctypes.Float64
+ else raise Not_found
+
+ let float_literal_from_q ~cnv tau q =
+ let use_hex = true in
+ let f = match cfloat_of_tau tau with
+ | Float32 -> Floating_point.round_to_single_precision_float (Q.to_float q)
+ | Float64 -> Q.to_float q
+ in
+ let s = Format.asprintf "%a" (Floating_point.pretty_normal ~use_hex) f in
+ let re_float =
+ Str.regexp "-?0x\\([0-9a-f]+\\).\\([0-9a-f]+\\)?p?\\([+-]?[0-9a-f]+\\)?$"
+ in
+ if Str.string_match re_float s 0 then
+ let group n r = try Str.matched_group n r with Not_found -> "" in
+ let (i,d,e) = (group 1 s), (group 2 s), (group 3 s) in
+ let e = if String.equal e "" then None else Some e in
+ let t = Extlib.the (of_tau ~cnv tau) in
+ why3_real t ~use_hex (Q.sign q < 0) i d e
+ else raise Not_found
+
+ let const_float ~cnv tau (repr:Lang.F.QED.repr) =
+ match repr with
+ | Fun(f, [x]) when Lang.Fun.(equal f Cfloat.fq32 || equal f Cfloat.fq64) ->
+ begin match Lang.F.repr x with
+ | Kreal q -> float_literal_from_q ~cnv tau q
+ | _ -> raise Not_found
+ end
+ | _ -> raise Not_found
+
+ let is_float_literal ~cnv tau repr =
+ try (ignore (const_float ~cnv tau repr) ; true)
+ with Not_found | Why3.Number.NonRepresentableFloat _ -> false
+
+end
+
let rec full_trigger = function
| Qed.Engine.TgAny -> false
| TgVar _ -> true
@@ -339,15 +368,17 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| True, _, Bool -> Why3.Term.t_bool_true
| False, _, Prop -> Why3.Term.t_false
| False, _, Bool -> Why3.Term.t_bool_false
- | Kint z, Int, _ -> coerce ~cnv sort expected $ const_int z
- | Kreal q, Real, _ -> coerce ~cnv sort expected $ const_real ~cnv q
+ | Kint z, Int, _ -> coerce ~cnv sort expected $ Literal.const_int z
+ | Kreal q, Real, _ -> coerce ~cnv sort expected $ Literal.const_real ~cnv q
+ | repr, t, _ when Literal.is_float_literal ~cnv t repr ->
+ coerce ~cnv sort expected $ Literal.const_float ~cnv t repr
| Times(z,t), Int, _ ->
coerce ~cnv sort expected $
- t_app ~cnv ~f:["int"] ~l:"Int" ~p:["infix *"] [const_int z; of_term cnv sort t]
+ t_app ~cnv ~f:["int"] ~l:"Int" ~p:["infix *"] [Literal.const_int z; of_term cnv sort t]
| Times(z,t), Real, _ ->
coerce ~cnv sort expected $
t_app ~cnv ~f:["real"] ~l:"Real" ~p:["infix *"]
- [const_real ~cnv (Q.of_bigint z); of_term cnv sort t]
+ [Literal.const_real ~cnv (Q.of_bigint z); of_term cnv sort t]
| Add l, Int, _ ->
coerce ~cnv sort expected $
t_app_fold ~f:["int"] ~l:"Int" ~p:["infix +"] ~cnv sort l
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 338ce8992abfb449129aa056505c2f8234dd4d50..40238be85bde3c5c429b26cdc1cad0fe961e7e26 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -53,7 +53,8 @@ let l_repeat = Lang.(E.({
(*--- Typechecking ---*)
-let a_list = Lang.get_builtin_type ~library ~name:t_list ~link:l_list
+let () = LogicBuiltins.add_type t_list ~library ~link:l_list ()
+let a_list = Lang.get_builtin_type t_list
let vlist_get_tau = function
| None -> invalid_arg "a list operator without result type"
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
index 5868a5a1ab2bc11e06fc62f2092d419763125719..aaedd4489efc3d61a0113eca8f6e2a3265efe616 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
@@ -26,189 +26,126 @@
theory Cfloat
- use bool.Bool
- use real.RealInfix
use real.Abs
- use real.Square
- use real.FromInt
+ use ieee_float.RoundingMode as Rounding
+ use ieee_float.Float32 as F32
+ use ieee_float.Float64 as F64
+ use ieee_float.FloatConverter as Cnv
+ use real.RealInfix
(* -------------------------------------------------------------------------- *)
(* --- C-Integer Arithmetics for Alt-Ergo --- *)
(* -------------------------------------------------------------------------- *)
- type f32 (* single precision IEEE *)
- type f64 (* double precision IEEE *)
+ type f32 = F32.t (* single precision IEEE *)
+ type f64 = F64.t (* double precision IEEE *)
(* C-Float Conversion *)
- function to_f32 real : f32
- function of_f32 f32 : real
-
- function to_f64 real : f64
- function of_f64 f64 : real
-
- axiom to_f32_zero: of_f32 (to_f32 0.0) = 0.0
- axiom to_f32_one: of_f32 (to_f32 1.0) = 1.0
- axiom to_f64_zero: of_f64 (to_f64 0.0) = 0.0
- axiom to_f64_one: of_f64 (to_f64 1.0) = 1.0
-
- (* C-Float Rounding Modes *)
-
- type rounding_mode = Up | Down | ToZero | NearestTiesToAway | NearestTiesToEven
-
- function round_float rounding_mode real : f32
- function round_double rounding_mode real : f64
-
- axiom float_32:
- forall x:real [ round_float NearestTiesToEven x ].
- to_f32 x = round_float NearestTiesToEven x
-
- axiom float_64:
- forall x:real [ round_double NearestTiesToEven x ].
- to_f64 x = round_double NearestTiesToEven x
+ function of_f32 (f: f32) : real = F32.t'real f
+ function of_f64 (d: f64) : real = F64.t'real d
(* C-Float Classification *)
- type float_kind = Finite | NaN | Inf_pos | Inf_neg
+ predicate is_finite_f32 (f:f32) = F32.t'isFinite f
+ predicate is_NaN_f32 (f:f32) = F32.is_nan f
+ predicate is_infinite_f32 (f: f32) = F32.is_infinite f
+ predicate is_positive_infinite_f32 (f: f32) = F32.is_plus_infinity f
+ predicate is_negative_infinite_f32 (f: f32) = F32.is_minus_infinity f
- function classify_f32 f32 : float_kind
- function classify_f64 f64 : float_kind
+ predicate is_finite_f64 (d:f64) = F64.t'isFinite d
+ predicate is_NaN_f64 (d:f64) = F64.is_nan d
+ predicate is_infinite_f64 (d: f64) = F64.is_infinite d
+ predicate is_positive_infinite_f64 (d: f64) = F64.is_plus_infinity d
+ predicate is_negative_infinite_f64 (d: f64) = F64.is_minus_infinity d
- predicate is_finite_f32 (f:f32) = (classify_f32 f = Finite)
- predicate is_finite_f64 (d:f64) = (classify_f64 d = Finite)
+ (* To_float *)
- predicate is_NaN_f32 (f:f32) = (classify_f32 f = NaN)
- predicate is_NaN_f64 (d:f64) = (classify_f64 d = NaN)
-
- predicate is_infinite_f32 (f:f32) = (classify_f32 f = Inf_pos || classify_f32 f = Inf_neg)
- predicate is_infinite_f64 (d:f64) = (classify_f64 d = Inf_pos || classify_f64 d = Inf_neg)
-
- predicate is_positive_infinite_f32 (f:f32) = (classify_f32 f = Inf_pos)
- predicate is_positive_infinite_f64 (d:f64) = (classify_f64 d = Inf_pos)
+ function to_f32 real : f32
+ function to_f64 real : f64
- predicate is_negative_infinite_f32 (f:f32) = (classify_f32 f = Inf_neg)
- predicate is_negative_infinite_f64 (d:f64) = (classify_f64 d = Inf_neg)
+ axiom to_float_is_finite_32: forall f:f32. is_finite_f32(f) -> F32.eq (to_f32( of_f32 f )) f
+ axiom to_f32_range_round: forall x. F32.in_range x -> of_f32 (to_f32 x) = F32.round Rounding.RNE x
+ axiom to_f32_range_finite: forall x. F32.in_range x -> is_finite_f32 (to_f32 x)
+ axiom to_f32_minus_infinity: forall x. x <. -. F32.max_real -> is_negative_infinite_f32 (to_f32 x)
+ axiom to_f32_plus_infinity: forall x. x >. F32.max_real -> is_positive_infinite_f32 (to_f32 x)
- axiom is_finite_to_float_32 :
- forall x:real [is_finite_f32(to_f32 x)]. is_finite_f32 (to_f32 x)
+ axiom to_float_is_finite_64: forall f:f64. is_finite_f64(f) -> F64.eq (to_f64( of_f64 f )) f
+ axiom to_f64_range_round: forall x. F64.in_range x -> of_f64 (to_f64 x) = F64.round Rounding.RNE x
+ axiom to_f64_range_finite: forall x. F64.in_range x -> is_finite_f64 (to_f64 x)
+ axiom to_f64_minus_infinity: forall x. x <. -. F64.max_real -> is_negative_infinite_f64 (to_f64 x)
+ axiom to_f64_plus_infinity: forall x. x >. F64.max_real -> is_positive_infinite_f64 (to_f64 x)
- axiom is_finite_to_float_64 :
- forall x:real [is_finite_f64(to_f64 x)]. is_finite_f64 (to_f64 x)
+ (* Take care of +0/-0 *)
+ axiom is_zero_to_f32_zero: F32.is_zero (to_f32 0.0)
+ axiom is_zero_to_f64_zero: F64.is_zero (to_f64 0.0)
- axiom to_float_is_finite_32 :
- forall f:f32 [ to_f32( of_f32 f ) | is_finite_f32(f) ]. is_finite_f32(f) -> to_f32( of_f32 f ) = f
+ lemma real_0_is_zero_f32: forall f:f32. 0.0 = of_f32 f -> F32.is_zero f
+ lemma real_0_is_zero_f64: forall f:f64. 0.0 = of_f64 f -> F64.is_zero f
- axiom to_float_is_finite_64 :
- forall d:f64 [ to_f64( of_f64 d ) | is_finite_f64(d) ]. is_finite_f64(d) -> to_f64( of_f64 d ) = d
+ (* Conversions *)
+ axiom f32_to_f64:
+ forall f:f32 [to_f64 (of_f32 f)]. to_f64 (of_f32 f) = Cnv.to_float64 Rounding.RNE f
+ axiom f64_to_f32:
+ forall f:f64 [to_f32 (of_f64 f)]. to_f32 (of_f64 f) = Cnv.to_float32 Rounding.RNE f
(* Finite Constants *)
predicate finite (x:real) = (is_finite_f32 (to_f32 x)) /\ (is_finite_f64 (to_f64 x))
- constant max_f32 : real = 340282346600000016151267322115014000640.0
- constant max_f64 : real = 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0
-
- axiom finite_small_f32 : forall x:real. -. max_f64 <=. x <=. max_f32 -> is_finite_f32(to_f32 x)
- axiom finite_small_f64 : forall x:real. -. max_f64 <=. x <=. max_f64 -> is_finite_f64(to_f64 x)
- axiom finite_range_f32 : forall f:f32. is_finite_f32(f) <-> -. max_f32 <=. of_f32 f <=. max_f32
- axiom finite_range_f64 : forall d:f64. is_finite_f64(d) <-> -. max_f64 <=. of_f64 d <=. max_f64
-
(* Equal *)
- function eq_f32b (x:f32) (y:f32) : bool
- function eq_f64b (x:f64) (y:f64) : bool
- predicate eq_f32 (x:f32) (y:f32) = (eq_f32b x y = true)
- predicate eq_f64 (x:f64) (y:f64) = (eq_f64b x y = true)
- axiom eq_finite_f32 : forall x,y:f32 [eq_f32 x y]. is_finite_f32 x -> is_finite_f32 y ->
- eq_f32 x y <-> of_f32 x = of_f32 y
-
- axiom eq_finite_f64 : forall x,y:f64 [eq_f64 x y]. is_finite_f64 x -> is_finite_f64 y ->
- eq_f64 x y <-> of_f64 x = of_f64 y
+ predicate eq_f32 (x:f32) (y:f32) = F32.eq x y
+ predicate eq_f64 (x:f64) (y:f64) = F64.eq x y
+ function eq_f32b (x:f32) (y:f32) : bool = eq_f32 x y
+ function eq_f64b (x:f64) (y:f64) : bool = eq_f64 x y
(* Not Equal *)
- function ne_f32b (x:f32) (y:f32) : bool
- function ne_f64b (x:f64) (y:f64) : bool
- predicate ne_f32 (x:f32) (y:f32) = (ne_f32b x y = true)
- predicate ne_f64 (x:f64) (y:f64) = (ne_f64b x y = true)
+ predicate ne_f32 (x:f32) (y:f32) = not (eq_f32 x y)
+ predicate ne_f64 (x:f64) (y:f64) = not (eq_f64 x y)
+ function ne_f32b (x:f32) (y:f32) : bool = ne_f32 x y
+ function ne_f64b (x:f64) (y:f64) : bool = ne_f64 x y
- axiom ne_finite_f32 : forall x,y:f32 [ne_f32 x y]. is_finite_f32 x -> is_finite_f32 y ->
- ne_f32 x y <-> of_f32 x <> of_f32 y
-
- axiom ne_finite_f64 : forall x,y:f64 [ne_f64 x y]. is_finite_f64 x -> is_finite_f64 y ->
- ne_f64 x y <-> of_f64 x <> of_f64 y
(* Comparison (<=) *)
- function le_f32b (x:f32) (y:f32) : bool
- function le_f64b (x:f64) (y:f64) : bool
- predicate le_f32 (x:f32) (y:f32) = (le_f32b x y = true)
- predicate le_f64 (x:f64) (y:f64) = (le_f64b x y = true)
+ predicate le_f32 (x:f32) (y:f32) = F32.le x y
+ predicate le_f64 (x:f64) (y:f64) = F64.le x y
+ function le_f32b (x:f32) (y:f32) : bool = le_f32 x y
+ function le_f64b (x:f64) (y:f64) : bool = le_f64 x y
- axiom le_finite_f32 : forall x,y:f32 [le_f32 x y]. is_finite_f32 x -> is_finite_f32 y ->
- le_f32 x y <-> of_f32 x <=. of_f32 y
- axiom le_finite_f64 : forall x,y:f64 [le_f64 x y]. is_finite_f64 x -> is_finite_f64 y ->
- le_f64 x y <-> of_f64 x <=. of_f64 y
(* Comparison (<) *)
- function lt_f32b (x:f32) (y:f32) : bool
- function lt_f64b (x:f64) (y:f64) : bool
- predicate lt_f32 (x:f32) (y:f32) = (lt_f32b x y = true)
- predicate lt_f64 (x:f64) (y:f64) = (lt_f64b x y = true)
-
- axiom lt_finite_f32 : forall x,y:f32 [lt_f32 x y]. is_finite_f32 x -> is_finite_f32 y ->
- lt_f32 x y <-> of_f32 x <. of_f32 y
-
- axiom lt_finite_f64 : forall x,y:f64 [lt_f64 x y]. is_finite_f64 x -> is_finite_f64 y ->
- lt_f64 x y <-> of_f64 x <. of_f64 y
+ predicate lt_f32 (x:f32) (y:f32) = F32.lt x y
+ predicate lt_f64 (x:f64) (y:f64) = F64.lt x y
+ function lt_f32b (x:f32) (y:f32) : bool = lt_f32 x y
+ function lt_f64b (x:f64) (y:f64) : bool = lt_f64 x y
(* Negation *)
-
- function neg_f32 (x:f32) : f32
- function neg_f64 (x:f64) : f64
-
- axiom neg_finite_f32 : forall x:f32 [neg_f32 x]. is_finite_f32 x -> of_f32 (neg_f32 x) = -. (of_f32 x)
- axiom neg_finite_f64 : forall x:f64 [neg_f64 x]. is_finite_f64 x -> of_f64 (neg_f64 x) = -. (of_f64 x)
+ function neg_f32 (x:f32) : f32 = F32.neg x
+ function neg_f64 (x:f64) : f64 = F64.neg x
(* Addition *)
- function add_f32 (x:f32) (y:f32) : f32
- function add_f64 (x:f64) (y:f64) : f64
+ function add_f32 (x:f32) (y:f32) : f32 = F32.(.+) x y
+ function add_f64 (x:f64) (y:f64) : f64 = F64.(.+) x y
- axiom add_finite_f32 : forall x,y:f32 [add_f32 x y]. is_finite_f32 x -> is_finite_f32 y ->
- add_f32 x y = to_f32 (of_f32 x +. of_f32 y)
-
- axiom add_finite_f64 : forall x,y:f64 [add_f64 x y]. is_finite_f64 x -> is_finite_f64 y ->
- add_f64 x y = to_f64 (of_f64 x +. of_f64 y)
(* Multiplication *)
- function mul_f32 (x:f32) (y:f32) : f32
- function mul_f64 (x:f64) (y:f64) : f64
-
- axiom mul_finite_f32 : forall x,y:f32 [mul_f32 x y]. is_finite_f32 x -> is_finite_f32 y ->
- mul_f32 x y = to_f32 (of_f32 x *. of_f32 y)
+ function mul_f32 (x:f32) (y:f32) : f32 = F32.(.-) x y
+ function mul_f64 (x:f64) (y:f64) : f64 = F64.(.-) x y
- axiom mul_finite_f64 : forall x,y:f64 [mul_f64 x y]. is_finite_f64 x -> is_finite_f64 y ->
- mul_f64 x y = to_f64 (of_f64 x *. of_f64 y)
(* Division *)
- function div_f32 (x:f32) (y:f32) : f32
- function div_f64 (x:f64) (y:f64) : f64
-
- axiom div_finite_f32 : forall x,y:f32 [div_f32 x y]. is_finite_f32 x -> is_finite_f32 y ->
- div_f32 x y = to_f32 (of_f32 x /. of_f32 y)
-
- axiom div_finite_f64 : forall x,y:f64 [div_f64 x y]. is_finite_f64 x -> is_finite_f64 y ->
- div_f64 x y = to_f64 (of_f64 x /. of_f64 y)
+ function div_f32 (x:f32) (y:f32) : f32 = F32.(./) x y
+ function div_f64 (x:f64) (y:f64) : f64 = F64.(./) x y
(* Square Root *)
- function sqrt_f32 f32 : f32
- function sqrt_f64 f64 : f64
-
- axiom sqrt_finite_f32 : forall x:f32 [sqrt_f32 x]. is_finite_f32 x -> sqrt_f32 x = to_f32 (sqrt (of_f32 x))
- axiom sqrt_finite_f64 : forall x:f64 [sqrt_f64 x]. is_finite_f64 x -> sqrt_f64 x = to_f64 (sqrt (of_f64 x))
+ function sqrt_f32 (x: f32) : f32 = F32.sqrt Rounding.RNE x
+ function sqrt_f64 (x: f64) : f64 = F64.sqrt Rounding.RNE x
(* Models *)
diff --git a/src/plugins/wp/tests/wp_acsl/float_const.i b/src/plugins/wp/tests/wp_acsl/float_const.i
new file mode 100644
index 0000000000000000000000000000000000000000..9becb069d883cc189ca38aca1ec3a959599de6f3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_const.i
@@ -0,0 +1,25 @@
+/* run.config
+ OPT:-wp-gen -wp-prover=why3 -wp-msg-key=print-generated -kernel-warn-key parser:decimal-float=active
+*/
+/* run.config_qualif
+ OPT:
+*/
+
+void float_convertible(float f){
+ double d = f ;
+ if(f == 0.1f){
+ //@ check f != 0.1 ;
+ //@ check f == (float)0.1 ;
+ //@ check f != (double)0.1 ;
+ //@ check (float) d == f ;
+ }
+}
+void double_convertible(double d){
+ double x = (float) d ;
+ if(d == 0.1){
+ //@ check d != 0.1 ;
+ //@ check d == (double)0.1 ;
+ //@ check d != (float)0.1 ;
+ //@ check x == (float) d ;
+ }
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..36c2f74c36303b6d9ffb3c4b171977fe6cc9e4ed
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
@@ -0,0 +1,326 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/float_const.i (no preprocessing)
+[kernel:parser:decimal-float] tests/wp_acsl/float_const.i:10: Warning:
+ Floating-point constant 0.1f is not represented exactly. Will use 0x1.99999a0000000p-4.
+[kernel:parser:decimal-float] tests/wp_acsl/float_const.i:19: Warning:
+ Floating-point constant 0.1 is not represented exactly. Will use 0x1.999999999999ap-4.
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 8 goals scheduled
+[wp:print-generated]
+ theory WP
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t.
+ let r = of_f32 (to_f32 (of_f64 f)) in
+ eq_f64 f (0x1.999999999999ap-4:t) -> of_f64 (to_f64 r) = r
+ end
+[wp:print-generated]
+ theory WP1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t.
+ eq_f64 f (0x1.999999999999ap-4:t) ->
+ not of_f64 f = (13421773.0 / 134217728.0)
+ end
+[wp:print-generated]
+ theory WP2
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t.
+ eq_f64 f (0x1.999999999999ap-4:t) ->
+ of_f64 f = (3602879701896397.0 / 36028797018963968.0)
+ end
+[wp:print-generated]
+ theory WP3
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use real.Abs *)
+
+ (* use frama_c_wp.cmath.Cmath *)
+
+ (* use real.Square *)
+
+ (* use frama_c_wp.cmath.Square1 *)
+
+ (* use frama_c_wp.cfloat.Cfloat *)
+
+ goal wp_goal :
+ forall f:t.
+ eq_f64 f (0x1.999999999999ap-4:t) -> not of_f64 f = (1.0 / 10.0)
+ end
+[wp:print-generated]
+ theory WP4
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ let r = of_f321 f in
+ eq_f32 f (0x1.99999a0000000p-4:t1) ->
+ of_f321 (to_f321 (of_f641 (to_f641 r))) = r
+ end
+[wp:print-generated]
+ theory WP5
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 f (0x1.99999a0000000p-4:t1) ->
+ not of_f321 f = (3602879701896397.0 /' 36028797018963968.0)
+ end
+[wp:print-generated]
+ theory WP6
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 f (0x1.99999a0000000p-4:t1) ->
+ of_f321 f = (13421773.0 /' 134217728.0)
+ end
+[wp:print-generated]
+ theory WP7
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool1 *)
+
+ (* use int.Int1 *)
+
+ (* use int.ComputerDivision1 *)
+
+ (* use real.RealInfix1 *)
+
+ (* use frama_c_wp.qed.Qed1 *)
+
+ (* use map.Map1 *)
+
+ (* use real.Abs1 *)
+
+ (* use frama_c_wp.cmath.Cmath1 *)
+
+ (* use real.Square2 *)
+
+ (* use frama_c_wp.cmath.Square3 *)
+
+ (* use frama_c_wp.cfloat.Cfloat1 *)
+
+ goal wp_goal :
+ forall f:t1.
+ eq_f32 f (0x1.99999a0000000p-4:t1) -> not of_f321 f = (1.0 /' 10.0)
+ end
+[wp] 8 goals generated
+------------------------------------------------------------
+ Function double_convertible
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 20):
+Assume {
+ (* Then *)
+ Have: eq_f64(d, to_f64((3602879701896397.0/36028797018963968))).
+}
+Prove: of_f64(d) != (1.0/10).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 21):
+Assume {
+ (* Then *)
+ Have: eq_f64(d, to_f64((3602879701896397.0/36028797018963968))).
+}
+Prove: of_f64(d) = (3602879701896397.0/36028797018963968).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 22):
+Assume {
+ (* Then *)
+ Have: eq_f64(d, to_f64((3602879701896397.0/36028797018963968))).
+}
+Prove: of_f64(d) != (13421773.0/134217728).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 23):
+Let r = of_f32(to_f32(of_f64(d))).
+Assume {
+ (* Then *)
+ Have: eq_f64(d, to_f64((3602879701896397.0/36028797018963968))).
+}
+Prove: of_f64(to_f64(r)) = r.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function float_convertible
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 11):
+Assume { (* Then *) Have: eq_f32(f, to_f32((13421773.0/134217728))). }
+Prove: of_f32(f) != (1.0/10).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 12):
+Assume { (* Then *) Have: eq_f32(f, to_f32((13421773.0/134217728))). }
+Prove: of_f32(f) = (13421773.0/134217728).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 13):
+Assume { (* Then *) Have: eq_f32(f, to_f32((13421773.0/134217728))). }
+Prove: of_f32(f) != (3602879701896397.0/36028797018963968).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/float_const.i, line 14):
+Let r = of_f32(f).
+Assume { (* Then *) Have: eq_f32(f, to_f32((13421773.0/134217728))). }
+Prove: of_f32(to_f32(of_f64(to_f64(r)))) = r.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ba6653276cc75ae8be4101cb33aa82a76395cc3b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/unsupported_builtin.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_acsl/unsupported_builtin.i:10: Warning:
+ No code nor implicit assigns clause for function foo, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/unsupported_builtin.i:7: Warning:
+ Builtin unimplemented_builtin not defined
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_acsl/unsupported_builtin.i, line 12):
+tests/wp_acsl/unsupported_builtin.i:7: warning from wp:
+ - Warning: Ignored Hypothesis
+ Reason: Builtin unimplemented_builtin not defined
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
index d94b1a0dbd8aa0ee3398624d9296661efe681123..cb949a9f9545c5163da4efda55c2ac57205e9b0b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.res.oracle
@@ -5,7 +5,7 @@
[wp] Warning: Missing RTE guards
[wp] 19 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_finite_32_64 : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_finite_32_64_real : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lemma_finite_32_64_real : Valid
[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare : Valid
[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare_greater : Valid
[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare : Valid
@@ -23,12 +23,12 @@
[wp] [Alt-Ergo] Goal typed_cmp_ff_ensures_REL2 : Valid
[wp] [Qed] Goal typed_cmp_fnan_ensures_POS : Valid
[wp] [Qed] Goal typed_cmp_fnan_ensures_NEG : Valid
-[wp] Proved goals: 18 / 19
+[wp] Proved goals: 19 / 19
Qed: 2
- Alt-Ergo: 16 (unsuccess: 1)
+ Alt-Ergo: 17
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma - 5 6 83.3%
+ Lemma - 6 6 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
cmp_ff - 3 3 100%
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/211e52458be3c1ae451dfd1d012b443d.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/211e52458be3c1ae451dfd1d012b443d.json
new file mode 100644
index 0000000000000000000000000000000000000000..74f5bb38c308ea0290053e5f8b87e1a39cc3d4a4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/211e52458be3c1ae451dfd1d012b443d.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.4341,
+ "steps": 1458 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/3744b87afb2193c88857aec75c88378c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/3744b87afb2193c88857aec75c88378c.json
new file mode 100644
index 0000000000000000000000000000000000000000..3f3afe181dbf9d2f8bd719d171385dde594f74b4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/3744b87afb2193c88857aec75c88378c.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0888,
+ "steps": 332 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/52e0b6c21b84e63c174bec2662584b59.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/52e0b6c21b84e63c174bec2662584b59.json
new file mode 100644
index 0000000000000000000000000000000000000000..bd1857637f18c522c93b33462951b204dca3619f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/52e0b6c21b84e63c174bec2662584b59.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.2926,
+ "steps": 1145 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/5d05945c4e22b2861b15d558fb83c6e1.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/5d05945c4e22b2861b15d558fb83c6e1.json
new file mode 100644
index 0000000000000000000000000000000000000000..ba30e6254772d7d12b8dac51ce7c7241fad858b1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/5d05945c4e22b2861b15d558fb83c6e1.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.1586,
+ "steps": 596 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/86231af23e1064da708992cd22fcc6cd.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/86231af23e1064da708992cd22fcc6cd.json
new file mode 100644
index 0000000000000000000000000000000000000000..b614d74d7813fb556ab95e0d42d5381538c9b60a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/86231af23e1064da708992cd22fcc6cd.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0916,
+ "steps": 332 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/9c06dc676f02ccbf93885782c64aa8c0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/9c06dc676f02ccbf93885782c64aa8c0.json
new file mode 100644
index 0000000000000000000000000000000000000000..b3c09fcfc35fed533c6bbb0dccdf31873db923e9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/9c06dc676f02ccbf93885782c64aa8c0.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.1483,
+ "steps": 596 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/addd047e7326afb3baae18e98392f6ad.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/addd047e7326afb3baae18e98392f6ad.json
new file mode 100644
index 0000000000000000000000000000000000000000..fab86abb6f448b87b768b06097dcb942ab14f420
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/addd047e7326afb3baae18e98392f6ad.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.1022,
+ "steps": 332 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/af03277f3ce7d723e9695176099b9946.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/af03277f3ce7d723e9695176099b9946.json
new file mode 100644
index 0000000000000000000000000000000000000000..6c9b90bb8ecfc3f82771bf26bc7110423141ab6b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.0.session/cache/af03277f3ce7d723e9695176099b9946.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0908,
+ "steps": 332 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bc8717807fd0d5bfde96f27734717207d76c39db
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_const.res.oracle
@@ -0,0 +1,25 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/float_const.i (no preprocessing)
+[kernel:parser:decimal-float] tests/wp_acsl/float_const.i:10: Warning:
+ Floating-point constant 0.1f is not represented exactly. Will use 0x1.99999a0000000p-4.
+ (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
+[wp] 8 goals scheduled
+[wp] [Alt-Ergo] Goal typed_double_convertible_check : Valid
+[wp] [Alt-Ergo] Goal typed_double_convertible_check_2 : Valid
+[wp] [Alt-Ergo] Goal typed_double_convertible_check_3 : Valid
+[wp] [Alt-Ergo] Goal typed_double_convertible_check_4 : Valid
+[wp] [Alt-Ergo] Goal typed_float_convertible_check : Valid
+[wp] [Alt-Ergo] Goal typed_float_convertible_check_2 : Valid
+[wp] [Alt-Ergo] Goal typed_float_convertible_check_3 : Valid
+[wp] [Alt-Ergo] Goal typed_float_convertible_check_4 : Valid
+[wp] Proved goals: 8 / 8
+ Qed: 0
+ Alt-Ergo: 8
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ float_convertible - 4 4 100%
+ double_convertible - 4 4 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i
new file mode 100644
index 0000000000000000000000000000000000000000..b412a516663d5e3e228cfbeb7d43971796145812
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.i
@@ -0,0 +1,13 @@
+/* run.config
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.ml
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+/*@ ensures unimplemented_builtin ; */
+void foo(void);
+
+int main(void){
+ foo();
+ //@ assert \true ;
+}
\ No newline at end of file
diff --git a/src/plugins/wp/tests/wp_acsl/unsupported_builtin.ml b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ed343f06029c748895e17bcddb6652e4ddd3a8c6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/unsupported_builtin.ml
@@ -0,0 +1,12 @@
+open Cil_types
+
+let builtin = {
+ bl_name = "unimplemented_builtin" ;
+ bl_labels = [] ;
+ bl_params = [] ;
+ bl_type = None ;
+ bl_profile = [] ;
+}
+
+let () =
+ Logic_builtin.add builtin
\ No newline at end of file
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
index 1274212b3de4edfa6b92d981a76d07bae8da56e8..f573edafe8d54e38b786507fc9900efc9d02cf1f 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
@@ -11,6 +11,7 @@
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_preserved : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_deductible_established : not tried
+[wp] Goal typed_BinaryMultiplication_assert : not tried
[wp] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : not tried
[wp] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_2 : not tried
[wp] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_3 : not tried
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 1b12533c9f8de027acbe4871855f4d283b89627f..9cd3bd3d041d28f969185ef6d728ca3a37f273f3 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -3324,6 +3324,9 @@
[ Extern ] Post-condition 'positive_result'
ensures positive_result: \result ≥ -0.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'result_value'
+ ensures result_value: \result ≡ sqrt(\old(x))
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
@@ -3344,10 +3347,13 @@
[ Extern ] Post-condition 'positive_result'
ensures positive_result: \result ≥ -0.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'result_value'
+ ensures result_value: \result ≡ sqrtf(\old(x))
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 547)
+[ Extern ] Froms (file share/libc/math.h, line 548)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3367,7 +3373,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 555)
+[ Extern ] Froms (file share/libc/math.h, line 557)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3384,7 +3390,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 578)
+[ Extern ] Froms (file share/libc/math.h, line 580)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3401,7 +3407,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 584)
+[ Extern ] Froms (file share/libc/math.h, line 586)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3418,7 +3424,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 591)
+[ Extern ] Froms (file share/libc/math.h, line 593)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3435,7 +3441,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 597)
+[ Extern ] Froms (file share/libc/math.h, line 599)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3452,7 +3458,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 603)
+[ Extern ] Froms (file share/libc/math.h, line 605)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3469,7 +3475,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 609)
+[ Extern ] Froms (file share/libc/math.h, line 611)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3486,7 +3492,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 631)
+[ Extern ] Froms (file share/libc/math.h, line 633)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3503,7 +3509,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 637)
+[ Extern ] Froms (file share/libc/math.h, line 639)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3520,7 +3526,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 643)
+[ Extern ] Froms (file share/libc/math.h, line 645)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3537,7 +3543,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 657)
+[ Extern ] Froms (file share/libc/math.h, line 659)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3554,7 +3560,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 663)
+[ Extern ] Froms (file share/libc/math.h, line 665)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3571,7 +3577,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 669)
+[ Extern ] Froms (file share/libc/math.h, line 671)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3588,7 +3594,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 676)
+[ Extern ] Froms (file share/libc/math.h, line 678)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3605,7 +3611,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 683)
+[ Extern ] Froms (file share/libc/math.h, line 685)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3622,7 +3628,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 704)
+[ Extern ] Froms (file share/libc/math.h, line 706)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3639,7 +3645,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 711)
+[ Extern ] Froms (file share/libc/math.h, line 713)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3656,7 +3662,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 718)
+[ Extern ] Froms (file share/libc/math.h, line 720)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3673,7 +3679,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 766)
+[ Extern ] Froms (file share/libc/math.h, line 768)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3690,7 +3696,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 772)
+[ Extern ] Froms (file share/libc/math.h, line 774)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4054,7 +4060,7 @@
--------------------------------------------------------------------------------
179 Completely validated
16 Locally validated
- 484 Considered valid
+ 486 Considered valid
56 To be validated
- 735 Total
+ 737 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 26025f53b3f3c3eaabb341ba703905a224cf6157..705dcf5c78ca7dac8390b734fb4b5276c36e83bd 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3256,6 +3256,7 @@ extern float powf(float x, float y);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
+ ensures result_value: \result ≡ sqrt(\old(x));
assigns \result;
assigns \result \from x;
*/
@@ -3265,6 +3266,7 @@ extern double sqrt(double x);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
+ ensures result_value: \result ≡ sqrtf(\old(x));
assigns \result;
assigns \result \from x;
*/