From 4f7af118724ea38549c439f0e4af07fd3f554a16 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 14 Mar 2019 17:32:28 +0100
Subject: [PATCH] [Tagset] give bounds for max_tags

---
 examples/stdlib/tagset/why3session.xml | 6 ++++--
 stdlib/mach/tagset.mlw                 | 4 +++-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/examples/stdlib/tagset/why3session.xml b/examples/stdlib/tagset/why3session.xml
index 1b8ec3055..fd02dce7a 100644
--- a/examples/stdlib/tagset/why3session.xml
+++ b/examples/stdlib/tagset/why3session.xml
@@ -34,7 +34,9 @@
  <proof prover="1"><result status="valid" time="0.11"/></proof>
  </goal>
  <goal name="VC max_tags" expl="VC for max_tags" proved="true">
+ <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="valid" time="0.09"/></proof>
+ <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
  </goal>
  <goal name="VC resize" expl="VC for resize" proved="true">
  <transf name="split_vc" proved="true" >
@@ -209,7 +211,7 @@
   <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC remove.22" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.05" steps="161"/></proof>
+  <proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
   </goal>
  </transf>
  </goal>
@@ -291,7 +293,7 @@
  <goal name="Iterator.VC next" expl="VC for next" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC next.0" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="109"/></proof>
   </goal>
   <goal name="VC next.1" expl="index in array bounds" proved="true">
   <proof prover="1"><result status="valid" time="0.06"/></proof>
diff --git a/stdlib/mach/tagset.mlw b/stdlib/mach/tagset.mlw
index 1add3e7cb..2828d8775 100644
--- a/stdlib/mach/tagset.mlw
+++ b/stdlib/mach/tagset.mlw
@@ -53,6 +53,7 @@ module TagSetIntf
 
   val function max_tags (h: t) : Int63.int63
     ensures { forall v. S.mem v h.elts -> tag v <= result }
+    ensures { -1 <= result  < Int63.max_int63 }
 
   val add (h: t) (k: key): unit
     requires { k <> S.dummy }
@@ -156,7 +157,8 @@ module TagSet
      tag k < Array.length h.iterated.value && Array.(S.tag h.iterated.value[tag k] <> S.tag S.dummy)
 
   let function max_tags (h: t) : Int63.int63
-    ensures { forall v. S.mem v h.elts -> tag v <= result } =
+    ensures { forall v. S.mem v h.elts -> tag v <= result }
+    ensures { -1 <= result  < Int63.max_int63 } =
     Array.(length h.iterated.value) - 1
 
   let resize (h:t) (k:key) : unit
-- 
GitLab