diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4c70e7912aa6f3fc37ee63b1e160179b3874ed1b..64bd16cb8239e8272bed82fc0653977951537875 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3923,7 +3923,7 @@ struct
let anonCompFieldName = anonCompFieldName
let conditionalConversion = logicConditionalConversion
let find_macro _ = raise Not_found
- let find_var ?label ~var =
+ let find_var ?label var =
let find_from_curr_env test =
(* logic has always access to the ghost variables. *)
match Datatype.String.Hashtbl.find ghost_env var with
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 98cf45da1bd0c70c4b39f8ff3fc5e3d6fc8b56f0..7dedd4c4c7adbd6fca8949d7c940a91decff2608 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -27,7 +27,7 @@ open Cil_datatype
exception Error of Cil_types.location * string
exception Unbound of string
-let find_var kf kinstr ?label ~var =
+let find_var kf kinstr ?label var =
let vi =
try
let vi = Globals.Vars.find_from_astinfo var (VLocal kf) in
@@ -89,7 +89,7 @@ end) =
let find_macro _ = raise Not_found
- let find_var ?label ~var = find_var X.kf X.kinstr ?label ~var
+ let find_var ?label var = find_var X.kf X.kinstr ?label var
let find_enum_tag x =
try
diff --git a/src/kernel_services/analysis/wto_statement.ml b/src/kernel_services/analysis/wto_statement.ml
index bfa182f5e12a8603b8a2989ba244fd5a4bae7a21..b69dd555d6df1d8677820742661f3347b329d35e 100644
--- a/src/kernel_services/analysis/wto_statement.ml
+++ b/src/kernel_services/analysis/wto_statement.ml
@@ -39,7 +39,7 @@ let build_wto kf =
let init = Kernel_function.find_first_stmt kf
and succs = fun stmt -> List.rev stmt.succs
in
- Scheduler.partition ?pref:None ~init ~succs
+ Scheduler.partition ~pref:(fun _ _ -> 0) ~init ~succs
(* ********************************************************************** *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 250e409acf6a0d98e05f474c6cea24cec0d44f40..b317c5daf7a72cf8413c5e366010e7b51aacaaad 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -488,7 +488,7 @@ type typing_context = {
anonCompFieldName : string;
conditionalConversion : typ -> typ -> typ;
find_macro : string -> lexpr;
- find_var : ?label:string -> var:string -> logic_var;
+ find_var : ?label:string -> string -> logic_var;
find_enum_tag : string -> exp * typ;
find_comp_field: compinfo -> string -> offset;
find_type : type_namespace -> string -> typ;
@@ -670,7 +670,7 @@ module Make
val anonCompFieldName : string
val conditionalConversion : typ -> typ -> typ
val find_macro : string -> lexpr
- val find_var : ?label:string -> var:string -> logic_var
+ val find_var : ?label:string -> string -> logic_var
val find_enum_tag : string -> exp * typ
val find_comp_field: compinfo -> string -> offset
val find_type : type_namespace -> string -> typ
@@ -2615,7 +2615,7 @@ struct
with Not_found ->
try
let label = Lenv.string_of_current_label env in
- let info = ctxt.find_var ?label ~var:x in
+ let info = ctxt.find_var ?label x in
(match info.lv_origin with
| Some lv ->
check_current_label loc env;
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e1c613d9e297cac4e1fdc8a18ab8a31489934bf3..109b45d7f1b47375d2ed4b23d9c505c1cfb7d036 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -97,7 +97,7 @@ type typing_context = {
anonCompFieldName : string;
conditionalConversion : typ -> typ -> typ;
find_macro : string -> Logic_ptree.lexpr;
- find_var : ?label:string -> var:string -> logic_var;
+ find_var : ?label:string -> string -> logic_var;
(** the label argument is a C label (obeying the restrictions
of which label can be present in a \at). If present, the scope for
searching local C variables is the one of the statement with
@@ -262,7 +262,7 @@ module Make
val anonCompFieldName : string
val conditionalConversion : typ -> typ -> typ
val find_macro : string -> Logic_ptree.lexpr
- val find_var : ?label:string -> var:string -> logic_var
+ val find_var : ?label:string -> string -> logic_var
(** see corresponding field in {!Logic_typing.typing_context}. *)
val find_enum_tag : string -> exp * typ
val find_type : type_namespace -> string -> typ
diff --git a/src/libraries/utils/wto.ml b/src/libraries/utils/wto.ml
index ec3583f300351100430761003f5348622c2220e2..5c6ed3e9801f96d8fb047afd2ad8ca49cc1f8acd 100644
--- a/src/libraries/utils/wto.ml
+++ b/src/libraries/utils/wto.ml
@@ -187,10 +187,9 @@ module Make(N:sig
let element = Stack.pop state.stack in
DFN.remove state.dfn element;
if not (N.equal element vertex) then begin
- let best_head = match pref with
- (** the strict is important because we are conservative *)
- | Some cmp when cmp best_head element < 0 -> element
- | _ -> best_head
+ (** the strict is important because we are conservative *)
+ let best_head =
+ if pref best_head element < 0 then element else best_head
in
reset_SCC best_head
end
@@ -223,7 +222,7 @@ module Make(N:sig
type pref = N.t -> N.t -> int
- let partition ?pref ~init ~succs =
+ let partition ~pref ~init ~succs =
let state = {dfn = DFN.create 17; num = 0; succs;
stack = Stack.create () } in
let loop,component = visit ~pref state init [] in
diff --git a/src/libraries/utils/wto.mli b/src/libraries/utils/wto.mli
index 004312ad709592fbdc8c8e98b139f2a098da10f1..6a12f1a3f847e361a9692454ed3b326f1eea29d3 100644
--- a/src/libraries/utils/wto.mli
+++ b/src/libraries/utils/wto.mli
@@ -53,11 +53,14 @@ module Make(Node:sig
end):sig
type pref = Node.t -> Node.t -> int
- (** partial order of preference for the choice of the head of a loop *)
+ (** Partial order of preference for the choice of the head of a loop.
+ [pref current_head new_candidate] must return < 0 if [new_candidate]
+ is preferred to [current_head].
+ Use "(fun _ _ -> 0)" for no specific preference. *)
(** Implements Bourdoncle "Efficient chaotic iteration strategies with
widenings" algorithm to compute a WTO. *)
- val partition: ?pref:pref -> init:Node.t -> succs:(Node.t -> Node.t list) -> Node.t partition
+ val partition: pref:pref -> init:Node.t -> succs:(Node.t -> Node.t list) -> Node.t partition
val pretty_partition: Format.formatter -> Node.t partition -> unit
val pretty_component: Format.formatter -> Node.t component -> unit
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index b1423f97bef4baa66534e326e85340364dd9ef14..abc05400af319157f5bf72762e44972d831f463b 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -697,7 +697,7 @@ struct
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () = false
let find_macro _ = raise Not_found
- let find_var ?label:_ ~var:_ = raise Not_found
+ let find_var ?label:_ _ = raise Not_found
let find_enum_tag _ = raise Not_found
(*let find_comp_type ~kind:_ _ = raise Not_found*)
let find_comp_field info s =
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index c5a986d5802ee1663188d80d51817a05a251fdc8..21ade2a5af1b660f194cea1f3c85eb7717069438 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1034,7 +1034,7 @@ class main_window () : main_window_extension_points =
let m =
new Menu_manager.menu_manager
~packing:(toplevel_vbox#pack ~expand:false ~fill:false ~from:`START)
- ~host:(self :> Gtk_helper.host)
+ (self :> Gtk_helper.host)
in
menu_manager <- Some m;
m
diff --git a/src/plugins/gui/menu_manager.ml b/src/plugins/gui/menu_manager.ml
index 5d835aabd1c60aef79cff1ad0118f5bf3cae62e9..af195e70150242030b612ab071b8f9d148251690 100644
--- a/src/plugins/gui/menu_manager.ml
+++ b/src/plugins/gui/menu_manager.ml
@@ -112,7 +112,7 @@ let add_submenu container ~pos label =
external set_menu : Obj.t -> unit = "ige_mac_menu_set_menu_bar"
*)
-class menu_manager ?packing ~host:(_:Gtk_helper.host) =
+class menu_manager ?packing (_:Gtk_helper.host) =
let menubar = GMenu.menu_bar ?packing () in
(* let () = set_menu (Obj.field (Obj.repr ((menubar)#as_widget)) 1) in *)
let factory = new GMenu.factory menubar in
diff --git a/src/plugins/gui/menu_manager.mli b/src/plugins/gui/menu_manager.mli
index dba70f9279ccb6d55cb566d59e26cdfce42eee12..22f5cba0dc5ead35416e58d45365f8cdd02f23dc 100644
--- a/src/plugins/gui/menu_manager.mli
+++ b/src/plugins/gui/menu_manager.mli
@@ -113,7 +113,7 @@ end
(** How to handle a Frama-C menu.
@since Boron-20100401 *)
-class menu_manager: ?packing:(GObj.widget -> unit) -> host:Gtk_helper.host ->
+class menu_manager: ?packing:(GObj.widget -> unit) -> Gtk_helper.host ->
object
(** {2 API for plug-ins} *)
diff --git a/src/plugins/wp/Auto.mli b/src/plugins/wp/Auto.mli
index 6b5234198a8d8392f8666e32b77c33cfaf0047fa..669b50df4c8a7b94c115fc5cb6c7eb4cbad5d972 100644
--- a/src/plugins/wp/Auto.mli
+++ b/src/plugins/wp/Auto.mli
@@ -35,7 +35,7 @@ val contrapose : ?priority:float -> selection -> strategy
val compound : ?priority:float -> selection -> strategy
val cut : ?priority:float -> ?modus:bool -> selection -> strategy
val filter : ?priority:float -> ?anti:bool -> unit -> strategy
-val havoc : ?priority:float -> havoc:selection -> strategy
+val havoc : ?priority:float -> selection -> strategy
val separated : ?priority:float -> selection -> strategy
val instance : ?priority:float -> selection -> selection list -> strategy
val lemma : ?priority:float -> ?at:selection -> string -> selection list -> strategy
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 54e5d9d0cbf24f3a2768a07a0f1a8a0dccca85a8..ed48014f5628c551088149998f0db4c2bee9e168 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1088,7 +1088,7 @@ let prove_goal ~id ~title ~name ?axioms t =
end;
th, decl
-let prove_prop ?axioms ~pid ~prop =
+let prove_prop ?axioms ~pid prop =
let id = WpPropId.get_propid pid in
let title = Pretty_utils.to_string WpPropId.pretty pid in
let name = "WP" in
@@ -1105,13 +1105,13 @@ let task_of_wpo wpo =
let axioms = v.Wpo.VC_Annot.axioms in
let prop = Wpo.GOAL.compute_proof v.Wpo.VC_Annot.goal in
(* Format.printf "Goal: %a@." Lang.F.pp_pred prop; *)
- prove_prop ~pid ~prop ?axioms
+ prove_prop ~pid prop ?axioms
| Wpo.GoalLemma v ->
let lemma = v.Wpo.VC_Lemma.lemma in
let depends = v.Wpo.VC_Lemma.depends in
let prop = Lang.F.p_forall lemma.l_forall lemma.l_lemma in
let axioms = Some(lemma.l_cluster,depends) in
- prove_prop ~pid ~prop ?axioms
+ prove_prop ~pid prop ?axioms
(* -------------------------------------------------------------------------- *)
(* --- Prover Task --- *)
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index f5236949e0ae9c9826c14289b87253d90caf0a88..5466a629e8d5f07e5029164aa35342820fc18558 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -597,7 +597,7 @@ struct
let next = (a.return_point,Vertex.Set.empty) in
let wto =
WTO.partition
- ?pref:None (* natural loop keep the heads *)
+ ~pref:(fun _ _ -> 0) (* natural loops keep their heads *)
~succs:(UnrollUnnatural.G.succ g)
~init:here in
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index f363cf4ecc86d90c71fd51c3eb131165fef1c002..294c706e6b6342ef1337ccebff69b54da3620fc3 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -196,7 +196,7 @@ class validity =
module Havoc =
struct
let tactical = Tactical.export (new havoc)
- let strategy ?(priority=1.0) ~havoc =
+ let strategy ?(priority=1.0) havoc =
Strategy.{
priority ;
tactical ;
diff --git a/src/plugins/wp/TacHavoc.mli b/src/plugins/wp/TacHavoc.mli
index 0942b43ac08e40faf0cfa83bc9f542affb988a3c..de44ed3601eaeba6c3757cf35397db333d725339 100644
--- a/src/plugins/wp/TacHavoc.mli
+++ b/src/plugins/wp/TacHavoc.mli
@@ -29,7 +29,7 @@ module Havoc :
sig
val tactical : tactical
val strategy :
- ?priority:float -> havoc:selection -> strategy
+ ?priority:float -> selection -> strategy
end
module Separated :