Skip to content

Commit

Permalink
Update sessions
Browse files Browse the repository at this point in the history
  • Loading branch information
@dewert99
dewert99 committed Jul 25, 2024
1 parent 15dcef7 commit 09a5e44
Show file tree
Hide file tree
Showing 6 changed files with 194 additions and 0 deletions.
73 changes: 73 additions & 0 deletions creusot/tests/should_succeed/heapsort_generic/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,73 @@
<prover id="3" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="coma" proved="true">
<path name=".."/><path name="heapsort_generic.coma"/>
<theory name="Core_Cmp_Ordering_Type" proved="true">
<goal name="vc_less" proved="true">
<proof prover="3"><result status="valid" time="0.008128" steps="27"/></proof>
</goal>
<goal name="vc_equal" proved="true">
<proof prover="3"><result status="valid" time="0.016468" steps="27"/></proof>
</goal>
<goal name="vc_greater" proved="true">
<proof prover="3"><result status="valid" time="0.015901" steps="27"/></proof>
</goal>
</theory>
<theory name="HeapsortGeneric_HeapFragMax_Impl" proved="true">
<goal name="vc_heap_frag_max" proved="true">
<proof prover="3"><result status="valid" time="0.058313" steps="14037"/></proof>
</goal>
</theory>
<theory name="Core_Ptr_NonNull_NonNull_Type" proved="true">
<goal name="vc_t_nonnull" proved="true">
<proof prover="3"><result status="valid" time="0.006210" steps="27"/></proof>
</goal>
</theory>
<theory name="Core_Marker_PhantomData_Type" proved="true">
<goal name="vc_t_phantomdata" proved="true">
<proof prover="3"><result status="valid" time="0.009209" steps="27"/></proof>
</goal>
</theory>
<theory name="Core_Ptr_Unique_Unique_Type" proved="true">
<goal name="vc_t_unique" proved="true">
<proof prover="3"><result status="valid" time="0.004976" steps="27"/></proof>
</goal>
</theory>
<theory name="Alloc_RawVec_Cap_Type" proved="true">
<goal name="vc_t_cap" proved="true">
<proof prover="3"><result status="valid" time="0.002710" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_RawVec_RawVec_Type" proved="true">
<goal name="vc_t_rawvec" proved="true">
<proof prover="3"><result status="valid" time="0.000001" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_Vec_Vec_Type" proved="true">
<goal name="vc_t_vec" proved="true">
<proof prover="3"><result status="valid" time="0.004103" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_Alloc_Global_Type" proved="true">
<goal name="vc_t_global" proved="true">
<proof prover="3"><result status="valid" time="0.000001" steps="27"/></proof>
</goal>
</theory>
<theory name="HeapsortGeneric_SiftDown" proved="true">
<goal name="vc_swap&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.028525" steps="11390"/></proof>
</goal>
<goal name="vc_deref_mut&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.021035" steps="11390"/></proof>
</goal>
<goal name="vc_le&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.020693" steps="11390"/></proof>
</goal>
<goal name="vc_lt&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.020517" steps="11390"/></proof>
</goal>
<goal name="vc_index&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.016194" steps="11390"/></proof>
</goal>
<goal name="vc_sift_down" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_sift_down.0" expl="type invariant" proved="true">
Expand Down Expand Up @@ -248,6 +309,18 @@
</goal>
</theory>
<theory name="HeapsortGeneric_HeapSort" proved="true">
<goal name="vc_swap&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.022747" steps="12937"/></proof>
</goal>
<goal name="vc_deref_mut&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.024721" steps="12937"/></proof>
</goal>
<goal name="vc_sift_down&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.022190" steps="12937"/></proof>
</goal>
<goal name="vc_len&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.023049" steps="12937"/></proof>
</goal>
<goal name="vc_heap_sort" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_heap_sort.0" expl="type invariant" proved="true">
Expand Down
Binary file modified creusot/tests/should_succeed/heapsort_generic/why3shapes.gz
View file
Binary file not shown.
43 changes: 43 additions & 0 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 @@ -7,6 +7,11 @@
<prover id="4" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="coma" proved="true">
<path name=".."/><path name="06_map_precond.coma"/>
<theory name="C06MapPrecond_Map_Type" proved="true">
<goal name="vc_t_map" proved="true">
<proof prover="4"><result status="valid" time="0.033707" steps="3720"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Impl1_PreservationInv_Impl" proved="true">
<goal name="vc_preservation_inv" proved="true">
<transf name="use_th" proved="true" arg1="seq.FreeMonoid">
Expand Down Expand Up @@ -129,6 +134,14 @@
</transf>
</goal>
</theory>
<theory name="Core_Option_Option_Type" proved="true">
<goal name="vc_none" proved="true">
<proof prover="4"><result status="valid" time="0.004507" steps="27"/></proof>
</goal>
<goal name="vc_some" proved="true">
<proof prover="4"><result status="valid" time="0.007780" steps="27"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Impl1_ProducesOne_Impl" proved="true">
<goal name="vc_produces_one" proved="true">
<transf name="split_vc" proved="true" >
Expand Down Expand Up @@ -270,6 +283,12 @@
</goal>
</theory>
<theory name="C06MapPrecond_Impl0_Next" proved="true">
<goal name="vc_call_mut&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.018075" steps="9365"/></proof>
</goal>
<goal name="vc_next&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.017797" steps="9365"/></proof>
</goal>
<goal name="vc_next" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_next.0" expl="precondition" proved="true">
Expand Down Expand Up @@ -328,22 +347,38 @@
<proof prover="4" timelimit="5"><result status="valid" time="0.025407" steps="9843"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Identity_Closure0_Type" proved="true">
<goal name="vc_c06mapprecond_identity_closure0" proved="true">
<proof prover="4"><result status="valid" time="0.008745" steps="3879"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Identity_Closure0" proved="true">
<goal name="vc_c06mapprecond_identity_closure0" proved="true">
<proof prover="1"><result status="valid" time="0.012097" steps="3"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Identity" proved="true">
<goal name="vc_map&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.010900" steps="7175"/></proof>
</goal>
<goal name="vc_identity" proved="true">
<proof prover="1"><result status="valid" time="0.016418" steps="210"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Increment_Closure2_Type" proved="true">
<goal name="vc_c06mapprecond_increment_closure2" proved="true">
<proof prover="4"><result status="valid" time="0.008792" steps="4038"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Increment_Closure2" proved="true">
<goal name="vc_c06mapprecond_increment_closure2" proved="true">
<proof prover="1"><result status="valid" time="0.009703" steps="8"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Increment" proved="true">
<goal name="vc_map&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.023452" steps="11423"/></proof>
</goal>
<goal name="vc_increment" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_increment.0" expl="precondition" proved="true">
Expand All @@ -370,12 +405,20 @@
</transf>
</goal>
</theory>
<theory name="C06MapPrecond_Counter_Closure2_Type" proved="true">
<goal name="vc_c06mapprecond_counter_closure2" proved="true">
<proof prover="4"><result status="valid" time="0.015425" steps="4197"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Counter_Closure2" proved="true">
<goal name="vc_c06mapprecond_counter_closure2" proved="true">
<proof prover="1"><result status="valid" time="0.013350" steps="123"/></proof>
</goal>
</theory>
<theory name="C06MapPrecond_Counter" proved="true">
<goal name="vc_map&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.022737" steps="8253"/></proof>
</goal>
<goal name="vc_counter" proved="true">
<proof prover="1"><result status="valid" time="0.053608" steps="676"/></proof>
</goal>
Expand Down
Binary file modified creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz
View file
Binary file not shown.
78 changes: 78 additions & 0 deletions creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,22 +8,80 @@
<prover id="4" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="coma" proved="true">
<path name=".."/><path name="list_reversal_lasso.coma"/>
<theory name="Core_Ptr_NonNull_NonNull_Type" proved="true">
<goal name="vc_t_nonnull" proved="true">
<proof prover="4"><result status="valid" time="0.012429" steps="27"/></proof>
</goal>
</theory>
<theory name="Core_Marker_PhantomData_Type" proved="true">
<goal name="vc_t_phantomdata" proved="true">
<proof prover="4"><result status="valid" time="0.016298" steps="27"/></proof>
</goal>
</theory>
<theory name="Core_Ptr_Unique_Unique_Type" proved="true">
<goal name="vc_t_unique" proved="true">
<proof prover="4"><result status="valid" time="0.015518" steps="27"/></proof>
</goal>
</theory>
<theory name="Alloc_RawVec_Cap_Type" proved="true">
<goal name="vc_t_cap" proved="true">
<proof prover="4"><result status="valid" time="0.007652" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_RawVec_RawVec_Type" proved="true">
<goal name="vc_t_rawvec" proved="true">
<proof prover="4"><result status="valid" time="0.009702" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_Vec_Vec_Type" proved="true">
<goal name="vc_t_vec" proved="true">
<proof prover="4"><result status="valid" time="0.005059" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_Alloc_Global_Type" proved="true">
<goal name="vc_t_global" proved="true">
<proof prover="4"><result status="valid" time="0.004024" steps="27"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Memory_Type" proved="true">
<goal name="vc_t_memory" proved="true">
<proof prover="4"><result status="valid" time="0.006687" steps="189"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl1_Index" proved="true">
<goal name="vc_index&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.007485" steps="4967"/></proof>
</goal>
<goal name="vc_index" proved="true">
<proof prover="4"><result status="valid" time="0.046154" steps="9439"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl2_IndexMut" proved="true">
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.011546" steps="5210"/></proof>
</goal>
<goal name="vc_index_mut" proved="true">
<proof prover="4"><result status="valid" time="0.041927" steps="13978"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalSafe" proved="true">
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.015298" steps="4924"/></proof>
</goal>
<goal name="vc_index&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.007217" steps="4924"/></proof>
</goal>
<goal name="vc_list_reversal_safe" proved="true">
<proof prover="4"><result status="valid" time="0.101834" steps="26672"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalList" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.008005" steps="5187"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.007850" steps="5187"/></proof>
</goal>
<goal name="vc_list_reversal_list" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_list.0" expl="loop invariant" proved="true">
Expand Down Expand Up @@ -72,6 +130,12 @@
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalLoop" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.011949" steps="5187"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.016232" steps="5187"/></proof>
</goal>
<goal name="vc_list_reversal_loop" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_loop.0" expl="loop invariant" proved="true">
Expand Down Expand Up @@ -173,6 +237,12 @@
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalLasso" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.012186" steps="5187"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="4"><result status="valid" time="0.015363" steps="5187"/></proof>
</goal>
<goal name="vc_list_reversal_lasso" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.0" expl="loop invariant" proved="true">
Expand Down Expand Up @@ -415,6 +485,14 @@
</transf>
</goal>
</theory>
<theory name="Core_Option_Option_Type" proved="true">
<goal name="vc_none" proved="true">
<proof prover="4"><result status="valid" time="0.004505" steps="27"/></proof>
</goal>
<goal name="vc_some" proved="true">
<proof prover="4"><result status="valid" time="0.000001" steps="27"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_FindPtrInSeq_Impl" proved="true">
<goal name="vc_find_ptr_in_seq" proved="true">
<proof prover="4"><result status="valid" time="0.042008" steps="8450"/></proof>
Expand Down
Binary file modified creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz
View file
Binary file not shown.

0 comments on commit 09a5e44

Please sign in to comment.