Commit 7f895454 authored by MARCHE Claude's avatar MARCHE Claude

pairing old/new goals tries to be conservative

with old Why3 version where sessions do not contain goal shapes
parent 7acaf877
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/fib_memo/why3session.xml">
<why3session name="programs/fib_memo/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../fib_memo.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter fibo" expl="correctness of parameter fibo" sum="f0a3a1ac8674e9e268ae11f8df9ff39d" proved="true" expanded="true">
<goal name="WP_parameter fibo" expl="parameter fibo" sum="b2f9c59516b56e8121a870326cd6372f" proved="true" expanded="true" shape="iainfix <=V0c1ainvV1Aainfix =c1afibV0ainvV4Aainfix =ainfix +V3V5afibV0IainvV4Aainfix =V5afibainfix -V0c2FFAainvV2Aainfix <=c0ainfix -V0c2IainvV2Aainfix =V3afibainfix -V0c1FFAainvV1Aainfix <=c0ainfix -V0c1IainvV1Aainfix <=c0V0FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter memo_fibo" expl="correctness of parameter memo_fibo" sum="9373cd2e2bcff22cf5eaa6b757149684" proved="true" expanded="true">
<goal name="WP_parameter memo_fibo" expl="parameter memo_fibo" sum="bf0eac17c1109b6bf5a06bc4de105cb4" proved="true" expanded="true" shape="ainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2Aainfix =V3afibV0FFAainvV1Aainfix <=c0V0Iainfix =agetV1V0aNoneAainvV1Aainfix =V5afibV0Iainfix =agetV1V0aSomeV5FIainvV1Aainfix <=c0V0FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter memo_fibo.1" expl="normal postcondition" sum="935d25dee5b707cf0bd087e131e709da" proved="true" expanded="true">
<goal name="WP_parameter memo_fibo.1" expl="normal postcondition" sum="191aa05a82087b2fe04b6ec1f56aea5c" proved="true" expanded="true" shape="ainvV1Aainfix =V2afibV0Iainfix =agetV1V0aSomeV2FIainvV1Aainfix <=c0V0FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter memo_fibo.2" expl="precondition" sum="2efb9e3e13eeb740e06fe133ea0ed5da" proved="true" expanded="true">
<goal name="WP_parameter memo_fibo.2" expl="precondition" sum="8913ff358744193d16e3e8c0e70410cb" proved="true" expanded="true" shape="ainvV1Aainfix <=c0V0Iainfix =agetV1V0aNoneIainvV1Aainfix =V2afibV0Iainfix =agetV1V0aSomeV2FIainvV1Aainfix <=c0V0FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter memo_fibo.3" expl="normal postcondition" sum="12383032cf9410a6d7547ff592884006" proved="true" expanded="true">
<goal name="WP_parameter memo_fibo.3" expl="normal postcondition" sum="a07d81d85f066a7daf5413f54edf2ea7" proved="true" expanded="true" shape="ainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2Aainfix =V3afibV0FFIainvV1Aainfix <=c0V0Iainfix =agetV1V0aNoneIainvV1Aainfix =V5afibV0Iainfix =agetV1V0aSomeV5FIainvV1Aainfix <=c0V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/same_fringe/why3session.xml">
<why3session name="programs/same_fringe/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../same_fringe.mlw" verified="true" expanded="true">
<theory name="WP SameFringe" verified="true" expanded="true">
<goal name="WP_parameter enum" expl="correctness of parameter enum" sum="bdf86692af3d9108fb10b1c5ad0566cb" proved="true" expanded="true">
<goal name="WP_parameter enum" expl="parameter enum" sum="81ad6789c82a5da87d82ed79c481b2d8" proved="true" expanded="true" shape="CV0aEmptyainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aNodeVVVainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FAtAainfix <alengthaelementsV2alengthaelementsV0Aainfix <=c0alengthaelementsV0FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter enum.1" expl="correctness of parameter enum" sum="a6693a559bfaec7856fabbbd720cd46d" proved="true" expanded="true">
<goal name="WP_parameter enum.1" expl="parameter enum" sum="b4034ddbcbdc1870740ae9d636804019" proved="true" expanded="true" shape="CV0aEmptyainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aNodeVVVtFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter enum.2" expl="correctness of parameter enum" sum="1738f0e9c67bc5354834008977e07775" proved="true" expanded="true">
<goal name="WP_parameter enum.2" expl="parameter enum" sum="b21b169de882b1e10c977d31940d96cb" proved="true" expanded="true" shape="CV0aEmptytaNodeVVVtAainfix <alengthaelementsV2alengthaelementsV0Aainfix <=c0alengthaelementsV0FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter enum.3" expl="correctness of parameter enum" sum="ad0c532ed8c898123ca6cc75e6c44cb5" proved="true" expanded="true">
<goal name="WP_parameter enum.3" expl="parameter enum" sum="e5340919f1183dcd6ac96cd13e3a7645" proved="true" expanded="true" shape="CV0aEmptytaNodeVVVainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FItAainfix <alengthaelementsV2alengthaelementsV0Aainfix <=c0alengthaelementsV0FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter eq_enum" expl="correctness of parameter eq_enum" sum="d3dfe508d88185c560d08001b044edcb" proved="true" expanded="true">
<goal name="WP_parameter eq_enum" expl="parameter eq_enum" sum="3c50db5bd3ec55393c2ddd90f9945fd4" proved="true" expanded="true" shape="CV1aNextVVVCV0aNextVVViainfix =V5V2ainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV8aenum_elementsV9qainfix =V10aTrueFAtAainfix <alengthaenum_elementsV8alengthaenum_elementsV0Aainfix <=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV3aenum_elementsV4FIainfix =aenum_elementsV8ainfix ++aelementsV6aenum_elementsV7Fainfix =aenum_elementsV0aenum_elementsV1qfwainfix =aenum_elementsV0aenum_elementsV1qfaDoneCV0aDoneainfix =aenum_elementsV0aenum_elementsV1qtwainfix =aenum_elementsV0aenum_elementsV1qfFF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.1" expl="correctness of parameter eq_enum" sum="541824b988f4678bfb4e4b13dab9ba9b" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.1" expl="parameter eq_enum" sum="a51108cd4c449d92c487a33109b079ab" proved="true" expanded="true" shape="CV1aNextVVVCV0aNextVVVtAainfix <alengthaenum_elementsV8alengthaenum_elementsV0Aainfix <=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV3aenum_elementsV4FIainfix =aenum_elementsV8ainfix ++aelementsV6aenum_elementsV7FIainfix =V5V2wtaDonetFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.2" expl="correctness of parameter eq_enum" sum="6af4cbaa87aae0d4f4abb13e1285a5e1" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.2" expl="parameter eq_enum" sum="c8bc4bb5bb758e3f084765762b126c9e" proved="true" expanded="true" shape="CV1aNextVVVCV0aNextVVVainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV8aenum_elementsV9qainfix =V10aTrueFItAainfix <alengthaenum_elementsV8alengthaenum_elementsV0Aainfix <=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV3aenum_elementsV4FIainfix =aenum_elementsV8ainfix ++aelementsV6aenum_elementsV7FIainfix =V5V2wtaDonetFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.3" expl="correctness of parameter eq_enum" sum="57cd5beee94ebf4da014c8011ed7ec67" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.3" expl="parameter eq_enum" sum="2baa166ded999d479c6c60aea2d17ab7" proved="true" expanded="true" shape="CV1aNextVVVCV0aNextVVVainfix =aenum_elementsV0aenum_elementsV1qfIainfix =V5V2NwtaDonetFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.4" expl="correctness of parameter eq_enum" sum="25a36c430de0ebe984ce2e0f408f1a07" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.4" expl="parameter eq_enum" sum="30d09d4dcd66e07e2f747776c8fc5634" proved="true" expanded="true" shape="CV1aNextVVVCV0aNextVVVtwainfix =aenum_elementsV0aenum_elementsV1qfaDonetFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.5" expl="correctness of parameter eq_enum" sum="97b8f446464842dc4d839da5b5961fdb" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.5" expl="parameter eq_enum" sum="edf75c415095e661d5c2f42c41e868f0" proved="true" expanded="true" shape="CV1aNextVVVtaDoneCV0aDoneainfix =aenum_elementsV0aenum_elementsV1qtwtFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.6" expl="correctness of parameter eq_enum" sum="32374fa5283ef3c4909474d899dcacdf" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.6" expl="parameter eq_enum" sum="5391a12c5cf5917c768f8405db0df747" proved="true" expanded="true" shape="CV1aNextVVVtaDoneCV0aDonetwainfix =aenum_elementsV0aenum_elementsV1qfFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter same_fringe" expl="normal postcondition" sum="735f92bd11fb50afcf213c093d95fac9" proved="true" expanded="true">
<goal name="WP_parameter same_fringe" expl="normal postcondition" sum="9562e52813643d97602e52910d53384d" proved="true" expanded="true" shape="ainfix =aelementsV0aelementsV1qainfix =V4aTrueIainfix =aenum_elementsV2aenum_elementsV3qainfix =V4aTrueFIainfix =aenum_elementsV3ainfix ++aelementsV1aenum_elementsaDoneFIainfix =aenum_elementsV2ainfix ++aelementsV0aenum_elementsaDoneFFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
......
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/zeros/why3session.xml">
<why3session name="programs/zeros/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../zeros.mlw" verified="true" expanded="true">
<theory name="WP SetZeros" verified="true" expanded="true">
<goal name="WP_parameter set_zeros" expl="correctness of parameter set_zeros" sum="608a2ce58877f53e9321cbda96aef314" proved="true" expanded="true">
<goal name="WP_parameter set_zeros" expl="parameter set_zeros" sum="f6e18a017be683ab3093cfd0d89c2089" proved="true" expanded="true" shape="ainfix =agetV2V3c0Iainfix <V3V0Aainfix <=c0V3FIainfix =agetV2V4c0Iainfix <V4ainfix +ainfix -V0c1c1Aainfix <=c0V4FAainfix =agetV6V7c0Iainfix <V7ainfix +V5c1Aainfix <=c0V7FIainfix =V6asetV2V5c0FAainfix <V5V0Aainfix <=c0V5Iainfix =agetV2V8c0Iainfix <V8V5Aainfix <=c0V8FIainfix <=V5ainfix -V0c1Aainfix <=c0V5FFAainfix =agetV1V9c0Iainfix <V9c0Aainfix <=c0V9FIainfix <=c0ainfix -V0c1Aainfix =agetV1V10c0Iainfix <V10V0Aainfix <=c0V10FIainfix >c0ainfix -V0c1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.1" expl="normal postcondition" sum="a431d4701cdb317ba9ec6e8ce36fd903" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.1" expl="normal postcondition" sum="f58245d4b3f2788b8faec89e71a4593d" proved="true" expanded="true" shape="ainfix =agetV1V2c0Iainfix <V2V0Aainfix <=c0V2FIainfix >c0ainfix -V0c1FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.2" expl="for loop initialization" sum="4fdcef61de7fd0dbce171e29c6a6c2c2" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.2" expl="for loop initialization" sum="f48c054282a92445bcc73fe91552336b" proved="true" expanded="true" shape="ainfix =agetV1V2c0Iainfix <V2c0Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.3" expl="for loop preservation" sum="c3bc7e2f309687b6496a3c2155d9f105" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.3" expl="for loop preservation" sum="1c42dec1a25f08c3595dee18bd3abcef" proved="true" expanded="true" shape="ainfix =agetV4V5c0Iainfix <V5ainfix +V3c1Aainfix <=c0V5FIainfix =V4asetV2V3c0FAainfix <V3V0Aainfix <=c0V3Iainfix =agetV2V6c0Iainfix <V6V3Aainfix <=c0V6FIainfix <=V3ainfix -V0c1Aainfix <=c0V3FFIainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.4" expl="normal postcondition" sum="09ba19838fab192b5d1170a3f4919eb9" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.4" expl="normal postcondition" sum="afbeb8d431c04bf7131f317e6f9036df" proved="true" expanded="true" shape="ainfix =agetV2V3c0Iainfix <V3V0Aainfix <=c0V3FIainfix =agetV2V4c0Iainfix <V4ainfix +ainfix -V0c1c1Aainfix <=c0V4FFIainfix <=c0ainfix -V0c1FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter harness" expl="correctness of parameter harness" sum="65df51e3d0d0d1ffbbacf1a0e8b9ab4d" proved="true" expanded="true">
<goal name="WP_parameter harness" expl="parameter harness" sum="3bbc0bd5226781b088ca904ff4fcbfe8" proved="true" expanded="true" shape="ainfix =agetV0c12c0Aainfix =c42c42Iainfix =agetV0V1c0Iainfix <V1c42Aainfix <=c0V1FFAainfix >=c42c0">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter harness.1" expl="precondition" sum="284da52c8b6d467e508ce632f80c060f" proved="true" expanded="true">
<goal name="WP_parameter harness.1" expl="precondition" sum="bc9d5154bb22af5e7d53d24481e085a3" proved="true" expanded="true" shape="ainfix >=c42c0">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter harness.2" expl="assertion" sum="6401951319f58db7beb77a4ecffcafdb" proved="true" expanded="true">
<goal name="WP_parameter harness.2" expl="assertion" sum="b8e5898048ee9697e7392cdd5b7693ec" proved="true" expanded="true" shape="ainfix =c42c42Iainfix =agetV0V1c0Iainfix <V1c42Aainfix <=c0V1FFIainfix >=c42c0">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter harness.3" expl="assertion" sum="b720467ebdc03ae1045b93f08b0ca3b8" proved="true" expanded="true">
<goal name="WP_parameter harness.3" expl="assertion" sum="4549ac88635e016fd559fc0a901e31a4" proved="true" expanded="true" shape="ainfix =agetV0c12c0Iainfix =c42c42Iainfix =agetV0V1c0Iainfix <V1c42Aainfix <=c0V1FFIainfix >=c42c0">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
......
......@@ -880,7 +880,14 @@ let associate_subgoals gname old_goals new_goals =
ordered by shapes, then by name *)
let old_goals_without_pairing =
Hashtbl.fold
(fun _ g acc -> (g.goal_shape,Old_goal g)::acc)
(fun _ g acc ->
let s = g.goal_shape in
if s = "" then
(* We don't try to associate old goals without shapes:
they will be paired in order in next phase *)
acc
else
(s,Old_goal g)::acc)
old_goals_map
[]
in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment