Skip to content

Commit bab4b23

Browse files
mgrojomgrojo
committed
Avoid proof error related to Global
Original error was: ``` medium: "memory accessed through objects of access type" might not be initialized after elaboration of main program "CoAP_Client" ``` See ticket CS0041304 #4830.
1 parent 57d8cba commit bab4b23

652 files changed

Lines changed: 66988 additions & 16912 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎client/proof/sessions/007fec219a1bef9962b3-erver__main_loop__fsm__initialize/why3session.xml‎

Lines changed: 395 additions & 0 deletions
Large diffs are not rendered by default.

‎client/proof/sessions/01de463bf74ee5b8bcca-eq_elements_checks__eq_transitive/why3session.xml‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@
33
"http://why3.lri.fr/why3session.dtd">
44
<why3session shape_version="6">
55
<prover id="0" name="altergo" version="1.30-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
6-
<prover id="1" name="CVC5" version="0.0.7-gnatprove" timelimit="0" steplimit="0" memlimit="0"/>
6+
<prover id="1" name="CVC5" version="0.0.7-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
77
<prover id="2" name="Z3" version="4.5.1-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
88
<prover id="3" name="Trivial" version="1.0" alternative="trivial" timelimit="1" steplimit="1" memlimit="1000"/>
9+
<prover id="4" name="colibri" version="2137" timelimit="180" steplimit="0" memlimit="2000"/>
910
<file format="gnat-json" proved="true">
1011
<path name=".."/><path name=".."/><path name=".."/><path name=".."/><path name="obj"/>
1112
<path name="release"/><path name="gnatprove"/><path name="01de463bf74ee5b8bcca-eq_elements_checks__eq_transitive.gnat-json"/>
@@ -16,22 +17,25 @@
1617
<proof prover="3"><result status="valid" steps="1"/></proof>
1718
</goal>
1819
<goal name="def&#39;vc.1" proved="true">
19-
<proof prover="0"><result status="highfailure"/></proof>
20-
<proof prover="1" steplimit="9980"><result status="valid" steps="9072"/></proof>
20+
<proof prover="0"><result status="valid" steps="441"/></proof>
21+
<proof prover="1"><result status="valid" steps="9072"/></proof>
2122
<proof prover="2"><result status="valid" steps="6041"/></proof>
23+
<proof prover="4"><result status="highfailure"/></proof>
2224
</goal>
2325
<goal name="def&#39;vc.2" proved="true">
2426
<proof prover="0"><result status="highfailure"/></proof>
25-
<proof prover="1"><result status="valid" steps="9072"/></proof>
27+
<proof prover="1"><result status="highfailure"/></proof>
2628
<proof prover="2"><result status="valid" steps="6166"/></proof>
29+
<proof prover="4"><result status="highfailure"/></proof>
2730
</goal>
2831
<goal name="def&#39;vc.3" proved="true">
2932
<proof prover="3"><result status="valid" steps="1"/></proof>
3033
</goal>
3134
<goal name="def&#39;vc.4" proved="true">
32-
<proof prover="0" timelimit="0" steplimit="480" memlimit="0"><result status="valid" steps="436"/></proof>
33-
<proof prover="1" timelimit="180" memlimit="2000"><result status="valid" steps="7135"/></proof>
35+
<proof prover="0"><result status="valid" steps="436"/></proof>
36+
<proof prover="1"><result status="valid" steps="7135"/></proof>
3437
<proof prover="2"><result status="valid" steps="6572"/></proof>
38+
<proof prover="4"><result status="highfailure"/></proof>
3539
</goal>
3640
</transf>
3741
</goal>

‎client/proof/sessions/02f728d06b3bbd8f0f30-ap_message__get_client_error_code/why3session.xml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,9 @@
44
<why3session shape_version="6">
55
<prover id="0" name="altergo" version="1.30-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
66
<prover id="1" name="CVC5" version="0.0.7-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
7-
<prover id="2" name="Z3" version="4.5.1-gnatprove" timelimit="0" steplimit="142119" memlimit="0"/>
7+
<prover id="2" name="Z3" version="4.5.1-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
88
<prover id="3" name="Trivial" version="1.0" alternative="trivial" timelimit="1" steplimit="1" memlimit="1000"/>
9+
<prover id="4" name="colibri" version="2137" timelimit="180" steplimit="0" memlimit="2000"/>
910
<file format="gnat-json" proved="true">
1011
<path name=".."/><path name=".."/><path name=".."/><path name=".."/><path name="obj"/>
1112
<path name="release"/><path name="gnatprove"/><path name="02f728d06b3bbd8f0f30-ap_message__get_client_error_code.gnat-json"/>
@@ -20,8 +21,9 @@
2021
</goal>
2122
<goal name="def&#39;vc.2" proved="true">
2223
<proof prover="0"><result status="highfailure"/></proof>
23-
<proof prover="1"><result status="highfailure"/></proof>
24+
<proof prover="1"><result status="valid"/></proof>
2425
<proof prover="2"><result status="valid" steps="129199"/></proof>
26+
<proof prover="4"><result status="failure" steps="0"/></proof>
2527
</goal>
2628
</transf>
2729
</goal>

‎client/proof/sessions/0372b825e1293f8b3340-en_data__sufficient_buffer_length/why3session.xml‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@
33
"http://why3.lri.fr/why3session.dtd">
44
<why3session shape_version="6">
55
<prover id="0" name="altergo" version="1.30-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
6-
<prover id="1" name="CVC5" version="0.0.7-gnatprove" timelimit="0" steplimit="19695" memlimit="0"/>
6+
<prover id="1" name="CVC5" version="0.0.7-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
77
<prover id="2" name="Z3" version="4.5.1-gnatprove" timelimit="180" steplimit="0" memlimit="2000"/>
88
<prover id="3" name="Trivial" version="1.0" alternative="trivial" timelimit="1" steplimit="1" memlimit="1000"/>
9+
<prover id="4" name="colibri" version="2137" timelimit="180" steplimit="0" memlimit="2000"/>
910
<file format="gnat-json" proved="true">
1011
<path name=".."/><path name=".."/><path name=".."/><path name=".."/><path name="obj"/>
1112
<path name="release"/><path name="gnatprove"/><path name="0372b825e1293f8b3340-en_data__sufficient_buffer_length.gnat-json"/>
@@ -19,14 +20,16 @@
1920
<proof prover="3"><result status="valid" steps="1"/></proof>
2021
</goal>
2122
<goal name="def&#39;vc.2" proved="true">
22-
<proof prover="0"><result status="failure" steps="0"/></proof>
23+
<proof prover="0"><result status="highfailure"/></proof>
2324
<proof prover="1"><result status="valid" steps="17904"/></proof>
2425
<proof prover="2"><result status="valid" steps="64250"/></proof>
26+
<proof prover="4"><result status="highfailure"/></proof>
2527
</goal>
2628
<goal name="def&#39;vc.3" proved="true">
2729
<proof prover="0"><result status="failure" steps="0"/></proof>
28-
<proof prover="1" steplimit="9781"><result status="valid" steps="8891"/></proof>
30+
<proof prover="1"><result status="valid"/></proof>
2931
<proof prover="2"><result status="valid" steps="37372"/></proof>
32+
<proof prover="4"><result status="failure" steps="0"/></proof>
3033
</goal>
3134
</transf>
3235
</goal>

0 commit comments

Comments
 (0)