ada/SPARKlib
0
0
Fork 0
mirror of https://github.com/AdaCore/SPARKlib.git synced 2026-02-12 13:11:36 -08:00
Code Issues Packages Projects Releases Wiki Activity

Update session test

Browse Source
This commit is contained in:
Claire Dross
2025-11-17 17:09:30 +01:00
parent 6ae1d02777
commit cbaf645e05
31 changed files with 1964 additions and 1955 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
tests/63__c_strings_proof/proof/sessions/c_constant_strings__chars_ptr/why3session.xml
View File

@@ -16,8 +16,8 @@
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2297"/></proof>
<proof prover="2"><result status="valid" steps="1556"/></proof>
<proof prover="4"><result status="valid" steps="122"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>

6
tests/63__c_strings_proof/proof/sessions/c_constant_strings__chars_ptrPredicate/why3session.xml
View File

@@ -14,10 +14,10 @@
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="18"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1518"/></proof>
<proof prover="2"><result status="valid" steps="1184"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="203"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>

34
tests/63__c_strings_proof/proof/sessions/c_constant_strings__find_nul/why3session.xml
View File

@@ -20,16 +20,16 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1150"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="35"/></proof>
<proof prover="1"><result status="valid" steps="13032"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -41,24 +41,24 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1317"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="247"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="21671"/></proof>
<proof prover="0"><result status="valid" steps="139"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="valid" steps="236"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="17382"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
@@ -68,10 +68,10 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2021"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>

12
tests/63__c_strings_proof/proof/sessions/c_constant_strings__is_null/why3session.xml
View File

@@ -17,16 +17,16 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2784"/></proof>
<proof prover="2"><result status="valid" steps="2484"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="575"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2790"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="571"/></proof>
</goal>
</transf>
</goal>

12
tests/63__c_strings_proof/proof/sessions/c_constant_strings__strlen/why3session.xml
View File

@@ -23,16 +23,16 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1718"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="valid" steps="24"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1677"/></proof>
<proof prover="2"><result status="valid" steps="1556"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>
</goal>

62
tests/63__c_strings_proof/proof/sessions/c_constant_strings__to_chars_ptr__3/why3session.xml
View File

@@ -17,7 +17,7 @@
<proof prover="0"><result status="valid" steps="22"/></proof>
<proof prover="1"><result status="valid" steps="1758"/></proof>
<proof prover="2"><result status="valid" steps="1489"/></proof>
<proof prover="4"><result status="valid" steps="406"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -26,37 +26,37 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1741"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2990"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="26"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2007"/></proof>
<proof prover="2"><result status="valid" steps="1748"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1992"/></proof>
<proof prover="2"><result status="valid" steps="1744"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3498"/></proof>
<proof prover="2"><result status="valid" steps="2471"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
@@ -65,13 +65,13 @@
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="1"><result status="valid" steps="4177"/></proof>
<proof prover="2"><result status="valid" steps="3684"/></proof>
<proof prover="4"><result status="valid" steps="1198"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2932"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="valid" steps="59"/></proof>
@@ -89,25 +89,25 @@
<proof prover="0"><result status="valid" steps="1377"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4427"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.16" proved="true">
<proof prover="0"><result status="valid" steps="42"/></proof>
<proof prover="1"><result status="valid" steps="5322"/></proof>
<proof prover="2"><result status="valid" steps="5906"/></proof>
<proof prover="4"><result status="valid" steps="1518"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.17" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="28004"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="42"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="15281"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -116,10 +116,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.20" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3035"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.21" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
@@ -128,10 +128,10 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.22" proved="true">
<proof prover="0"><result status="valid" steps="858"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="166570"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.23" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>

50
tests/63__c_strings_proof/proof/sessions/c_constant_strings__value/why3session.xml
View File

@@ -25,32 +25,32 @@
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4232"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4600"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="valid" steps="177"/></proof>
<proof prover="1"><result status="valid" steps="3501"/></proof>
<proof prover="2"><result status="valid" steps="5308"/></proof>
<proof prover="4"><result status="valid" steps="947"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid"/></proof>
<proof prover="2"><result status="valid" steps="9969"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="11951"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="valid" steps="13"/></proof>
<proof prover="1"><result status="valid" steps="4957"/></proof>
<proof prover="2"><result status="valid" steps="4353"/></proof>
<proof prover="4"><result status="valid" steps="1200"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="42"/></proof>
@@ -59,16 +59,16 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3944"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="18408"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="11306"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -77,22 +77,22 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7373"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7683"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="75471"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="1024"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="0"><result status="valid" steps="5694"/></proof>

