Skip to content
Snippets Groups Projects
Commit 6961078a authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[ocaml] silence spurious warnings about partial applications

parent f3c4504d
No related branches found
No related tags found
No related merge requests found
......@@ -347,10 +347,11 @@ module ValueCoverageGUI = struct
~markup:(Format.sprintf "%s%% functions reached"
(Metrics_base.float_to_string pcent))
~justify:`LEFT ~packing:box#pack ());
let _ = Gtk_helper.on_bool box "Highlight results" (fun () -> !highlight)
(fun b -> highlight := b; main_ui#rehighlight ())
let _ignore = Gtk_helper.on_bool box "Highlight results"
(fun () -> !highlight)
(fun b -> highlight := b; main_ui#rehighlight ())
in
let _ = Gtk_helper.on_bool box "Show columns"
let _ignore = Gtk_helper.on_bool box "Show columns"
~tooltip:"Shows the columns related to dead code in the filetree."
(fun () -> !filetree_enabled)
(fun b -> filetree_enabled := b; !update_filetree `Visibility)
......
......@@ -71,7 +71,7 @@ let filter_accesses l =
let f = consider_access () in
List.filter (fun access -> f (Register.classify_accesses access)) l
let _ =
let _ignore =
Dynamic.register
~plugin:"Occurrence"
~journalize:false
......@@ -79,7 +79,7 @@ let _ =
(Datatype.func Datatype.bool Datatype.unit)
Enabled.set
let _ =
let _ignore =
Dynamic.register
~plugin:"Occurrence"
~journalize:false
......
......@@ -63,7 +63,7 @@ let journal_register ?comment is_dyn name ty_arg fctref fct =
let ty = Datatype.func ty_arg Datatype.unit in
Db.register (Db.Journalize("RteGen." ^ name, ty)) fctref fct;
if is_dyn then
let _ =
let _ignore =
Dynamic.register ?comment ~plugin:"RteGen" name ty ~journalize:true fct
in
()
......@@ -111,7 +111,7 @@ let _ =
(* retrieve list of generated rte annotations (not precond) for
a given stmt *)
let _ =
let _ignore =
Dynamic.register
~comment:"Get the list of annotations previously emitted by RTE for the \
given statement."
......@@ -123,7 +123,7 @@ let _ =
~journalize:true
Generator.get_registered_annotations
let _ =
let _ignore =
Dynamic.register
~comment:"Generate RTE annotations corresponding to the given stmt of \
the given function."
......@@ -134,7 +134,7 @@ let _ =
~journalize:false
Visit.get_annotations_stmt
let _ =
let _ignore =
Dynamic.register
~comment:"Generate RTE annotations corresponding to the given exp \
of the given stmt in the given function."
......
......@@ -84,7 +84,7 @@ let is_shift e =
let open Qed.Logic in
match F.repr e with
| Fun( f , [_;n] ) ->
let _ = select_op f in
let _ignore = select_op f in
let _ = select_int n in
true
| _ -> false
......
......@@ -732,7 +732,7 @@ let deprecated name =
"Dynamic '%s' now is deprecated. Use `Wp.VC` api instead." name
let register name ty code =
let _ =
let _ignore =
Dynamic.register ~plugin:"Wp" name ty
~journalize:false (*LC: Because of Property is not journalizable. *)
(fun x -> deprecated name ; code x)
......
......@@ -965,7 +965,7 @@ let get_logfile w prover result =
let model = get_model w in
DISK.cache_log ~pid:w.po_pid ~model ~prover ~result
let _ =
let _ignore =
Dynamic.register ~plugin:"Wp" "Wpo.file_for_log_proof" ~journalize:false
(Datatype.func2
WpoType.ty ProverType.ty
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment