sessions: update

Signed-off-by: Denis Efremov <[email protected]>
evdenis · Oct 7, 2020 · 120a130 · 120a130
1 parent 440fee7
commit 120a130
Show file tree

Hide file tree

Showing 30 changed files with 1,878 additions and 1,725 deletions.
diff --git a/sessions/_parse_integer_fixup_radix.av/whole_program/why3session.xml b/sessions/_parse_integer_fixup_radix.av/whole_program/why3session.xml
@@ -949,29 +949,29 @@
 </theory>
 <theory name="Function__parse_integer_fixup_radix_safety" sum="e1ecc0d015449beaa4c58a6c495172b7" expanded="true">
  <goal name="WP_parameter _parse_integer_fixup_radix" expl="Function _parse_integer_fixup_radix, safety" expanded="true">
- <proof prover="1"><result status="valid" time="0.09"/></proof>
+ <proof prover="1"><result status="valid" time="0.10"/></proof>
  </goal>
 </theory>
 <theory name="Function__parse_integer_fixup_radix_behaviors" sum="ccccd7245da959158eb64de49ad1b74b" expanded="true">
  <goal name="WP_parameter _parse_integer_fixup_radix_ensures_default" expl="Function _parse_integer_fixup_radix, default behavior" expanded="true">
- <proof prover="1"><result status="valid" time="0.14"/></proof>
+ <proof prover="1"><result status="valid" time="0.18"/></proof>
  </goal>
  <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess" expl="Function _parse_integer_fixup_radix, behavior guess" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.1" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.19" steps="1443"/></proof>
+  <proof prover="0"><result status="valid" time="0.21" steps="1443"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.2" expl="Postcondition (Ensures clause)">
   <proof prover="0"><result status="valid" time="0.03" steps="141"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.3" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.03" steps="129"/></proof>
+  <proof prover="0"><result status="valid" time="0.04" steps="129"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.4" expl="Postcondition (Ensures clause)">
   <proof prover="0"><result status="valid" time="0.03" steps="121"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.5" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.01" steps="108"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="108"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.6" expl="Postcondition (Ensures clause)">
   <proof prover="0"><result status="valid" time="0.02" steps="108"/></proof>
@@ -986,28 +986,28 @@
   <proof prover="0"><result status="valid" time="0.01" steps="100"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.10" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.01" steps="100"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="100"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.11" expl="Postcondition (Ensures clause)">
   <proof prover="0"><result status="valid" time="0.02" steps="100"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.12" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.21" steps="813"/></proof>
+  <proof prover="0"><result status="valid" time="0.23" steps="813"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.13" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.01" steps="88"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="88"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.14" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.01" steps="88"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="88"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.15" expl="Postcondition (Ensures clause)">
   <proof prover="0"><result status="valid" time="0.01" steps="88"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.16" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.22" steps="1675"/></proof>
+  <proof prover="0"><result status="valid" time="0.25" steps="1675"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.17" expl="Postcondition (Ensures clause)">
-  <proof prover="0"><result status="valid" time="0.02" steps="107"/></proof>
+  <proof prover="0"><result status="valid" time="0.03" steps="107"/></proof>
   </goal>
   <goal name="WP_parameter _parse_integer_fixup_radix_ensures_guess.18" expl="Postcondition (Ensures clause)">
   <proof prover="0"><result status="valid" time="0.02" steps="103"/></proof>
@@ -1021,7 +1021,7 @@
  </transf>
  </goal>
  <goal name="WP_parameter _parse_integer_fixup_radix_ensures_shift" expl="Function _parse_integer_fixup_radix, behavior shift" expanded="true">
- <proof prover="1"><result status="valid" time="0.74"/></proof>
+ <proof prover="1"><result status="valid" time="1.12"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/sessions/check_bytes8.av/whole_program/why3session.xml b/sessions/check_bytes8.av/whole_program/why3session.xml
@@ -793,7 +793,7 @@
 </theory>
 <theory name="Function_check_bytes8_0_safety" sum="f214dc0feff67b31e8151b86412f139d" expanded="true">
  <goal name="WP_parameter check_bytes8_0" expl="Function check_bytes8, safety" expanded="true">
- <proof prover="1"><result status="valid" time="0.09"/></proof>
+ <proof prover="1"><result status="valid" time="0.11"/></proof>
  </goal>
 </theory>
 <theory name="Function_check_bytes8_0_behaviors" sum="56f6c92a103ac54a5d98c66f41419a6d" expanded="true">