56
tests/63__c_strings_proof/proof/sessions/c_constant_strings__value__2/why3session.xml
View File

@@ -20,37 +20,37 @@
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="1"><result status="valid" steps="1691"/></proof>
<proof prover="2"><result status="valid" steps="1540"/></proof>
<proof prover="4"><result status="valid" steps="543"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3230"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2707"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3233"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="10246"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="10173"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5204"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="930"/></proof>
@@ -62,36 +62,36 @@
<proof prover="0"><result status="valid" steps="14"/></proof>
<proof prover="1"><result status="valid" steps="2560"/></proof>
<proof prover="2"><result status="valid" steps="3900"/></proof>
<proof prover="4"><result status="valid" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="valid" steps="63"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5735"/></proof>
<proof prover="2"><result status="valid" steps="6261"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="1456"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="0"><result status="valid" steps="63"/></proof>
<proof prover="1"><result status="valid" steps="4716"/></proof>
<proof prover="2"><result status="valid" steps="6270"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="31734"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="valid" steps="63"/></proof>
<proof prover="1"><result status="valid" steps="28990"/></proof>
<proof prover="2"><result status="valid" steps="9140"/></proof>
<proof prover="4"><result status="valid" steps="1533"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="0"><result status="valid" steps="1059"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="13687"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
@@ -103,20 +103,20 @@
<goal name="def&#39;vc.16" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="13452"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="27150"/></proof>
<proof prover="4"><result status="unknown" steps="1274"/></proof>
</goal>
<goal name="def&#39;vc.17" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="18151"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="0"><result status="valid" steps="1334"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="202511"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>
</goal>

132
tests/63__c_strings_proof/proof/sessions/c_constant_strings__value__3/why3session.xml
View File

@@ -16,8 +16,8 @@
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="1"><result status="valid" steps="1360"/></proof>
<proof prover="2"><result status="valid" steps="1806"/></proof>
<proof prover="4"><result status="valid" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -29,22 +29,22 @@
<proof prover="4"><result status="valid" steps="546"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="valid" steps="403"/></proof>
<proof prover="1"><result status="valid" steps="42732"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="38146"/></proof>
<proof prover="4"><result status="unknown" steps="838"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="62209"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="49781"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1801"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="valid" steps="58"/></proof>
@@ -53,28 +53,28 @@
<proof prover="4"><result status="valid" steps="1177"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7954"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7967"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="valid" steps="111"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="8166"/></proof>
<proof prover="2"><result status="valid" steps="35952"/></proof>
<proof prover="4"><result status="valid" steps="1245"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="6135"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="valid" steps="1698"/></proof>
@@ -86,16 +86,16 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="valid" steps="58"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5075"/></proof>
<proof prover="2"><result status="valid" steps="6419"/></proof>
<proof prover="4"><result status="valid" steps="1290"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5411"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -107,55 +107,55 @@
<proof prover="0"><result status="valid" steps="6973"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="unknown" steps="2119"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
<proof prover="0"><result status="valid" steps="21"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7490"/></proof>
<proof prover="2"><result status="valid" steps="6386"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.19" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="9551"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.20" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.21" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4824"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.22" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4824"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.23" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.24" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="9165"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.25" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="9591"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.26" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="9601"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.27" proved="true">
<proof prover="0"><result status="valid" steps="144"/></proof>
@@ -164,31 +164,31 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.28" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="7257"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="7340"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.29" proved="true">
<proof prover="0"><result status="valid" steps="257"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.30" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.31" proved="true">
<proof prover="0"><result status="valid" steps="72"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5278"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="5142"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.32" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5270"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.33" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -197,10 +197,10 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.35" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="25727"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="38577"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.36" proved="true">
<proof prover="0"><result status="valid" steps="1836"/></proof>
@@ -216,9 +216,9 @@
</goal>
<goal name="def&#39;vc.38" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="36898"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="unknown" steps="2272"/></proof>
<proof prover="1"><result status="valid"/></proof>
<proof prover="2"><result status="valid" steps="88070"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>
</goal>

402
tests/63__c_strings_proof/proof/sessions/c_constant_strings__value__4/why3session.xml
View File

