Commit 6049c2ea authored by MARCHE Claude's avatar MARCHE Claude

Extraction: replace debug message with appropriate warning

parent 317d51b8
......@@ -40,7 +40,7 @@ OCAMLC=ocamlopt.opt
INCLUDES=-I $(BD) $(INCLUDE)
LIBS=unix.cmxa $(BIGINTLIB).cmxa why3extract.cmxa
LIBSOLD=$(BD)/why3__BuiltIn.cmx $(BD)/int__Int.cmx $(BD)/array__Array.cmx
WHY3FLAGS=-L . --debug ignore_unused_vars --debug extraction
WHY3FLAGS=-L . --debug ignore_unused_vars
MLFLAGS=
MLIFLAGS=
MLEXECFLAGS=
......@@ -70,7 +70,7 @@ endif
replay:
for i in $(MLWUTIL) $(MLWIMPL); do \
why3 replay -L . $$i ; \
why3 replay -q -L . $$i ; \
done
depend: .depend
......
......@@ -671,19 +671,20 @@ module Translate = struct
else
[ML.Dexn (id, Some (ity info xs.xs_ity))]
let warn_non_ghost_non_exec ps =
if not ps.ps_ghost then
Warning.emit ?loc:ps.ps_name.id_loc
"Cannot extract code from non-ghost function %s: body is not executable"
ps.ps_name.id_string
let pdecl info d =
if Mlw_exec.is_exec_pdecl info.exec d then pdecl info d else
begin
begin match d.pd_node with
| PDlet { let_sym = lv } ->
Debug.dprintf debug "ignoring non-executable declaration %s@."
(lv_name lv).id_string;
| PDlet { let_sym = LetA ps } -> warn_non_ghost_non_exec ps
| PDrec fdl ->
List.iter
(fun {fun_ps=ps} ->
Debug.dprintf debug
"ignoring non-executable declaration %s (ghost = %b)@."
ps.ps_name.id_string ps.ps_ghost) fdl
(fun {fun_ps=ps} -> warn_non_ghost_non_exec ps) fdl
| _ -> ()
end;
[]
......
......@@ -2,16 +2,8 @@
module M
type t = O | S t
use import map.Map
let f () =
let ghost g (x:t) : t =
match x with O -> O | S y -> y end
(*
with ghost h (x:t) : t =
match x with O -> O | S y -> y end
*)
in
()
let f (x:map int int) : int = x[0]
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment