Update proofs!!

colis-anr · Feb 20, 2020 · c4497c1 · c4497c1
1 parent 21ec2e5
commit c4497c1
Show file tree

Hide file tree

Showing 8 changed files with 1,220 additions and 1,198 deletions.
diff --git a/src/concrete/interpreter.mlw b/src/concrete/interpreter.mlw
@@ -14,7 +14,8 @@ module Semantics
 
   (* Instantiate the concrete semantics with our dummy filesystem *)
   clone export semantics.Semantics with
-    type filesystem = unit
+    type filesystem = unit,
+    axiom interp_utility_extends_output
 end
 
 module State

diff --git a/src/concrete/interpreter/why3session.xml b/src/concrete/interpreter/why3session.xml
diff --git a/src/concrete/interpreter/why3shapes.gz b/src/concrete/interpreter/why3shapes.gz
diff --git a/src/concrete/semantics/why3session.xml b/src/concrete/semantics/why3session.xml
@@ -169,13 +169,15 @@
  </transf>
  </goal>
 </theory>
-<theory name="Semantics" proved="true">
+<theory name="Context" proved="true">
  <goal name="add_var_bindings&#39;vc" expl="VC for add_var_bindings" proved="true">
- <proof prover="5"><result status="valid" time="0.02" steps="83"/></proof>
+ <proof prover="1" timelimit="1" memlimit="1000"><result status="valid" time="0.06" steps="18917"/></proof>
  </goal>
  <goal name="same_context" proved="true">
- <proof prover="5"><result status="valid" time="0.03" steps="28"/></proof>
+ <proof prover="1" timelimit="1" memlimit="1000"><result status="valid" time="0.06" steps="16802"/></proof>
  </goal>
+</theory>
+<theory name="Semantics" proved="true">
  <goal name="no_while_incomplete&#39;vc" expl="VC for no_while_incomplete" proved="true">
  <proof prover="5" timelimit="10"><result status="valid" time="1.02" steps="449"/></proof>
  </goal>
@@ -186,7 +188,7 @@
  <proof prover="5"><result status="valid" time="0.21" steps="143"/></proof>
  </goal>
  <goal name="eval_foreach_concat&#39;vc" expl="VC for eval_foreach_concat" proved="true">
- <proof prover="5" timelimit="10"><result status="valid" time="3.24" steps="970"/></proof>
+ <proof prover="5" timelimit="10"><result status="valid" time="2.60" steps="970"/></proof>
  </goal>
  <goal name="eval_foreach_last&#39;vc" expl="VC for eval_foreach_last" proved="true">
  <transf name="split_vc" proved="true" >
@@ -195,15 +197,15 @@
    <goal name="eval_foreach_last&#39;vc.0.0" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="eval_foreach_last&#39;vc.0.0.0" expl="postcondition" proved="true">
-    <proof prover="5" timelimit="10" memlimit="4000"><result status="valid" time="2.21" steps="719"/></proof>
+    <proof prover="5" timelimit="10" memlimit="4000"><result status="valid" time="1.77" steps="719"/></proof>
     </goal>
    </transf>
    </goal>
    <goal name="eval_foreach_last&#39;vc.0.1" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.07" steps="26"/></proof>
+   <proof prover="5"><result status="valid" time="0.13" steps="26"/></proof>
    </goal>
    <goal name="eval_foreach_last&#39;vc.0.2" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.27" steps="44"/></proof>
+   <proof prover="5"><result status="valid" time="0.24" steps="44"/></proof>
    </goal>
   </transf>
   </goal>
@@ -213,10 +215,10 @@
    <proof prover="5"><result status="valid" time="0.09" steps="39"/></proof>
    </goal>
    <goal name="eval_foreach_last&#39;vc.1.1" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.11" steps="26"/></proof>
+   <proof prover="5"><result status="valid" time="0.13" steps="26"/></proof>
    </goal>
    <goal name="eval_foreach_last&#39;vc.1.2" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.43" steps="115"/></proof>
+   <proof prover="5"><result status="valid" time="0.27" steps="115"/></proof>
    </goal>
   </transf>
   <transf name="split_vc" proved="true" >

diff --git a/src/concrete/semantics/why3shapes.gz b/src/concrete/semantics/why3shapes.gz
diff --git a/src/symbolic/symbolicInterpreter.mlw b/src/symbolic/symbolicInterpreter.mlw
@@ -26,7 +26,8 @@ module Interpreter
     end
 
     clone export semantics.Semantics with
-      type filesystem = filesystem
+      type filesystem = filesystem,
+      axiom interp_utility_extends_output
 
     scope MakeInterpreter
 

diff --git a/src/symbolic/symbolicInterpreter/why3session.xml b/src/symbolic/symbolicInterpreter/why3session.xml
diff --git a/src/symbolic/symbolicInterpreter/why3shapes.gz b/src/symbolic/symbolicInterpreter/why3shapes.gz