File diff suppressed because it is too large Load Diff

50
tests/63__c_strings_proof/proof/sessions/c_constant_strings__value_def/why3session.xml
View File

@@ -17,52 +17,52 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2115"/></proof>
<proof prover="2"><result status="valid" steps="2350"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="valid" steps="28"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1914"/></proof>
<proof prover="2"><result status="valid" steps="1634"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1918"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2115"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1914"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1934"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2115"/></proof>
<proof prover="2"><result status="valid" steps="2350"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -70,26 +70,26 @@
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="valid" steps="30"/></proof>
<proof prover="1"><result status="valid" steps="3308"/></proof>
<proof prover="2"><result status="valid" steps="4160"/></proof>
<proof prover="4"><result status="valid" steps="512"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="valid" steps="30"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3308"/></proof>
<proof prover="2"><result status="valid" steps="4160"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="valid" steps="3055"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="3204567"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="0"><result status="valid" steps="5702"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="unknown" steps="832"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>

40
tests/63__c_strings_proof/proof/sessions/c_strings__c_length_ghost/why3session.xml
View File

@@ -20,16 +20,16 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1150"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="13032"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="35"/></proof>
<proof prover="1"><result status="valid"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -41,25 +41,25 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1317"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="139"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="valid" steps="412042"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="valid" steps="236"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="17382"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="0"><result status="valid" steps="160"/></proof>
@@ -68,10 +68,10 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2095"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -83,10 +83,10 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="0"><result status="valid" steps="5"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="655"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>
</goal>

132
tests/63__c_strings_proof/proof/sessions/c_strings__c_length_ghost__2/why3session.xml
View File

@@ -23,90 +23,90 @@
<proof prover="0"><result status="valid" steps="6"/></proof>
<proof prover="1"><result status="valid" steps="1573"/></proof>
<proof prover="2"><result status="valid" steps="2723"/></proof>
<proof prover="4"><result status="valid" steps="258"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="valid" steps="6"/></proof>
<proof prover="1"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1578"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="valid" steps="7"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1554"/></proof>
<proof prover="2"><result status="valid" steps="2806"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1442"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1426"/></proof>
<proof prover="2"><result status="valid" steps="1130"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2014"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="valid" steps="15"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1980"/></proof>
<proof prover="2"><result status="valid" steps="8892"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2361"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2376"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2453"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.13" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1632"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.14" proved="true">
<proof prover="0"><result status="valid" steps="29"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1620"/></proof>
<proof prover="2"><result status="valid" steps="1353"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.15" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2660"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.16" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.17" proved="true">
<proof prover="0"><result status="valid" steps="39"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4116"/></proof>
<proof prover="2"><result status="valid" steps="11354"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.18" proved="true">
@@ -116,16 +116,16 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.19" proved="true">
<proof prover="0"><result status="valid" steps="9"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2825"/></proof>
<proof prover="2"><result status="valid" steps="16761"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.20" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2851"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.21" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -133,50 +133,50 @@
<goal name="def&#39;vc.22" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3348"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.23" proved="true">
<proof prover="0"><result status="valid" steps="157"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3341"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.24" proved="true">
<proof prover="0"><result status="valid" steps="58"/></proof>
<proof prover="1"><result status="valid" steps="3380"/></proof>
<proof prover="2"><result status="valid" steps="18712"/></proof>
<proof prover="4"><result status="valid" steps="1032"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.25" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2706"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.26" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2908"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.27" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2908"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.28" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2841"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.29" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2841"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.30" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -184,14 +184,14 @@
<goal name="def&#39;vc.31" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2863"/></proof>
<proof prover="2"><result status="valid" steps="2414"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.32" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4071"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.33" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -206,16 +206,16 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.36" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4706"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.37" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="5237"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.38" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>

6
tests/63__c_strings_proof/proof/sessions/c_strings__chars_ptr/why3session.xml
View File

@@ -16,8 +16,8 @@
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2082"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -34,7 +34,7 @@
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="4904"/></proof>
<proof prover="2"><result status="valid" steps="5462"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">

28
tests/63__c_strings_proof/proof/sessions/c_strings__chars_ptrPredicate/why3session.xml
View File

