Skip to content

Commit

Permalink
Update test cases
Browse files Browse the repository at this point in the history
  • Loading branch information
@xldenis
xldenis committed Nov 9, 2023
1 parent 4bdd004 commit 193ba00
Show file tree
Hide file tree
Showing 32 changed files with 306 additions and 67 deletions.
6 changes: 3 additions & 3 deletions creusot/tests/should_succeed/hillel/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -232,13 +232,13 @@
<proof prover="4"><result status="valid" time="0.020000" steps="163"/></proof>
</goal>
<goal name="fulcrum&#39;vc.21" expl="index in bounds" proved="true">
<proof prover="0"><result status="valid" time="0.190000" steps="27989"/></proof>
<proof prover="0"><result status="valid" time="0.190000" steps="27987"/></proof>
</goal>
<goal name="fulcrum&#39;vc.22" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.020000" steps="92"/></proof>
</goal>
<goal name="fulcrum&#39;vc.23" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.217213" steps="52303"/></proof>
<proof prover="0"><result status="valid" time="0.217213" steps="52301"/></proof>
</goal>
<goal name="fulcrum&#39;vc.24" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.010000" steps="157"/></proof>
Expand Down Expand Up @@ -278,7 +278,7 @@
</transf>
</goal>
<goal name="fulcrum&#39;vc.35" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.076927" steps="22882"/></proof>
<proof prover="0"><result status="valid" time="0.076927" steps="22877"/></proof>
</goal>
</transf>
</goal>
Expand Down
Binary file modified creusot/tests/should_succeed/hillel/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/01_range/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/02_iter_mut/why3shapes.gz
View file
Binary file not shown.
9 changes: 5 additions & 4 deletions creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,19 +3,20 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="03_std_iterators.mlcfg"/>
<theory name="C03StdIterators_SliceIter" proved="true">
<goal name="slice_iter&#39;vc" expl="VC for slice_iter" proved="true">
<proof prover="3"><result status="valid" time="0.158075" steps="1324"/></proof>
<proof prover="1"><result status="valid" time="0.158075" steps="1313"/></proof>
</goal>
</theory>
<theory name="C03StdIterators_VecIter" proved="true">
<goal name="vec_iter&#39;vc" expl="VC for vec_iter" proved="true">
<proof prover="3"><result status="valid" time="0.068472" steps="1242"/></proof>
<proof prover="1"><result status="valid" time="0.068472" steps="1232"/></proof>
</goal>
</theory>
<theory name="C03StdIterators_AllZero" proved="true">
Expand All @@ -25,7 +26,7 @@
</theory>
<theory name="C03StdIterators_SkipTake" proved="true">
<goal name="skip_take&#39;vc" expl="VC for skip_take" proved="true">
<proof prover="3"><result status="valid" time="0.020000" steps="239"/></proof>
<proof prover="1"><result status="valid" time="0.020000" steps="240"/></proof>
</goal>
</theory>
<theory name="C03StdIterators_Counter_Closure0" proved="true">
Expand Down Expand Up @@ -74,7 +75,7 @@
</theory>
<theory name="C03StdIterators_SumRange" proved="true">
<goal name="sum_range&#39;vc" expl="VC for sum_range" proved="true">
<proof prover="3"><result status="valid" time="0.111099" steps="1655"/></proof>
<proof prover="1"><result status="valid" time="0.111099" steps="1654"/></proof>
</goal>
</theory>
<theory name="C03StdIterators_EnumerateRange" proved="true">
Expand Down
Binary file modified creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/05_map/why3shapes.gz
View file
Binary file not shown.
54 changes: 27 additions & 27 deletions creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
<goal name="produces_refl&#39;vc.0.0" expl="postcondition" proved="true">
<transf name="use_th" proved="true" arg1="seq.FreeMonoid">
<goal name="produces_refl&#39;vc.0.0.0" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.234741" steps="39281"/></proof>
<proof prover="4"><result status="valid" time="0.234741" steps="39188"/></proof>
</goal>
</transf>
</goal>
Expand Down Expand Up @@ -72,19 +72,19 @@
<proof prover="0"><result status="valid" time="0.010000" steps="50"/></proof>
</goal>
<goal name="produces_trans&#39;vc.0.1.0.4.0.2" proved="true">
<proof prover="0"><result status="valid" time="0.039524" steps="586"/></proof>
<proof prover="0"><result status="valid" time="0.039524" steps="559"/></proof>
</goal>
<goal name="produces_trans&#39;vc.0.1.0.4.0.3" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="88"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="85"/></proof>
</goal>
<goal name="produces_trans&#39;vc.0.1.0.4.0.4" proved="true">
<proof prover="0"><result status="valid" time="0.030000" steps="274"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="259"/></proof>
</goal>
<goal name="produces_trans&#39;vc.0.1.0.4.0.5" proved="true">
<proof prover="0"><result status="valid" time="0.020000" steps="230"/></proof>
<proof prover="0"><result status="valid" time="0.020000" steps="218"/></proof>
</goal>
<goal name="produces_trans&#39;vc.0.1.0.4.0.6" proved="true">
<proof prover="0"><result status="valid" time="0.150000" steps="618"/></proof>
<proof prover="0"><result status="valid" time="0.150000" steps="596"/></proof>
</goal>
<goal name="produces_trans&#39;vc.0.1.0.4.0.7" proved="true">
<transf name="instantiate" proved="true" arg1="H2" arg2="(i-length ab)">
Expand All @@ -93,7 +93,7 @@
<goal name="produces_trans&#39;vc.0.1.0.4.0.7.0.0" proved="true">
<transf name="use_th" proved="true" arg1="seq.FreeMonoid">
<goal name="produces_trans&#39;vc.0.1.0.4.0.7.0.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.507833" steps="7161"/></proof>
<proof prover="0"><result status="valid" time="0.507833" steps="6847"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -108,7 +108,7 @@
<goal name="produces_trans&#39;vc.0.1.0.4.0.8.0.0" proved="true">
<transf name="use_th" proved="true" arg1="seq.FreeMonoid">
<goal name="produces_trans&#39;vc.0.1.0.4.0.8.0.0.0" proved="true">
<proof prover="0" timelimit="30" memlimit="4000"><result status="valid" time="0.463977" steps="6890"/></proof>
<proof prover="0" timelimit="30" memlimit="4000"><result status="valid" time="0.463977" steps="6446"/></proof>
</goal>
</transf>
</goal>
Expand Down Expand Up @@ -139,7 +139,7 @@
<goal name="produces_one&#39;vc.0.0.0" expl="VC for produces_one" proved="true">
<transf name="split_vc" proved="true" >
<goal name="produces_one&#39;vc.0.0.0.0" expl="VC for produces_one" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="118"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="114"/></proof>
</goal>
<goal name="produces_one&#39;vc.0.0.0.1" expl="VC for produces_one" proved="true">
<transf name="exists" proved="true" arg1="(singleton e)">
Expand Down Expand Up @@ -169,7 +169,7 @@
<proof prover="0"><result status="valid" time="0.026703" steps="24"/></proof>
</goal>
<goal name="produces_one&#39;vc.0.0.0.1.0.4.0.1" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="28"/></proof>
<proof prover="0"><result status="valid" time="0.010000" steps="27"/></proof>
</goal>
<goal name="produces_one&#39;vc.0.0.0.1.0.4.0.2" proved="true">
<proof prover="0"><result status="valid" time="0.010000" steps="28"/></proof>
Expand All @@ -189,14 +189,14 @@
<goal name="produces_one&#39;vc.0.0.0.1.0.4.0.7" proved="true">
<transf name="use_th" proved="true" arg1="seq.FreeMonoid">
<goal name="produces_one&#39;vc.0.0.0.1.0.4.0.7.0" proved="true">
<proof prover="0"><result status="valid" time="0.030000" steps="398"/></proof>
<proof prover="0"><result status="valid" time="0.030000" steps="393"/></proof>
</goal>
</transf>
</goal>
<goal name="produces_one&#39;vc.0.0.0.1.0.4.0.8" proved="true">
<transf name="use_th" proved="true" arg1="seq.FreeMonoid">
<goal name="produces_one&#39;vc.0.0.0.1.0.4.0.8.0" proved="true">
<proof prover="0"><result status="valid" time="0.027414" steps="402"/></proof>
<proof prover="0"><result status="valid" time="0.027414" steps="396"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -215,7 +215,7 @@
<goal name="produces_one&#39;vc.0.1" expl="postcondition" proved="true">
<transf name="use_th" proved="true" arg1="seq.FreeMonoid">
<goal name="produces_one&#39;vc.0.1.0" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.128957" steps="38075"/></proof>
<proof prover="4"><result status="valid" time="0.128957" steps="37983"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -230,13 +230,13 @@
<goal name="produces_one_invariant&#39;vc.0" expl="VC for produces_one_invariant" proved="true">
<transf name="split_vc" proved="true" >
<goal name="produces_one_invariant&#39;vc.0.0" expl="assertion" proved="true">
<proof prover="4" timelimit="5"><result status="valid" time="0.054265" steps="17223"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.054265" steps="17114"/></proof>
</goal>
<goal name="produces_one_invariant&#39;vc.0.1" expl="postcondition" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.096337" steps="1828"/></proof>
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.096337" steps="1823"/></proof>
</goal>
<goal name="produces_one_invariant&#39;vc.0.2" expl="postcondition" proved="true">
<proof prover="4" timelimit="5"><result status="valid" time="0.335330" steps="76040"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.335330" steps="74202"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -253,37 +253,37 @@
<proof prover="0"><result status="valid" time="0.024082" steps="18"/></proof>
</goal>
<goal name="next&#39;vc.2" expl="type invariant" proved="true">
<proof prover="4" timelimit="5"><result status="valid" time="0.079981" steps="12268"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.079981" steps="12137"/></proof>
</goal>
<goal name="next&#39;vc.3" expl="type invariant" proved="true">
<proof prover="0"><result status="valid" time="0.013144" steps="410"/></proof>
<proof prover="0"><result status="valid" time="0.013144" steps="610"/></proof>
</goal>
<goal name="next&#39;vc.4" expl="type invariant" proved="true">
<proof prover="0"><result status="valid" time="0.024006" steps="29"/></proof>
</goal>
<goal name="next&#39;vc.5" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.025172" steps="170"/></proof>
<proof prover="0"><result status="valid" time="0.025172" steps="230"/></proof>
</goal>
<goal name="next&#39;vc.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.015449" steps="64"/></proof>
</goal>
<goal name="next&#39;vc.7" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.013939" steps="62"/></proof>
<proof prover="0"><result status="valid" time="0.013939" steps="61"/></proof>
</goal>
<goal name="next&#39;vc.8" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.015299" steps="63"/></proof>
</goal>
<goal name="next&#39;vc.9" expl="type invariant" proved="true">
<proof prover="4"><result status="valid" time="0.136766" steps="14624"/></proof>
<proof prover="4"><result status="valid" time="0.136766" steps="14513"/></proof>
</goal>
<goal name="next&#39;vc.10" expl="type invariant" proved="true">
<proof prover="4"><result status="valid" time="0.113274" steps="21386"/></proof>
<proof prover="4"><result status="valid" time="0.113274" steps="71025"/></proof>
</goal>
<goal name="next&#39;vc.11" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.012501" steps="26"/></proof>
</goal>
<goal name="next&#39;vc.12" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.073346" steps="26481"/></proof>
<proof prover="4"><result status="valid" time="0.073346" steps="26348"/></proof>
</goal>
<goal name="next&#39;vc.13" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.015445" steps="7"/></proof>
Expand All @@ -293,7 +293,7 @@
</theory>
<theory name="C06MapPrecond_Map" proved="true">
<goal name="map&#39;vc" expl="VC for map" proved="true">
<proof prover="4" timelimit="5"><result status="valid" time="0.044619" steps="10257"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.044619" steps="9983"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Identity_Closure0" proved="true">
Expand Down Expand Up @@ -333,7 +333,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.026428" steps="8"/></proof>
</goal>
<goal name="increment&#39;vc.6" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.069975" steps="332191"/></proof>
<proof prover="1"><result status="valid" time="0.069975" steps="449905"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -345,15 +345,15 @@
</theory>
<theory name="C06MapPrecond_Counter" proved="true">
<goal name="counter&#39;vc" expl="VC for counter" proved="true">
<proof prover="0"><result status="valid" time="0.054988" steps="808"/></proof>
<proof prover="0"><result status="valid" time="0.054988" steps="806"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Impl0" proved="true">
<goal name="produces_refl_refn" proved="true">
<proof prover="0"><result status="valid" time="0.000000" steps="0"/></proof>
</goal>
<goal name="next_refn" proved="true">
<proof prover="0"><result status="valid" time="0.079489" steps="1269"/></proof>
<proof prover="0"><result status="valid" time="0.079489" steps="1244"/></proof>
</goal>
<goal name="produces_trans_refn" proved="true">
<proof prover="0"><result status="valid" time="0.000000" steps="0"/></proof>
Expand Down
Binary file modified creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/07_fuse/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/09_empty/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/10_once/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/11_repeat/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/13_cloned/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz
View file
Binary file not shown.
Binary file modified creusot/tests/should_succeed/iterators/16_take/why3shapes.gz
View file
Binary file not shown.
4 changes: 2 additions & 2 deletions creusot/tests/should_succeed/knapsack_full/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -264,7 +264,7 @@
<proof prover="6"><result status="valid" time="0.049064" steps="149"/></proof>
</goal>
<goal name="knapsack01_dyn&#39;vc.76" expl="loop invariant preservation" proved="true">
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.074734" steps="1276"/></proof>
<proof prover="6" timelimit="5" memlimit="2000"><result status="valid" time="0.074734" steps="1274"/></proof>
</goal>
<goal name="knapsack01_dyn&#39;vc.77" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.036400" steps="184710"/></proof>
Expand Down Expand Up @@ -370,7 +370,7 @@
<goal name="knapsack01_dyn&#39;vc.110.0" expl="loop invariant preservation" proved="true">
<transf name="split_vc" proved="true" >
<goal name="knapsack01_dyn&#39;vc.110.0.0" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.423537" steps="96081"/></proof>
<proof prover="0"><result status="valid" time="0.423537" steps="96078"/></proof>
</goal>
<goal name="knapsack01_dyn&#39;vc.110.0.1" expl="loop invariant preservation" proved="true">
<transf name="inline_goal" proved="true" >
Expand Down
Binary file modified creusot/tests/should_succeed/knapsack_full/why3shapes.gz
View file
Binary file not shown.
Loading

0 comments on commit 193ba00

Please sign in to comment.