[prove] highlight unsound values

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 "" ;

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">&gt;=</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">&gt;=</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>
 --------------------------------------------------------------------------

tests/unsound.t/unsound.mlw

 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