@@ -806,13 +806,13 @@
   <proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="WP_parameter check_bytes8_ensures_default.3" expl="loop invariant init">
-  <proof prover="0"><result status="valid" time="0.10" steps="783"/></proof>
+  <proof prover="0"><result status="valid" time="0.11" steps="783"/></proof>
   </goal>
   <goal name="WP_parameter check_bytes8_ensures_default.4" expl="Ensures clause (Postcondition)">
   <proof prover="0"><result status="valid" time="0.02" steps="199"/></proof>
   </goal>
   <goal name="WP_parameter check_bytes8_ensures_default.5" expl="loop invariant preservation">
-  <proof prover="0"><result status="valid" time="1.20" steps="1632"/></proof>
+  <proof prover="0"><result status="valid" time="1.28" steps="1632"/></proof>
   </goal>
   <goal name="WP_parameter check_bytes8_ensures_default.6" expl="Assertion in line 23">
   <proof prover="0"><result status="valid" time="0.01" steps="36"/></proof>
@@ -826,10 +826,10 @@
  </transf>
  </goal>
  <goal name="WP_parameter check_bytes8_ensures_found" expl="Function check_bytes8, behavior found" expanded="true">
- <proof prover="1"><result status="valid" time="0.14"/></proof>
+ <proof prover="1"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="WP_parameter check_bytes8_ensures_not_exists" expl="Function check_bytes8, behavior not_exists" expanded="true">
- <proof prover="0"><result status="valid" time="0.02" steps="220"/></proof>
+ <proof prover="0"><result status="valid" time="0.03" steps="220"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/sessions/kstrtobool.av/whole_program/why3session.xml b/sessions/kstrtobool.av/whole_program/why3session.xml
@@ -895,7 +895,7 @@
 </theory>
 <theory name="Function_kstrtobool_safety" sum="1e29c951c5acfdd4394a74fea1cfa2e6" expanded="true">
  <goal name="WP_parameter kstrtobool" expl="Function kstrtobool, safety" expanded="true">
- <proof prover="1"><result status="valid" time="0.07"/></proof>
+ <proof prover="1"><result status="valid" time="0.08"/></proof>
  </goal>
 </theory>
 <theory name="Function_kstrtobool_behaviors" sum="d2894b22a99feb3792f47c6caef638b4" expanded="true">
@@ -905,10 +905,10 @@
   <proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.2" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.03" steps="431"/></proof>
+  <proof prover="0"><result status="valid" time="0.04" steps="431"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.3" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.03" steps="390"/></proof>
+  <proof prover="0"><result status="valid" time="0.04" steps="390"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.4" expl="Postcondition">
   <proof prover="0"><result status="valid" time="0.04" steps="401"/></proof>
@@ -917,51 +917,51 @@
   <proof prover="0"><result status="valid" time="0.05" steps="569"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.6" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.04" steps="436"/></proof>
+  <proof prover="0"><result status="valid" time="0.05" steps="436"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.7" expl="Postcondition">
   <proof prover="0"><result status="valid" time="0.04" steps="455"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.8" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.07" steps="860"/></proof>
+  <proof prover="0"><result status="valid" time="0.08" steps="860"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.9" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.07" steps="758"/></proof>
+  <proof prover="0"><result status="valid" time="0.08" steps="758"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.10" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.07" steps="860"/></proof>
+  <proof prover="0"><result status="valid" time="0.08" steps="860"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.11" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.08" steps="881"/></proof>
+  <proof prover="0"><result status="valid" time="0.09" steps="881"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.12" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.09" steps="876"/></proof>
+  <proof prover="0"><result status="valid" time="0.10" steps="876"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.13" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.07" steps="757"/></proof>
+  <proof prover="0"><result status="valid" time="0.08" steps="757"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.14" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.09" steps="939"/></proof>
+  <proof prover="0"><result status="valid" time="0.10" steps="939"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.15" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.08" steps="881"/></proof>
+  <proof prover="0"><result status="valid" time="0.09" steps="881"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.16" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.07" steps="844"/></proof>
+  <proof prover="0"><result status="valid" time="0.08" steps="844"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.17" expl="Postcondition">
-  <proof prover="0"><result status="valid" time="0.09" steps="889"/></proof>
+  <proof prover="0"><result status="valid" time="0.11" steps="889"/></proof>
   </goal>
   <goal name="WP_parameter kstrtobool_ensures_CORRECT.18" expl="Postcondition">
   <proof prover="0"><result status="valid" time="0.04" steps="457"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="WP_parameter kstrtobool_ensures_INVAL" expl="Function kstrtobool, behavior INVAL" expanded="true">
