Skip to content
This repository has been archived by the owner on Feb 24, 2023. It is now read-only.

Commit

Permalink
sessions: update verification artifacts with new strategy
Browse files Browse the repository at this point in the history 
Signed-off-by: Denis Efremov <[email protected]>
  • Loading branch information
@evdenis
evdenis committed Sep 7, 2020
1 parent 64d4fdb commit e5926d1
Show file tree
Hide file tree
Showing 29 changed files with 11,419 additions and 11,578 deletions.
1,092 changes: 546 additions & 546 deletions sessions/_parse_integer_fixup_radix.av/whole_program/why3session.xml
View file

Large diffs are not rendered by default.

18 changes: 9 additions & 9 deletions sessions/check_bytes8.av/whole_program/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -793,43 +793,43 @@
</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.18"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
</theory>
<theory name="Function_check_bytes8_0_behaviors" sum="56f6c92a103ac54a5d98c66f41419a6d" expanded="true">
<goal name="WP_parameter check_bytes8_ensures_default" expl="Function check_bytes8, default behavior" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter check_bytes8_ensures_default.1" expl="Behavior disjointness check">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter check_bytes8_ensures_default.2" expl="Behavior completeness check">
<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.16" steps="783"/></proof>
<proof prover="0"><result status="valid" time="0.10" 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.03" steps="199"/></proof>
<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.71" steps="1632"/></proof>
<proof prover="0"><result status="valid" time="1.20" 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.02" steps="36"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
<goal name="WP_parameter check_bytes8_ensures_default.7" expl="Assertion in line 24">
<proof prover="0"><result status="valid" time="0.02" steps="38"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
<goal name="WP_parameter check_bytes8_ensures_default.8" expl="Ensures clause (Postcondition)">
<proof prover="0"><result status="valid" time="0.01" steps="40"/></proof>
</goal>
</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.25"/></proof>
<proof prover="1"><result status="valid" time="0.14"/></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.04" steps="220"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="220"/></proof>
</goal>
</theory>
</file>
Expand Down
1,028 changes: 514 additions & 514 deletions sessions/kstrtobool.av/whole_program/why3session.xml
View file

Large diffs are not rendered by default.

30 changes: 10 additions & 20 deletions sessions/match_string.av/whole_program/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -849,47 +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.29"/></proof>
<proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
</theory>
<theory name="Function_match_string_0_behaviors" sum="d6c42d1a6fec4b2bc0c7eb8d1d6911b5" expanded="true">
<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.05" steps="151"/></proof>
<proof prover="0"><result status="valid" time="0.03" 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.05" steps="149"/></proof>
<proof prover="0"><result status="valid" time="0.03" 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.45"/></proof>
<proof prover="1"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_default.4" expl="Assertion in line 21">
<proof prover="0"><result status="valid" time="0.16" steps="912"/></proof>
<proof prover="0"><result status="valid" time="0.10" 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.86" steps="9248"/></proof>
<proof prover="0"><result status="valid" time="1.17" steps="9248"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_default.6" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.46" steps="2440"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="2440"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter match_string_ensures_exists" expl="Function match_string, behavior exists" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter match_string_ensures_exists.1" expl="Postcondition (Ensures clause)">
<proof prover="1"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_exists.2" expl="Postcondition (Ensures clause)">
<proof prover="0"><result status="valid" time="1.70" steps="5089"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_exists.3" expl="Postcondition (Ensures clause)">
<proof prover="0"><result status="valid" time="0.06" steps="174"/></proof>
</goal>
</transf>
<proof prover="0"><result status="valid" time="1.31" steps="6472"/></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.45" steps="2393"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="2393"/></proof>
</goal>
</theory>
</file>
Expand Down
Loading

0 comments on commit e5926d1

Please sign in to comment.