Skip to content

Commit 5255706

Browse files
mgrojomgrojo
committed
Avoid proof error related to Global (2)
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 bab4b23 commit 5255706

17 files changed

Lines changed: 939 additions & 932 deletions

File tree

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -376,10 +376,10 @@
376376
<proof prover="2"><result status="valid" steps="189770"/></proof>
377377
<proof prover="4"><result status="highfailure"/></proof>
378378
</goal>
379-
<goal name="def&#39;vc.76">
379+
<goal name="def&#39;vc.74">
380380
<proof prover="3"><result status="valid" steps="1"/></proof>
381381
</goal>
382-
<goal name="def&#39;vc.74">
382+
<goal name="def&#39;vc.76">
383383
<proof prover="3"><result status="valid" steps="1"/></proof>
384384
</goal>
385385
<goal name="def&#39;vc.72">

‎client/proof/sessions/5b8a2d25f6fa8e7838ed-__coap_client__session__fsm__tick/why3session.xml‎

Lines changed: 37 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@
2020
<proof prover="3"><result status="valid" steps="1"/></proof>
2121
</goal>
2222
<goal name="def&#39;vc.2" proved="true">
23-
<proof prover="0"><result status="highfailure"/></proof>
23+
<proof prover="0"><result status="valid" steps="3841"/></proof>
2424
<proof prover="1"><result status="valid" steps="31346"/></proof>
2525
<proof prover="2"><result status="valid" steps="128461"/></proof>
2626
<proof prover="4"><result status="highfailure"/></proof>
@@ -29,25 +29,25 @@
2929
<proof prover="0"><result status="highfailure"/></proof>
3030
<proof prover="1"><result status="highfailure"/></proof>
3131
<proof prover="2"><result status="valid" steps="128365"/></proof>
32-
<proof prover="4"><result status="highfailure"/></proof>
32+
<proof prover="4"><result status="failure" steps="0"/></proof>
3333
</goal>
3434
<goal name="def&#39;vc.4" proved="true">
35-
<proof prover="0"><result status="highfailure"/></proof>
35+
<proof prover="0"><result status="valid" steps="3845"/></proof>
3636
<proof prover="1"><result status="valid" steps="31433"/></proof>
3737
<proof prover="2"><result status="valid" steps="131609"/></proof>
3838
<proof prover="4"><result status="highfailure"/></proof>
3939
</goal>
4040
<goal name="def&#39;vc.5" proved="true">
41-
<proof prover="0"><result status="highfailure"/></proof>
41+
<proof prover="0"><result status="failure" steps="0"/></proof>
4242
<proof prover="1"><result status="highfailure"/></proof>
4343
<proof prover="2"><result status="valid" steps="131513"/></proof>
44-
<proof prover="4"><result status="highfailure"/></proof>
44+
<proof prover="4"><result status="failure" steps="0"/></proof>
4545
</goal>
4646
<goal name="def&#39;vc.6" proved="true">
47-
<proof prover="0"><result status="failure" steps="0"/></proof>
48-
<proof prover="1"><result status="failure" steps="0"/></proof>
47+
<proof prover="0"><result status="valid" steps="3852"/></proof>
48+
<proof prover="1"><result status="valid" steps="31524"/></proof>
4949
<proof prover="2"><result status="valid" steps="131672"/></proof>
50-
<proof prover="4"><result status="failure" steps="0"/></proof>
50+
<proof prover="4"><result status="highfailure"/></proof>
5151
</goal>
5252
<goal name="def&#39;vc.7" proved="true">
5353
<proof prover="0"><result status="highfailure"/></proof>
@@ -56,74 +56,74 @@
5656
<proof prover="4"><result status="failure" steps="0"/></proof>
5757
</goal>
5858
<goal name="def&#39;vc.8" proved="true">
59-
<proof prover="0"><result status="highfailure"/></proof>
59+
<proof prover="0"><result status="valid" steps="3858"/></proof>
6060
<proof prover="1"><result status="valid" steps="31619"/></proof>
6161
<proof prover="2"><result status="valid" steps="131735"/></proof>
6262
<proof prover="4"><result status="highfailure"/></proof>
6363
</goal>
6464
<goal name="def&#39;vc.9" proved="true">
65-
<proof prover="0"><result status="highfailure"/></proof>
65+
<proof prover="0"><result status="failure" steps="0"/></proof>
6666
<proof prover="1"><result status="highfailure"/></proof>
6767
<proof prover="2"><result status="valid" steps="131639"/></proof>
6868
<proof prover="4"><result status="failure" steps="0"/></proof>
6969
</goal>
7070
<goal name="def&#39;vc.10" proved="true">
71-
<proof prover="0"><result status="highfailure"/></proof>
71+
<proof prover="0"><result status="valid" steps="3863"/></proof>
7272
<proof prover="1"><result status="valid" steps="31718"/></proof>
7373
<proof prover="2"><result status="valid" steps="131798"/></proof>
7474
<proof prover="4"><result status="highfailure"/></proof>
7575
</goal>
7676
<goal name="def&#39;vc.11" proved="true">
77-
<proof prover="0"><result status="failure" steps="0"/></proof>
78-
<proof prover="1"><result status="valid" steps="31718"/></proof>
79-
<proof prover="2"><result status="highfailure"/></proof>
77+
<proof prover="0"><result status="highfailure"/></proof>
78+
<proof prover="1"><result status="valid"/></proof>
79+
<proof prover="2"><result status="valid" steps="131702"/></proof>
8080
<proof prover="4"><result status="failure" steps="0"/></proof>
8181
</goal>
8282
<goal name="def&#39;vc.12" proved="true">
83-
<proof prover="0"><result status="highfailure"/></proof>
83+
<proof prover="0"><result status="valid" steps="3870"/></proof>
8484
<proof prover="1"><result status="valid" steps="31821"/></proof>
8585
<proof prover="2"><result status="valid" steps="131861"/></proof>
8686
<proof prover="4"><result status="highfailure"/></proof>
8787
</goal>
8888
<goal name="def&#39;vc.13" proved="true">
89-
<proof prover="0"><result status="highfailure"/></proof>
90-
<proof prover="1"><result status="valid"/></proof>
89+
<proof prover="0"><result status="failure" steps="0"/></proof>
90+
<proof prover="1"><result status="highfailure"/></proof>
9191
<proof prover="2"><result status="valid" steps="131765"/></proof>
92-
<proof prover="4"><result status="highfailure"/></proof>
92+
<proof prover="4"><result status="failure" steps="0"/></proof>
9393
</goal>
9494
<goal name="def&#39;vc.14" proved="true">
95-
<proof prover="0"><result status="failure" steps="0"/></proof>
96-
<proof prover="1"><result status="failure" steps="0"/></proof>
95+
<proof prover="0"><result status="valid" steps="3874"/></proof>
96+
<proof prover="1"><result status="valid" steps="31928"/></proof>
9797
<proof prover="2"><result status="valid" steps="131924"/></proof>
98-
<proof prover="4"><result status="failure" steps="0"/></proof>
98+
<proof prover="4"><result status="highfailure"/></proof>
9999
</goal>
100100
<goal name="def&#39;vc.15" proved="true">
101-
<proof prover="0"><result status="failure" steps="0"/></proof>
102-
<proof prover="1"><result status="failure" steps="0"/></proof>
101+
<proof prover="0"><result status="highfailure"/></proof>
102+
<proof prover="1"><result status="valid" steps="31928"/></proof>
103103
<proof prover="2"><result status="valid" steps="131828"/></proof>
104-
<proof prover="4"><result status="failure" steps="0"/></proof>
104+
<proof prover="4"><result status="highfailure"/></proof>
105105
</goal>
106106
<goal name="def&#39;vc.16" proved="true">
107-
<proof prover="0"><result status="highfailure"/></proof>
107+
<proof prover="0"><result status="valid" steps="3881"/></proof>
108108
<proof prover="1"><result status="valid" steps="32039"/></proof>
109109
<proof prover="2"><result status="valid" steps="131987"/></proof>
110110
<proof prover="4"><result status="highfailure"/></proof>
111111
</goal>
112112
<goal name="def&#39;vc.17" proved="true">
113-
<proof prover="0"><result status="highfailure"/></proof>
114-
<proof prover="1"><result status="valid" steps="32039"/></proof>
113+
<proof prover="0"><result status="failure" steps="0"/></proof>
114+
<proof prover="1"><result status="highfailure"/></proof>
115115
<proof prover="2"><result status="valid" steps="131891"/></proof>
116-
<proof prover="4"><result status="highfailure"/></proof>
116+
<proof prover="4"><result status="failure" steps="0"/></proof>
117117
</goal>
118118
<goal name="def&#39;vc.18" proved="true">
119-
<proof prover="0"><result status="failure" steps="0"/></proof>
120-
<proof prover="1"><result status="valid" steps="55391"/></proof>
121-
<proof prover="2"><result status="highfailure"/></proof>
122-
<proof prover="4"><result status="failure" steps="0"/></proof>
119+
<proof prover="0"><result status="highfailure"/></proof>
120+
<proof prover="1"><result status="valid" steps="39203"/></proof>
121+
<proof prover="2"><result status="valid" steps="5374045"/></proof>
122+
<proof prover="4"><result status="highfailure"/></proof>
123123
</goal>
124124
<goal name="def&#39;vc.19" proved="true">
125125
<proof prover="0"><result status="highfailure"/></proof>
126-
<proof prover="1"><result status="valid" steps="55391"/></proof>
126+
<proof prover="1"><result status="valid" steps="39203"/></proof>
127127
<proof prover="2"><result status="highfailure"/></proof>
128128
<proof prover="4"><result status="highfailure"/></proof>
129129
</goal>
@@ -134,14 +134,14 @@
134134
<proof prover="3"><result status="valid" steps="1"/></proof>
135135
</goal>
136136
<goal name="def&#39;vc.22" proved="true">
137-
<proof prover="0"><result status="highfailure"/></proof>
138-
<proof prover="1"><result status="valid" steps="56259"/></proof>
139-
<proof prover="2"><result status="highfailure"/></proof>
137+
<proof prover="0"><result status="valid" steps="3821"/></proof>
138+
<proof prover="1"><result status="valid" steps="40027"/></proof>
139+
<proof prover="2"><result status="valid" steps="5400795"/></proof>
140140
<proof prover="4"><result status="highfailure"/></proof>
141141
</goal>
142142
<goal name="def&#39;vc.23" proved="true">
143143
<proof prover="0"><result status="highfailure"/></proof>
144-
<proof prover="1"><result status="valid" steps="56259"/></proof>
144+
<proof prover="1"><result status="valid" steps="40027"/></proof>
145145
<proof prover="2"><result status="highfailure"/></proof>
146146
<proof prover="4"><result status="highfailure"/></proof>
147147
</goal>

0 commit comments

Comments
 (0)