- <proof prover="1"><result status="valid" time="0.11"/></proof>
+ <proof prover="1"><result status="valid" time="0.13"/></proof>
  </goal>
  <goal name="WP_parameter kstrtobool_ensures_default" expl="Function kstrtobool, default behavior" expanded="true">
- <proof prover="1"><result status="valid" time="0.09"/></proof>
+ <proof prover="1"><result status="valid" time="0.11"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/sessions/match_string.av/whole_program/why3session.xml b/sessions/match_string.av/whole_program/why3session.xml
@@ -849,37 +849,37 @@
 </theory>
 <theory name="Function_match_string_0_safety" sum="1f8cc5c24984d52512517b21ae5a2b91" expanded="true">
  <goal name="WP_parameter match_string_0" expl="Function match_string, safety" expanded="true">
- <proof prover="1"><result status="valid" time="0.16"/></proof>
+ <proof prover="1"><result status="valid" time="0.18"/></proof>
  </goal>
 </theory>
 <theory name="Function_match_string_0_behaviors" sum="2f161d4328733cc19f2abd76a447ae37" expanded="true">
  <goal name="WP_parameter match_string_ensures_default" expl="Function match_string, default behavior" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter match_string_ensures_default.1" expl="Behavior disjointness check">
-  <proof prover="0"><result status="valid" time="0.03" steps="151"/></proof>
+  <proof prover="0"><result status="valid" time="0.04" steps="151"/></proof>
   </goal>
   <goal name="WP_parameter match_string_ensures_default.2" expl="Behavior completeness check">
-  <proof prover="0"><result status="valid" time="0.03" steps="149"/></proof>
+  <proof prover="0"><result status="valid" time="0.04" steps="149"/></proof>
   </goal>
   <goal name="WP_parameter match_string_ensures_default.3" expl="loop invariant init">
-  <proof prover="1"><result status="valid" time="0.21"/></proof>
+  <proof prover="1"><result status="valid" time="0.25"/></proof>
   </goal>
   <goal name="WP_parameter match_string_ensures_default.4" expl="Assertion in line 21">
-  <proof prover="0"><result status="valid" time="0.10" steps="912"/></proof>
+  <proof prover="0"><result status="valid" time="0.12" steps="912"/></proof>
   </goal>
   <goal name="WP_parameter match_string_ensures_default.5" expl="Assertion in line 25">
-  <proof prover="0"><result status="valid" time="1.17" steps="9248"/></proof>
+  <proof prover="0"><result status="valid" time="1.31" steps="9979"/></proof>
   </goal>
   <goal name="WP_parameter match_string_ensures_default.6" expl="loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.28" steps="2440"/></proof>
+  <proof prover="0"><result status="valid" time="0.31" steps="2440"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="WP_parameter match_string_ensures_exists" expl="Function match_string, behavior exists" expanded="true">
- <proof prover="0"><result status="valid" time="1.31" steps="6472"/></proof>
+ <proof prover="0"><result status="valid" time="1.43" steps="6471"/></proof>
  </goal>
  <goal name="WP_parameter match_string_ensures_missing" expl="Function match_string, behavior missing" expanded="true">
- <proof prover="0"><result status="valid" time="0.28" steps="2393"/></proof>
+ <proof prover="0"><result status="valid" time="0.33" steps="2393"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/sessions/memchr.av/whole_program/why3session.xml b/sessions/memchr.av/whole_program/why3session.xml
@@ -780,7 +780,7 @@
 </theory>
 <theory name="Function_memchr_safety" sum="fb441ee9bf53de800dfc8a2f5436ac31" expanded="true">
  <goal name="WP_parameter memchr" expl="Function memchr, safety" expanded="true">
- <proof prover="0"><result status="valid" time="0.13" steps="840"/></proof>
+ <proof prover="0"><result status="valid" time="0.15" steps="840"/></proof>
  </goal>
 </theory>
 <theory name="Function_memchr_behaviors" sum="cc395d0f49147f835a4659cd06a70128" expanded="true">
@@ -790,24 +790,24 @@
   <proof prover="0"><result status="valid" time="0.03" steps="157"/></proof>
   </goal>
   <goal name="WP_parameter memchr_ensures_default.2" expl="Behavior completeness check">
-  <proof prover="0"><result status="valid" time="0.02" steps="155"/></proof>
+  <proof prover="0"><result status="valid" time="0.03" steps="155"/></proof>
   </goal>
   <goal name="WP_parameter memchr_ensures_default.3" expl="loop invariant init">
