From 14cd24e5784ab62d54b8bc055d5c04c60c5f4c5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 7 Jul 2023 17:38:08 +0200
Subject: [PATCH] [prove] highlight unsound values
---
src/prove.ml | 24 +++++++++++++++---------
tests/unsound.t/run.t | 13 +++++++++----
tests/unsound.t/unsound.mlw | 6 +++++-
3 files changed, 29 insertions(+), 14 deletions(-)
diff --git a/src/prove.ml b/src/prove.ml
index f9a6e11c..5fbd251c 100644
--- a/src/prove.ml
+++ b/src/prove.ml
@@ -133,15 +133,17 @@ let hypotheses = "Hypothesis",ref 0
let parameters = "Parameter ",ref 0
let procedures = "Procedure ",ref 0
let externalized = "External ",ref 0
+let unsoundness = "Unsound ",ref 0
let print_axioms_stats () =
+ let u = !(snd unsoundness) in
let p = !(snd parameters) in
let h = !(snd hypotheses) in
let r = !(snd procedures) in
let e = !(snd externalized) in
let d = !(snd dependencies) in
let s = !(snd standardized) in
- if p+h+r+e+d+s = 0 then
+ if u+p+h+r+e+d+s = 0 then
Format.printf "Hypotheses: none@."
else
begin
@@ -156,11 +158,15 @@ let print_axioms_stats () =
Format.printf " - externalized: @{<orange>%d@}@\n" e ;
if s > 0 then
Format.printf " - standardized: @{<orange>%d@}@\n" s ;
+ if u > 0 then
+ Format.printf " - unsound%a: @{<red>%d@}@\n" Utils.pp_s u u ;
if d > 0 then
Format.printf " - dependenc%a: @{<red>%d@}@\n" Utils.pp_yies d d ;
Format.print_flush ()
end
+let pp_print_red fmt = Format.fprintf fmt "@{<red>%s@}"
+
let report_parameter ~lib ~signature (prm : Axioms.parameter) =
try
let id = Axioms.ident prm.param in
@@ -172,21 +178,21 @@ let report_parameter ~lib ~signature (prm : Axioms.parameter) =
((!builtins && builtin) || (!externals || not extern))
then
begin
- let kind, param =
+ let pp, kind, param =
match prm.param with
- | Type _ -> "type ", parameters
- | Logic _ -> "logic", parameters
- | Param _ -> "param", parameters
- | Value _ -> "value", procedures
- | Axiom _ -> "axiom", hypotheses
- | Unsafe _ -> "unsafe", procedures
+ | Type _ -> Format.pp_print_string,"type ", parameters
+ | Logic _ -> Format.pp_print_string,"logic", parameters
+ | Param _ -> Format.pp_print_string,"param", parameters
+ | Value _ -> Format.pp_print_string,"value", procedures
+ | Axiom _ -> Format.pp_print_string,"axiom", hypotheses
+ | Unsafe _ -> pp_print_red,"value", unsoundness
in
let action, count =
if builtin || extern then externalized else
if signature then param else
if std then standardized else dependencies
in incr count ;
- Format.printf " %s %s %a" action kind Id.pp_title ident ;
+ Format.printf " %a %s %a" pp action kind Id.pp_title ident ;
let categories = List.filter (fun c -> c <> "") [
if std then "stdlib" else "" ;
if builtin then "builtin" else "" ;
diff --git a/tests/unsound.t/run.t b/tests/unsound.t/run.t
index 4d705560..bf22c637 100644
--- a/tests/unsound.t/run.t
+++ b/tests/unsound.t/run.t
@@ -2,8 +2,8 @@
--- 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
+ Warning, file "unsound.mlw", line 11, characters 33-58: unused variable result
+ Warning, file "unsound.mlw", line 11, characters 27-30: unused variable foo
Generated $TESTCASE_ROOT/html/index.html
--------------------------------------------------------------------------
--- Generated Files
@@ -20,6 +20,7 @@
<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">use</span> int.<a title="int.Int" href="https://why3.lri.fr/stdlib/int.html#Int_">Int</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> }
@@ -27,9 +28,12 @@
<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">let</span> <a id="ok_unit">ok_unit</a><a href="unsound.proof.html#Dummy.ok_unit" 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">let</span> <a id="ok_some">ok_some</a><a href="unsound.proof.html#Dummy.ok_some" title="Failed (no proof)" class="icon failed icofont-warning"></a> () : int
+ <span class="keyword">ensures</span> { result <a title="int.Int.(>=)" href="https://why3.lri.fr/stdlib/int.html#infix%20%3E=_26">>=</a> 0 } = <span class="keyword">let</span> foo = <span class="keyword">any</span> int <span class="keyword">ensures</span> { result <a title="int.Int.(>=)" href="https://why3.lri.fr/stdlib/int.html#infix%20%3E=_26">>=</a> 0 } <span class="keyword">in</span> foo
+
<span class="keyword">end</span>
</pre>
<script type="text/javascript" src="script.js"></script>
@@ -69,7 +73,8 @@
<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>
+ <span class="keyword">goal</span> <a id="Dummy.ok_unit" href="unsound.Dummy.html#ok_unit">ok_unit</a><span title="Failed (no proof)" class="icon failed icofont-warning"></span></pre><pre class="src">
+ <span class="keyword">goal</span> <a id="Dummy.ok_some" href="unsound.Dummy.html#ok_some">ok_some</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
index afe80593..7f1eb3aa 100644
--- a/tests/unsound.t/unsound.mlw
+++ b/tests/unsound.t/unsound.mlw
@@ -1,4 +1,5 @@
module Dummy
+ use int.Int
let admit1 () : unit
ensures { false } = assume { false }
@@ -6,7 +7,10 @@ module Dummy
let admit2 () : unit
ensures { false } = val foo () : unit ensures { false } in foo ()
- let admit3 () : unit
+ let ok_unit () : unit
ensures { true } = let foo = any unit ensures { true } in ()
+ let ok_some () : int
+ ensures { result >= 0 } = let foo = any int ensures { result >= 0 } in foo
+
end
--
GitLab