@@ -15,32 +15,32 @@
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1301"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="3"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="3"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1311"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="3"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="valid" steps="19"/></proof>
<proof prover="1"><result status="valid" steps="1311"/></proof>
<proof prover="2"><result status="valid" steps="922"/></proof>
<proof prover="3"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1311"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="3"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1309"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="3"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="3"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1156"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="3"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="3"><result status="valid" steps="245"/></proof>
</goal>
</transf>
</goal>

40
tests/63__c_strings_proof/proof/sessions/c_strings__find_nul/why3session.xml
View File

@@ -20,32 +20,32 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1150"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="valid" steps="35"/></proof>
<proof prover="1"><result status="valid" steps="13032"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="valid" steps="81"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="9579"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="1317"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1317"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="139"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
@@ -56,22 +56,22 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="17382"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="11663"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2021"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>

27
tests/63__c_strings_proof/proof/sessions/c_strings__free/why3session.xml
View File

@@ -14,27 +14,36 @@
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="46"/></proof>
<proof prover="1"><result status="valid" steps="4224"/></proof>
<proof prover="2"><result status="valid" steps="1273"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1351"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="1"><result status="valid" steps="2191"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="valid" steps="46"/></proof>
<proof prover="1"><result status="valid" steps="4224"/></proof>
<proof prover="2"><result status="valid" steps="1273"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="valid" steps="20"/></proof>
<proof prover="1"><result status="valid" steps="2191"/></proof>
<proof prover="2"><result status="valid" steps="1826"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3377"/></proof>
<proof prover="2"><result status="valid" steps="3063"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>

30
tests/63__c_strings_proof/proof/sessions/c_strings__is_nul_terminated_ghost/why3session.xml
View File

@@ -14,15 +14,15 @@
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="valid" steps="11"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1013"/></proof>
<proof prover="2"><result status="valid" steps="782"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="valid" steps="11"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1558"/></proof>
<proof prover="2"><result status="valid" steps="4569"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
@@ -35,24 +35,24 @@
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1207"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.5" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2204"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.6" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="36"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2696"/></proof>
<proof prover="2"><result status="valid" steps="7350"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
@@ -67,13 +67,13 @@
<goal name="def&#39;vc.11" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3314"/></proof>
<proof prover="2"><result status="valid" steps="9067"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.12" proved="true">
<proof prover="0"><result status="valid" steps="47"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="3211"/></proof>
<proof prover="2"><result status="valid" steps="8688"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>

12
tests/63__c_strings_proof/proof/sessions/c_strings__is_null/why3session.xml
View File

@@ -17,16 +17,16 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2609"/></proof>
<proof prover="2"><result status="valid" steps="2063"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="valid" steps="694"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="valid" steps="12"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="2603"/></proof>
<proof prover="2"><result status="valid" steps="2313"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>
</goal>

38
tests/63__c_strings_proof/proof/sessions/c_strings__lemma_is_find_nul/why3session.xml
View File

@@ -14,28 +14,28 @@
<goal name="def&#39;vc" proved="true">
<transf name="split_goal_wp_conj" proved="true" >
<goal name="def&#39;vc.0" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="0"><result status="valid" steps="7"/></proof>
<proof prover="1"><result status="valid" steps="1007"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="395"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.1" proved="true">
<proof prover="0"><result status="failure" steps="0"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1007"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.2" proved="true">
<proof prover="0"><result status="valid" steps="16"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1032"/></proof>
<proof prover="2"><result status="valid" steps="619"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.3" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="15020"/></proof>
<proof prover="0"><result status="valid" steps="35"/></proof>
<proof prover="1"><result status="highfailure"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.4" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
@@ -47,25 +47,25 @@
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.7" proved="true">
<proof prover="0"><result status="valid" steps="9"/></proof>
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="1414"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="708"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.8" proved="true">
<proof prover="3"><result status="valid" steps="1"/></proof>
</goal>
<goal name="def&#39;vc.9" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="0"><result status="valid" steps="51"/></proof>
<proof prover="1"><result status="valid" steps="8110"/></proof>
<proof prover="2"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="2"><result status="valid" steps="4421"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
<goal name="def&#39;vc.10" proved="true">
<proof prover="0"><result status="highfailure"/></proof>
<proof prover="1"><result status="valid" steps="41697"/></proof>
<proof prover="2"><result status="highfailure"/></proof>
<proof prover="4"><result status="failure" steps="0"/></proof>
<proof prover="4"><result status="highfailure"/></proof>
</goal>
</transf>
</goal>

Some files were not shown because too many files have changed in this diff Show More