-  <proof prover="0"><result status="valid" time="0.31" steps="1788"/></proof>
+  <proof prover="0"><result status="valid" time="0.35" steps="1788"/></proof>
   </goal>
   <goal name="WP_parameter memchr_ensures_default.4" expl="loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.31" steps="1304"/></proof>
+  <proof prover="0"><result status="valid" time="0.34" steps="1304"/></proof>
   </goal>
   <goal name="WP_parameter memchr_ensures_default.5" expl="Assertion in line 18">
   <proof prover="0"><result status="valid" time="0.04" steps="290"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="WP_parameter memchr_ensures_found" expl="Function memchr, behavior found" expanded="true">
- <proof prover="0"><result status="valid" time="1.60" steps="7308"/></proof>
+ <proof prover="0"><result status="valid" time="1.80" steps="7308"/></proof>
  </goal>
  <goal name="WP_parameter memchr_ensures_not_exists" expl="Function memchr, behavior not_exists" expanded="true">
- <proof prover="0"><result status="valid" time="0.05" steps="426"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="426"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/sessions/memcmp.av/whole_program/why3session.xml b/sessions/memcmp.av/whole_program/why3session.xml
@@ -781,7 +781,7 @@
 </theory>
 <theory name="Function_memcmp_safety" sum="e7499e1c0257461e76c4cc03b9ffb17d" expanded="true">
  <goal name="WP_parameter memcmp" expl="Function memcmp, safety" expanded="true">
- <proof prover="1"><result status="valid" time="0.11"/></proof>
+ <proof prover="1"><result status="valid" time="0.13"/></proof>
  </goal>
 </theory>
 <theory name="Function_memcmp_behaviors" sum="f55880b5e5b70879e6b7df035e876764" expanded="true">
@@ -794,18 +794,18 @@
   <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
   </goal>
   <goal name="WP_parameter memcmp_ensures_default.3" expl="loop invariant init">
-  <proof prover="0"><result status="valid" time="0.09" steps="992"/></proof>
+  <proof prover="0"><result status="valid" time="0.10" steps="992"/></proof>
   </goal>
   <goal name="WP_parameter memcmp_ensures_default.4" expl="loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.40" steps="3146"/></proof>
+  <proof prover="0"><result status="valid" time="0.45" steps="3146"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="WP_parameter memcmp_ensures_diff" expl="Function memcmp, behavior diff" expanded="true">
- <proof prover="1"><result status="valid" time="0.22"/></proof>
+ <proof prover="1"><result status="valid" time="0.29"/></proof>
  </goal>
  <goal name="WP_parameter memcmp_ensures_equal" expl="Function memcmp, behavior equal" expanded="true">
- <proof prover="0"><result status="valid" time="0.07" steps="668"/></proof>
+ <proof prover="0"><result status="valid" time="0.08" steps="668"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/sessions/memcpy.av/whole_program/why3session.xml b/sessions/memcpy.av/whole_program/why3session.xml
@@ -773,20 +773,20 @@
 </theory>
 <theory name="Function_memcpy_safety" sum="0509ec78fd985bc6e247532ffc16630d" expanded="true">
  <goal name="WP_parameter memcpy" expl="Function memcpy, safety" expanded="true">
- <proof prover="0"><result status="valid" time="0.20" steps="1134"/></proof>
+ <proof prover="0"><result status="valid" time="0.22" steps="1134"/></proof>
  </goal>
 </theory>
 <theory name="Function_memcpy_behaviors" sum="487a640bac9a93147f3a631a74ab740c" expanded="true">
  <goal name="WP_parameter memcpy_ensures_default" expl="Function memcpy, default behavior" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter memcpy_ensures_default.1" expl="loop invariant init">
-  <proof prover="0"><result status="valid" time="0.92" steps="3445"/></proof>
+  <proof prover="0"><result status="valid" time="1.08" steps="3445"/></proof>
   </goal>
   <goal name="WP_parameter memcpy_ensures_default.2" expl="loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.21"/></proof>
+  <proof prover="1"><result status="valid" time="0.32"/></proof>
   </goal>
   <goal name="WP_parameter memcpy_ensures_default.3" expl="Assertion in line 20">
-  <proof prover="0"><result status="valid" time="0.05" steps="383"/></proof>
+  <proof prover="0"><result status="valid" time="0.06" steps="383"/></proof>
   </goal>
   <goal name="WP_parameter memcpy_ensures_default.4" expl="Postcondition">
   <proof prover="0"><result status="valid" time="0.03" steps="211"/></proof>