diff --git a/src/axioms.ml b/src/axioms.ml
index 9ffe019c78ac37418294a90ef3b75063a0404dec..2e6fa0f329e8d5392d1fd25e544bf29d8ed6fbc0 100644
--- a/src/axioms.ml
+++ b/src/axioms.ml
@@ -36,6 +36,7 @@ type param =
| Param of Expr.rsymbol
| Value of Expr.rsymbol
| Axiom of Decl.prsymbol
+ | Unsafe of Ident.ident
let ident = function
| Type ty -> ty.ts_name
@@ -43,6 +44,7 @@ let ident = function
| Param rs -> rs.rs_name
| Value rs -> rs.rs_name
| Axiom pr -> pr.pr_name
+ | Unsafe id -> id
type parameter = {
param : param ;
@@ -51,9 +53,14 @@ type parameter = {
}
let is_external { builtin ; extern } = builtin <> [] || extern <> None
+
+let is_unsafe = function
+ | { param = (Unsafe _) } -> true
+ | { param = (Value _ | Axiom _ | Type _ | Param _ | Logic _) } -> false
+
let is_hypothesis = function
- | { param = (Value _ | Axiom _) } -> true
- | _ -> false
+ | { param = (Value _ | Axiom _ | Unsafe _) } -> true
+ | { param = (Type _ | Param _ | Logic _) } -> false
type signature = {
locals : parameter Mid.t ;
@@ -166,7 +173,7 @@ let rec cany (ce : Expr.cexp) =
| _ -> false
(* Detect (fun result -> result = a) s.t. check a *)
-let constrained_post check (p : Ity.post) =
+let constrained_post unless (p : Ity.post) =
match p.t_node with
| Teps rp ->
let r,post = Term.t_open_bound rp in
@@ -176,7 +183,7 @@ let constrained_post check (p : Ity.post) =
| Tapp(f,[a;b]) ->
not Term.(ls_equal f ps_equ) ||
not @@ is_var r a ||
- not @@ check b
+ not @@ unless b
| _ -> true
end
| _ -> true
@@ -188,18 +195,56 @@ let constrained (rs : Expr.rsymbol) =
| RLlemma -> true
| RLnone -> rs.rs_cty.cty_post <> []
| RLpv pv ->
- let check = is_var pv.pv_vs in
- List.exists (constrained_post check) rs.rs_cty.cty_post
+ let unless = is_var pv.pv_vs in
+ List.exists (constrained_post unless) rs.rs_cty.cty_post
| RLls ls ->
rs.rs_cty.cty_post <> [] &&
let xs = List.map (fun pv -> pv.Ity.pv_vs) rs.rs_cty.cty_args in
- let check (a : Term.term) =
+ let unless (a : Term.term) =
match a.t_node with
| Tapp(f,es) ->
(try Term.ls_equal f ls && List.for_all2 is_var xs es
with Invalid_argument _ -> false)
| _ -> false
- in List.exists (constrained_post check) rs.rs_cty.cty_post
+ in List.exists (constrained_post unless) rs.rs_cty.cty_post
+
+(* -------------------------------------------------------------------------- *)
+(* --- Sound Expression Detection --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec safe_let_defn (def : Expr.let_defn) =
+ match def with
+ | LDvar(_,e) -> safe_expr e
+ | LDsym(_,ce) -> safe_cexpr ce
+ | LDrec lts -> List.for_all safe_rec_defn lts
+
+and safe_rec_defn (d : Expr.rec_defn) = safe_cexpr d.rec_fun
+
+and safe_expr (e : Expr.expr) =
+ match e.e_node with
+ | Evar _ | Econst _ | Eassign _ | Epure _ | Eabsurd -> true
+ | Eexec (ce, _) -> safe_cexpr ce
+ | Elet(def,e) -> safe_let_defn def && safe_expr e
+ | Eif (a, b, c) -> safe_expr a && safe_expr b && safe_expr c
+ | Ewhile(a,_,_,b) -> safe_expr a && safe_expr b
+ | Efor (_, _, _, _, b) -> safe_expr b
+ | Eraise (_, e) | Eexn (_, e) | Eghost e -> safe_expr e
+ | Eassert ((Assert | Check), _) -> true
+ | Eassert (Assume,_) -> false
+ | Ematch (a, ps, xs) ->
+ safe_expr a &&
+ List.for_all safe_branch ps &&
+ Ity.Mxs.for_all safe_handler xs
+
+and safe_branch (_,e) = safe_expr e
+and safe_handler _ (_,e) = safe_expr e
+and safe_cexpr (ce : Expr.cexp) =
+ match ce.c_node with
+ | Cfun e -> safe_expr e
+ | Capp _ | Cpur _ -> true
+ | Cany ->
+ (* don't understand why, but that why3 does *)
+ ce.c_cty.cty_args = []
(* -------------------------------------------------------------------------- *)
(* --- Module Declarations --- *)
@@ -213,21 +258,32 @@ let add_mtype henv (hs : signature) (it : Pdecl.its_defn) : signature =
let add_rsymbol henv hs (rs : Expr.rsymbol) (cexp : Expr.cexp) =
if Id.lemma rs.rs_name then hs else
- match rs.rs_logic with
- | RLlemma -> hs
- | RLnone | RLpv _ | RLls _ ->
- if cany cexp then
- if constrained rs then
- add henv hs (Value rs)
- else
- add henv hs (Param rs)
- else hs
+ match cexp.c_node with
+ | Cfun e when not (safe_expr e) -> add henv hs (Unsafe rs.rs_name)
+ | _ ->
+ match rs.rs_logic with
+ | RLlemma -> hs
+ | RLnone | RLpv _ | RLls _ ->
+ if cany cexp then
+ if constrained rs then
+ add henv hs (Value rs)
+ else
+ add henv hs (Param rs)
+ else hs
+
+let add_psymbol henv hs (pv : Ity.pvsymbol) (exp : Expr.expr) =
+ if safe_expr exp then hs else add henv hs (Unsafe pv.pv_vs.vs_name)
+
+let add_rec_def henv hs (def : Expr.rec_defn) =
+ if safe_rec_defn def then hs else add henv hs (Unsafe def.rec_sym.rs_name)
let add_pdecl henv (hs : signature) (d : Pdecl.pdecl) : signature =
match d.pd_node with
+ | PDexn _ -> hs
| PDtype tys -> List.fold_left (add_mtype henv) hs tys
| PDlet (LDsym(r,c)) -> add_rsymbol henv hs r c
- | PDlet (LDvar _ | LDrec _) | PDexn _ -> hs
+ | PDlet (LDvar(v,e)) -> add_psymbol henv hs v e
+ | PDlet (LDrec defs) -> List.fold_left (add_rec_def henv) hs defs
| PDpure -> List.fold_left (add_decl henv) hs d.pd_pure
let rec add_munit henv (hs : signature) (m : Pmodule.mod_unit) : signature =
diff --git a/src/axioms.mli b/src/axioms.mli
index 696f30a6eb23ecffd9590c5ff0aa6fb2d56507ae..627f56a7a2f3592237408b61d15d7f4a2793c2e3 100644
--- a/src/axioms.mli
+++ b/src/axioms.mli
@@ -35,6 +35,7 @@ type param =
| Param of Expr.rsymbol
| Value of Expr.rsymbol
| Axiom of Decl.prsymbol
+ | Unsafe of Ident.ident
type parameter = {
param : param ;
@@ -45,6 +46,7 @@ type parameter = {
val ident : param -> Ident.ident
val is_external : parameter -> bool
val is_hypothesis : parameter -> bool
+val is_unsafe : parameter -> bool
val parameter : signature -> Ident.ident -> parameter option
val parameters : signature -> parameter list
val dependencies : henv -> ?self:bool -> Theory.theory list -> Theory.theory list
diff --git a/src/docgen.ml b/src/docgen.ml
index 1ea8f33ee40563c8b6a4be9bd78649c290669f56..755f3a1c169ed5934a95ce48c7d45549826eae30 100644
--- a/src/docgen.ml
+++ b/src/docgen.ml
@@ -215,6 +215,7 @@ let icon_failed = "icon failed icofont-warning"
let icon_parameter = "icon small remark icofont-star"
let icon_sound_param = "icon small valid icofont-star"
let icon_unsound_param = "icon small warning icofont-star"
+let icon_unsafe_param = "icon small failed icofont-star"
let pp_mark ?href ~title ~cla fmt =
match href with
@@ -309,13 +310,17 @@ let process_axioms env (id : Id.id) =
match builtin, extern with
| [],None ->
let icon_sound () =
- if Soundness.is_sound @@ Soundness.compute env.senv theory
- then icon_sound_param else icon_unsound_param in
+ match Soundness.compute env.senv theory with
+ | Unsound -> icon_unsafe_param
+ | Sound _ -> icon_sound_param
+ | Unknown _ -> icon_unsound_param
+ in
let cla,title =
match param with
| Type _ | Logic _ | Param _ -> icon_parameter, "Parameter"
| Value _ -> icon_sound (), "Value Parameter"
| Axiom _ -> icon_sound (), "Hypothesis"
+ | Unsafe _ -> icon_unsafe_param, "Unsound Definition"
in
Pdoc.ppt env.out (pp_mark ~cla ~title)
| [], Some ext ->
@@ -329,22 +334,35 @@ let process_axioms env (id : Id.id) =
"Built-in symbol (%s), extracted to OCaml (%s)" (provers ops) ext
in Pdoc.ppt env.out (pp_mark ~cla:icon_unsound_param ~title)
-let process_hypothesis env Axioms.{ param } =
+let process_hypothesis env (s : Soundness.soundness) (p : Axioms.parameter) =
try
- let id = Id.resolve ~lib:env.src.lib @@ Axioms.ident param in
- let key = match param with
+ let id = Id.resolve ~lib:env.src.lib @@ Axioms.ident p.param in
+ let key = match p.param with
| Type _ -> "type"
| Logic _ -> "logic"
| Param _ -> "param"
| Value _ -> "value"
| Axiom _ -> "axiom"
+ | Unsafe _ -> "unsound"
+ in
+ let qualif fmt =
+ if Axioms.is_unsafe p then
+ pp_mark ~cla:icon_unsafe_param ~title:"unsafe definition" fmt
+ else
+ if Axioms.is_external p then
+ pp_mark ~cla:icon_unsound_param ~title:"external" fmt
+ else if Axioms.is_hypothesis p then
+ if Soundness.is_sound s then
+ pp_mark ~cla:icon_sound_param ~title:"witnessed hypothesis" fmt
+ else
+ pp_mark ~cla:icon_unsound_param ~title:"uncloned hypothesis" fmt
in
Pdoc.printf env.crc
- "@\n %a <a id=\"%a\" href=\"%a\">%a</a>"
+ "@\n %a <a id=\"%a\" href=\"%a\">%a</a>%t"
Pdoc.pp_keyword key
Id.pp_proof_aname id
(Id.pp_ahref ~scope:None) id
- Id.pp_local id
+ Id.pp_local id qualif
with Not_found -> ()
let process_instance env ~ok (s : Docref.instance) =
@@ -360,16 +378,18 @@ let process_module_axioms env =
| None -> ()
| Some thy ->
let pre = lazy (Pdoc.printf env.crc "<pre class=\"src\">") in
+ let sound = Soundness.compute env.senv thy in
Axioms.iter env.henv ~self:true
(fun (p : Axioms.parameter) ->
- if Axioms.is_hypothesis p && not (Axioms.is_external p) then
+ if Axioms.is_hypothesis p &&
+ not @@ Id.standard @@ Axioms.ident p.param then
begin
Lazy.force pre ;
- process_hypothesis env p ;
+ process_hypothesis env sound p ;
end
) [thy.theory] ;
- begin match Soundness.compute env.senv thy with
- | Sound [] | Unknown [] -> ()
+ begin match sound with
+ | Unsound | Sound [] | Unknown [] -> ()
| Sound ns ->
Lazy.force pre ; List.iter (process_instance env ~ok:true) ns
| Unknown ns ->
@@ -382,11 +402,12 @@ type axioms = {
prm : int ;
hyp : int ;
pvs : int ;
+ unsafe : int ;
sound : Soundness.soundness ;
}
let free = {
- ext = 0 ; prm = 0 ; hyp = 0 ; pvs = 0 ;
+ ext = 0 ; prm = 0 ; hyp = 0 ; pvs = 0 ; unsafe = 0 ;
sound = Soundness.unknown ;
}
@@ -399,16 +420,18 @@ let add_axiom hs (p : Axioms.parameter) =
match p.param with
| Axiom _ -> { hs with hyp = succ hs.hyp }
| Value _ -> { hs with pvs = succ hs.pvs }
+ | Unsafe _ -> { hs with unsafe = succ hs.unsafe }
| Type _ | Logic _ | Param _ -> { hs with prm = succ hs.prm }
-let pp_axioms_link ?href fmt { ext ; prm ; hyp ; pvs ; sound } =
- if ext+prm+hyp+pvs > 0 then
+let pp_axioms_link ?href fmt { ext ; prm ; hyp ; pvs ; unsafe ; sound } =
+ if ext+prm+hyp+pvs+unsafe > 0 then
let cla =
if Soundness.is_clone sound then icon_parameter else
- if hyp + pvs > 0 then
- if Soundness.is_sound sound
- then icon_sound_param
- else icon_unsound_param
+ if hyp + pvs + unsafe > 0 then
+ match sound with
+ | Unsound -> icon_unsafe_param
+ | Sound _ -> icon_sound_param
+ | Unknown _ -> icon_unsound_param
else if prm > 0 then icon_parameter else icon_unsound_param
in
let title =
@@ -420,6 +443,9 @@ let pp_axioms_link ?href fmt { ext ; prm ; hyp ; pvs ; sound } =
plural hyp "1 hypothesis" @@ Printf.sprintf "%d hypotheses" ;
plural ext "1 external symbol" @@ Printf.sprintf "%d external symbols" ;
match sound with
+ | Soundness.Unsound ->
+ plural unsafe "1 unsound definition" @@
+ Printf.sprintf "%d unsafe definitions"
| Soundness.Unknown [] -> ["0 instance found"]
| Soundness.Unknown ns ->
plural (List.length ns) "1 uncomplete instance" @@
diff --git a/src/id.ml b/src/id.ml
index 9fe159e1ddad2b485dd0fe93be34493ec39655be..16bdb6871c262588a83b21f6eafba6109ad9f74d 100644
--- a/src/id.ml
+++ b/src/id.ml
@@ -80,6 +80,12 @@ let resolve ~lib id =
with _ -> `Stdlib
in { self = id ; id_pkg ; id_lib = lp ; id_mod ; id_qid }
+let standard id =
+ let lp,_,_ = path id in
+ lp <> [] &&
+ not @@ Filename.is_relative (file id) &&
+ try let _ = Meta.find (List.hd lp) in false with _ -> true
+
(* List Printing *)
let pp_prefix fmt q =
diff --git a/src/id.mli b/src/id.mli
index f6a16e6ada8c32c55ef57757bb850be3b66d2e8a..96600ed47b24b0b94abec97e785b210a4c2f4c54 100644
--- a/src/id.mli
+++ b/src/id.mli
@@ -45,6 +45,7 @@ type id = {
}
val lemma : t -> bool
+val standard : t -> bool
val resolve : lib:string list -> t -> id
val of_infix : string -> string
diff --git a/src/prove.ml b/src/prove.ml
index 0996852bdc1061a0f9b1f1b86bcc728adfd42d5d..f9a6e11cd3cf5b82e709ba709dc84d5447882e97 100644
--- a/src/prove.ml
+++ b/src/prove.ml
@@ -179,6 +179,7 @@ let report_parameter ~lib ~signature (prm : Axioms.parameter) =
| Param _ -> "param", parameters
| Value _ -> "value", procedures
| Axiom _ -> "axiom", hypotheses
+ | Unsafe _ -> "unsafe", procedures
in
let action, count =
if builtin || extern then externalized else
diff --git a/src/soundness.ml b/src/soundness.ml
index 67267f361e66ffc9b100a87155b9a62863aceaa4..dba94219d252e709ec2cc7125492db603f7668cb 100644
--- a/src/soundness.ml
+++ b/src/soundness.ml
@@ -33,6 +33,7 @@ module Sinst = Set.Make
end)
type soundness =
+ | Unsound
| Sound of Docref.instance list
| Unknown of Docref.instance list
@@ -70,23 +71,26 @@ let clone = Sound []
let unknown = Unknown []
let is_clone = function Sound [] -> true | _ -> false
-let is_sound = function Sound _ -> true | Unknown _ -> false
+let is_sound = function Sound _ -> true | Unsound | Unknown _ -> false
+let is_unsound = function Unsound -> true | Sound _ | Unknown _ -> false
let rec compute (env : env) (th : Docref.theory) : soundness =
let key = th.theory.th_name in
try Hid.find env.soundness key with Not_found ->
Hid.add env.soundness key (Unknown []) ;
let s =
- let ok = List.for_all
- (fun p -> not (Axioms.is_hypothesis p) || Axioms.is_external p)
- (Axioms.parameters th.signature)
- in
- if ok then Sound [] else
- try
- let instances = Sinst.elements !(Hid.find env.instances key) in
- let grounds = List.filter (ground_instance env) instances in
- if grounds <> [] then Sound grounds else Unknown instances
- with Not_found -> Unknown []
+ let ps = Axioms.parameters th.signature in
+ if List.exists (fun p -> Axioms.is_unsafe p) ps then Unsound else
+ let ok = List.for_all
+ (fun p -> not (Axioms.is_hypothesis p) || Axioms.is_external p)
+ ps
+ in
+ if ok then Sound [] else
+ try
+ let instances = Sinst.elements !(Hid.find env.instances key) in
+ let grounds = List.filter (ground_instance env) instances in
+ if grounds <> [] then Sound grounds else Unknown instances
+ with Not_found -> Unknown []
in Hid.replace env.soundness key s ; s
and ground_instance env inst =
diff --git a/src/soundness.mli b/src/soundness.mli
index 2d7e9f6f1ca34ac155f3d82a75bac76c67655f9e..b2a5a2f46a47688c7475bb02803dc4cc72f66282 100644
--- a/src/soundness.mli
+++ b/src/soundness.mli
@@ -27,6 +27,7 @@ val init : unit -> env
val register : env -> Docref.source -> unit
type soundness =
+ | Unsound
| Sound of Docref.instance list
| Unknown of Docref.instance list
@@ -35,6 +36,7 @@ val unknown : soundness
val is_clone : soundness -> bool
val is_sound : soundness -> bool
+val is_unsound : soundness -> bool
val compute : env -> Docref.theory -> soundness
(* -------------------------------------------------------------------------- *)
diff --git a/tests/clones.t/run.t b/tests/clones.t/run.t
index ae70ae5c86d91f0478dcedf2f64a391162bda0d8..893c915a01a0c4396f8dd53067cbf505a2b928b2 100644
--- a/tests/clones.t/run.t
+++ b/tests/clones.t/run.t
@@ -235,11 +235,11 @@
<pre class="src"><span class="keyword">module</span> <a id="Monoid" href="clones.Monoid.html">clones.Monoid</a><span title="2 parameters" class="icon small remark icofont-star"></span><span title="Valid (no goals)" class="icon remark icofont-check"></span></pre>
<pre class="src"><span class="keyword">module</span> <a id="Neutral" href="clones.Neutral.html">clones.Neutral</a><span title="3 parameters, 1 hypothesis, 0 instance found" class="icon small warning icofont-star"></span><span title="Valid (no goals)" class="icon remark icofont-check"></span></pre>
<pre class="src">
- <span class="keyword">axiom</span> <a id="Neutral.neutral" href="clones.Neutral.html#neutral">neutral</a>
+ <span class="keyword">axiom</span> <a id="Neutral.neutral" href="clones.Neutral.html#neutral">neutral</a><span title="uncloned hypothesis" class="icon small warning icofont-star"></span>
</pre>
<pre class="src"><span class="keyword">module</span> <a id="Commutative" href="clones.Commutative.html">clones.Commutative</a><span title="2 parameters, 1 hypothesis, 4 ground instances" class="icon small valid icofont-star"></span><span title="Valid (no goals)" class="icon remark icofont-check"></span></pre>
<pre class="src">
- <span class="keyword">axiom</span> <a id="Commutative.commutative" href="clones.Commutative.html#commutative">commutative</a>
+ <span class="keyword">axiom</span> <a id="Commutative.commutative" href="clones.Commutative.html#commutative">commutative</a><span title="witnessed hypothesis" class="icon small valid icofont-star"></span>
<span class="keyword">clone</span> <a href="clones.AC.html#clone-3">clones.AC</a><span title="sound instance" class="icon small valid icofont-star"></span>
<span class="keyword">clone</span> <a href="clones.IntAC.html#clone-3">clones.IntAC</a><span title="sound instance" class="icon small valid icofont-star"></span>
<span class="keyword">clone</span> <a href="clones.IntC.html#clone-2">clones.IntC</a><span title="sound instance" class="icon small valid icofont-star"></span>
@@ -247,15 +247,15 @@
</pre>
<pre class="src"><span class="keyword">module</span> <a id="Associative" href="clones.Associative.html">clones.Associative</a><span title="2 parameters, 1 hypothesis, 3 ground instances" class="icon small valid icofont-star"></span><span title="Valid (no goals)" class="icon remark icofont-check"></span></pre>
<pre class="src">
- <span class="keyword">axiom</span> <a id="Associative.associative" href="clones.Associative.html#associative">associative</a>
+ <span class="keyword">axiom</span> <a id="Associative.associative" href="clones.Associative.html#associative">associative</a><span title="witnessed hypothesis" class="icon small valid icofont-star"></span>
<span class="keyword">clone</span> <a href="clones.AC.html#clone-5">clones.AC</a><span title="sound instance" class="icon small valid icofont-star"></span>
<span class="keyword">clone</span> <a href="clones.IntA.html#clone-2">clones.IntA</a><span title="sound instance" class="icon small valid icofont-star"></span>
<span class="keyword">clone</span> <a href="clones.IntAC.html#clone-5">clones.IntAC</a><span title="sound instance" class="icon small valid icofont-star"></span>
</pre>
<pre class="src"><span class="keyword">module</span> <a id="AC" href="clones.AC.html">clones.AC</a><span title="2 parameters, 2 hypotheses, 1 ground instance" class="icon small valid icofont-star"></span><span title="Valid (no goals)" class="icon remark icofont-check"></span></pre>
<pre class="src">
- <span class="keyword">axiom</span> <a id="AC.commutative" href="clones.AC.html#commutative">commutative</a>
- <span class="keyword">axiom</span> <a id="AC.associative" href="clones.AC.html#associative">associative</a>
+ <span class="keyword">axiom</span> <a id="AC.commutative" href="clones.AC.html#commutative">commutative</a><span title="witnessed hypothesis" class="icon small valid icofont-star"></span>
+ <span class="keyword">axiom</span> <a id="AC.associative" href="clones.AC.html#associative">associative</a><span title="witnessed hypothesis" class="icon small valid icofont-star"></span>
<span class="keyword">clone</span> <a href="clones.IntAC.html#clone-6">clones.IntAC</a><span title="sound instance" class="icon small valid icofont-star"></span>
</pre>
<pre class="src"><span class="keyword">module</span> <a id="IntC" href="clones.IntC.html">clones.IntC</a><span title="Failed (no proof)" class="icon failed icofont-warning"></span></pre>
diff --git a/tests/drivers.t/run.t b/tests/drivers.t/run.t
index 0aef9711d64142040ded19ed700e152b58044293..a9d344fc9ccb3f872717167a4cf1f9c422477d15 100644
--- a/tests/drivers.t/run.t
+++ b/tests/drivers.t/run.t
@@ -37,7 +37,7 @@
<h1>Proofs</h1>
<pre class="src"><span class="keyword">module</span> <a id="A" href="drivers.A.html">drivers.A</a><span title="3 parameters, 1 hypothesis, 0 instance found" class="icon small warning icofont-star"></span><span title="Valid (no goals)" class="icon remark icofont-check"></span></pre>
<pre class="src">
- <span class="keyword">axiom</span> <a id="A.increasing" href="drivers.A.html#increasing">increasing</a>
+ <span class="keyword">axiom</span> <a id="A.increasing" href="drivers.A.html#increasing">increasing</a><span title="uncloned hypothesis" class="icon small warning icofont-star"></span>
</pre>
<script type="text/javascript" src="script.js"></script>
</body>
diff --git a/tests/proof.t/run.t b/tests/proof.t/run.t
index 447f03a9684f88b70c28941b836f8f4388f12fd6..4aed0e012a90fa485c59a5bc481607a5deb9bb15 100644
--- a/tests/proof.t/run.t
+++ b/tests/proof.t/run.t
@@ -119,15 +119,15 @@
<h1>Proofs</h1>
<pre class="src"><span class="keyword">module</span> <a id="A" href="clones.A.html">clones.A</a><span title="3 parameters, 2 hypotheses, 1 uncomplete instance" class="icon small warning icofont-star"></span><span title="Valid (one goal)" class="icon valid icofont-check"></span></pre>
<pre class="src">
- <span class="keyword">axiom</span> <a id="A.neutral" href="clones.A.html#neutral">neutral</a>
- <span class="keyword">axiom</span> <a id="A.commutative" href="clones.A.html#commutative">commutative</a>
+ <span class="keyword">axiom</span> <a id="A.neutral" href="clones.A.html#neutral">neutral</a><span title="uncloned hypothesis" class="icon small warning icofont-star"></span>
+ <span class="keyword">axiom</span> <a id="A.commutative" href="clones.A.html#commutative">commutative</a><span title="uncloned hypothesis" class="icon small warning icofont-star"></span>
<span class="keyword">clone</span> <a href="clones.B.html#clone-1">clones.B</a><span title="uncomplete instance" class="icon small warning icofont-star"></span>
</pre>
<pre class="src">
<span class="keyword">goal</span> <a id="A.neutral_com" href="clones.A.html#neutral_com">neutral_com</a><span title="Valid (one goal)" class="icon valid icofont-check"></span>
alt-ergo 500ns</pre><pre class="src"><span class="keyword">module</span> <a id="B" href="clones.B.html">clones.B</a><span title="1 parameter, 1 hypothesis, 0 instance found" class="icon small warning icofont-star"></span><span title="Valid (one goal)" class="icon valid icofont-check"></span></pre>
<pre class="src">
- <span class="keyword">axiom</span> <a id="B.A.neutral" href="clones.B.html#A.neutral">A.neutral</a>
+ <span class="keyword">axiom</span> <a id="B.A.neutral" href="clones.B.html#A.neutral">A.neutral</a><span title="uncloned hypothesis" class="icon small warning icofont-star"></span>
</pre>
<pre class="src">
<span class="keyword">goal</span> <a id="B.A.commutative" href="clones.B.html#A.commutative">A.commutative</a><span title="Valid (one goal)" class="icon valid icofont-check"></span>
diff --git a/tests/unsound.t/run.t b/tests/unsound.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..4d7055603a7c5242369258364dde0bafc0bb7155
--- /dev/null
+++ b/tests/unsound.t/run.t
@@ -0,0 +1,75 @@
+--------------------------------------------------------------------------
+--- Generating Documentation
+--------------------------------------------------------------------------
+ $ why3find doc unsound.mlw
+ Warning, file "unsound.mlw", line 10, characters 33-58: unused variable result
+ Warning, file "unsound.mlw", line 10, characters 27-30: unused variable foo
+ Generated $TESTCASE_ROOT/html/index.html
+--------------------------------------------------------------------------
+--- Generated Files
+--------------------------------------------------------------------------
+ $ cat html/unsound.*.html
+ <html>
+ <head>
+ <meta http-equiv="Content-Type" content="text/html;charset=utf-8">
+ <link rel="stylesheet" type="text/css" href="style.css">
+ <link rel="stylesheet" type="text/css" href="icofont.min.css">
+ <title>Module unsound.Dummy</title>
+ </head>
+ <body>
+ <header><a href="index.html">index</a> — <code>library <a href="unsound.index.html">unsound</a></code> — <code>module Dummy</code></header>
+ <pre class="src">
+ <span class="keyword">module</span> Dummy<a href="unsound.proof.html#Dummy" title="2 unsafe definitions" class="icon small failed icofont-star"></a><a href="unsound.proof.html#Dummy" title="Failed (no proof)" class="icon failed icofont-warning"></a>
+
+ <span class="keyword">let</span> <a id="admit1">admit1</a><span title="Unsound Definition" class="icon small failed icofont-star"></span><a href="unsound.proof.html#Dummy.admit1" title="Failed (no proof)" class="icon failed icofont-warning"></a> () : unit
+ <span class="keyword">ensures</span> { <span class="keyword">false</span> } = <span class="keyword">assume</span> { <span class="keyword">false</span> }
+
+ <span class="keyword">let</span> <a id="admit2">admit2</a><span title="Unsound Definition" class="icon small failed icofont-star"></span><a href="unsound.proof.html#Dummy.admit2" title="Failed (no proof)" class="icon failed icofont-warning"></a> () : unit
+ <span class="keyword">ensures</span> { <span class="keyword">false</span> } = <span class="keyword">val</span> foo () : unit <span class="keyword">ensures</span> { <span class="keyword">false</span> } <span class="keyword">in</span> foo ()
+
+ <span class="keyword">let</span> <a id="admit3">admit3</a><a href="unsound.proof.html#Dummy.admit3" title="Failed (no proof)" class="icon failed icofont-warning"></a> () : unit
+ <span class="keyword">ensures</span> { <span class="keyword">true</span> } = <span class="keyword">let</span> foo = <span class="keyword">any</span> unit <span class="keyword">ensures</span> { <span class="keyword">true</span> } <span class="keyword">in</span> ()
+
+ <span class="keyword">end</span>
+ </pre>
+ <script type="text/javascript" src="script.js"></script>
+ </body>
+ </html>
+ <html>
+ <head>
+ <meta http-equiv="Content-Type" content="text/html;charset=utf-8">
+ <link rel="stylesheet" type="text/css" href="style.css">
+ <link rel="stylesheet" type="text/css" href="icofont.min.css">
+ <title>Library unsound</title>
+ </head>
+ <body>
+ <header><a href="index.html">index</a> — <code>library unsound</code></header>
+ <pre class="src"><span class="keyword">module</span> <a title="unsound.Dummy" href="unsound.Dummy.html">Dummy</a><a href="unsound.proof.html#Dummy" title="2 unsafe definitions" class="icon small failed icofont-star"></a><a href="unsound.proof.html#Dummy" title="Failed (no proof)" class="icon failed icofont-warning"></a></pre>
+ <script type="text/javascript" src="script.js"></script>
+ </body>
+ </html>
+ <html>
+ <head>
+ <meta http-equiv="Content-Type" content="text/html;charset=utf-8">
+ <link rel="stylesheet" type="text/css" href="style.css">
+ <link rel="stylesheet" type="text/css" href="icofont.min.css">
+ <title>Library unsound</title>
+ </head>
+ <body>
+ <header><a href="index.html">index</a> — <code>library <a href="unsound.index.html">unsound</a></code> — <code>proofs</code></header>
+ <h1>Provers</h1>
+ <pre class="src">
+ </pre>
+ <h1>Proofs</h1>
+ <pre class="src"><span class="keyword">module</span> <a id="Dummy" href="unsound.Dummy.html">unsound.Dummy</a><span title="2 unsafe definitions" class="icon small failed icofont-star"></span><span title="Failed (no proof)" class="icon failed icofont-warning"></span></pre>
+ <pre class="src">
+ <span class="keyword">unsound</span> <a id="Dummy.admit1" href="unsound.Dummy.html#admit1">admit1</a><span title="unsafe definition" class="icon small failed icofont-star"></span>
+ <span class="keyword">unsound</span> <a id="Dummy.admit2" href="unsound.Dummy.html#admit2">admit2</a><span title="unsafe definition" class="icon small failed icofont-star"></span>
+ </pre>
+ <pre class="src">
+ <span class="keyword">goal</span> <a id="Dummy.admit1" href="unsound.Dummy.html#admit1">admit1</a><span title="Failed (no proof)" class="icon failed icofont-warning"></span></pre><pre class="src">
+ <span class="keyword">goal</span> <a id="Dummy.admit2" href="unsound.Dummy.html#admit2">admit2</a><span title="Failed (no proof)" class="icon failed icofont-warning"></span></pre><pre class="src">
+ <span class="keyword">goal</span> <a id="Dummy.admit3" href="unsound.Dummy.html#admit3">admit3</a><span title="Failed (no proof)" class="icon failed icofont-warning"></span></pre><script type="text/javascript" src="script.js"></script>
+ </body>
+ </html>
+--------------------------------------------------------------------------
diff --git a/tests/unsound.t/unsound.mlw b/tests/unsound.t/unsound.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..afe80593f0bb7df392aae81f4b27914bd8999a6d
--- /dev/null
+++ b/tests/unsound.t/unsound.mlw
@@ -0,0 +1,12 @@
+module Dummy
+
+ let admit1 () : unit
+ ensures { false } = assume { false }
+
+ let admit2 () : unit
+ ensures { false } = val foo () : unit ensures { false } in foo ()
+
+ let admit3 () : unit
+ ensures { true } = let foo = any unit ensures { true } in ()
+
+end