Commit 249f4d95 authored by MARCHE Claude's avatar MARCHE Claude

fix proofs after change of Array.make precondition

parent 7bb00702
......@@ -326,13 +326,13 @@
</goal>
</theory>
</file>
<file name="../test_harness.mlw" verified="true" expanded="true">
<theory name="WP TestHarness" verified="true" expanded="true">
<goal name="WP_parameter testHarness" expl="correctness of parameter testHarness" sum="9bf9a58ff02f674f4f5f98ccdc628cd5" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter testHarness.1" expl="precondition" sum="3577cf310d4189b1fc0c281686e58579" proved="true" expanded="true">
<file name="../test_harness.mlw" verified="true" expanded="false">
<theory name="WP TestHarness" verified="true" expanded="false">
<goal name="WP_parameter testHarness" expl="correctness of parameter testHarness" sum="f02720f70bcb802728fa773feb0c1ae0" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter testHarness.1" expl="precondition" sum="eb63d9e9f3585d807610d9f6beac9bb1" proved="true" expanded="false">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.02"/>
......@@ -341,7 +341,7 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.2" expl="precondition" sum="29678ad56aabcb17bfc46d5cd6bd6024" proved="true" expanded="true">
<goal name="WP_parameter testHarness.2" expl="precondition" sum="692fb1c3ceba7a0d7b2259138bdde378" proved="true" expanded="false">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
......@@ -352,73 +352,84 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.3" expl="precondition" sum="b5eadc88e6559ff1b43cbdb32693ff09" proved="true" expanded="true">
<goal name="WP_parameter testHarness.3" expl="precondition" sum="f3469d84de5cabe46004f8661a8b2b9c" proved="true" expanded="false">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.4" expl="precondition" sum="433c12e9a0093e7e91ffd4ee623cd741" proved="true" expanded="true">
<goal name="WP_parameter testHarness.4" expl="precondition" sum="446680484efa46e51716fbe5de7a8fba" proved="true" expanded="false">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.5" expl="precondition" sum="edb204133fe560539e6ed5514bd6f4f4" proved="true" expanded="false">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.5" expl="assertion" sum="683bb822fa2a4014ab8cb16db12d7b81" proved="true" expanded="true">
<goal name="WP_parameter testHarness.6" expl="assertion" sum="31226dc65dfdbefea1542f0c08af62a8" proved="true" expanded="false">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.17"/>
<result status="valid" time="0.19"/>
</proof>
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.6" expl="assertion" sum="4a3a0f1d71d49f31290e456cf87de55f" proved="true" expanded="true">
<goal name="WP_parameter testHarness.7" expl="assertion" sum="fcd970a315e129a50f4a1dfd79ade5c3" proved="true" expanded="false">
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.13"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.7" expl="assertion" sum="23bbaf2815454f81e91cf2f622f7386c" proved="true" expanded="true">
<goal name="WP_parameter testHarness.8" expl="assertion" sum="7aa05a6097354f0613236a4092b830bb" proved="true" expanded="false">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.8" expl="assertion" sum="87ad0f8f7d5ba7eb903c8ee9cf6a1c88" proved="true" expanded="true">
<goal name="WP_parameter testHarness.9" expl="assertion" sum="b3573f6b21552e59421b359c792866e3" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.70"/>
</proof>
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.13"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.9" expl="assertion" sum="831517ebd729bfff55c0b23345b79dad" proved="true" expanded="true">
<goal name="WP_parameter testHarness.10" expl="assertion" sum="b8e76c18e73c31dabc1732a65a66b464" proved="true" expanded="false">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.10" expl="assertion" sum="17707e1eb34cf6c5a7ca8cfbab478cc6" proved="true" expanded="true">
<goal name="WP_parameter testHarness.11" expl="assertion" sum="622210295d298e88d2e0bb451fda108d" proved="true" expanded="false">
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="1.51"/>
<result status="valid" time="1.48"/>
</proof>
</goal>
<goal name="WP_parameter testHarness.11" expl="assertion" sum="69ff549c83f05f201976a49f23c7da67" proved="true" expanded="true">
<goal name="WP_parameter testHarness.12" expl="assertion" sum="98396ad9599534f76d993608b45c8b04" proved="true" expanded="false">
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.15"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
</transf>
......
......@@ -133,71 +133,79 @@
</goal>
</theory>
<theory name="WP TestCase" verified="true" expanded="true">
<goal name="WP_parameter test_case" expl="correctness of parameter test_case" sum="92454d139006992eeb57807ade03fb36" proved="true" expanded="true">
<goal name="WP_parameter test_case" expl="correctness of parameter test_case" sum="137c1f7a6676a39e94a3efa190022da4" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter test_case.1" expl="precondition" sum="9a3d89df4528c721ea8109204221271f" proved="true" expanded="true">
<goal name="WP_parameter test_case.1" expl="precondition" sum="f316cb64e14c63f2b981efde6be1f43e" proved="true" expanded="true">
<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 test_case.2" expl="precondition" sum="3096a557cd675399194bbd2c551352bf" proved="true" expanded="true">
<goal name="WP_parameter test_case.2" expl="precondition" sum="129ae2c2ec585e083f304c75e02d7059" proved="true" expanded="true">
<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 test_case.3" expl="precondition" sum="b32358f72b7a3570c4adf05c3aff5816" proved="true" expanded="true">
<goal name="WP_parameter test_case.3" expl="precondition" sum="cb53b856c9c68d5041e5e9e2d1472425" proved="true" expanded="true">
<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 test_case.4" expl="precondition" sum="0304d9d7b621785def666babe3788f2d" proved="true" expanded="true">
<goal name="WP_parameter test_case.4" expl="precondition" sum="87b8e4c0e5f7e396117b49b288dbb29c" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter test_case.5" expl="precondition" sum="b8c3f6eb45aecf0f82c3f41310f716c1" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter test_case.6" expl="precondition" sum="a6bb471987ff832cadca539c6cdb2123" proved="true" expanded="true">
<goal name="WP_parameter test_case.5" expl="precondition" sum="480ce07436e3c4f3f9004102858a5a5e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter test_case.7" expl="precondition" sum="e943e0dad5d66d295351e33d231250ac" proved="true" expanded="true">
<goal name="WP_parameter test_case.6" expl="precondition" sum="26fe47d86bdf55d43ebaa76e717dcfbc" proved="true" expanded="true">
<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 test_case.8" expl="precondition" sum="751914ade0f01432a2981c34674d6c8f" proved="true" expanded="true">
<goal name="WP_parameter test_case.7" expl="precondition" sum="dedec8b54b8eefeb72c3101e0126e3f8" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter test_case.9" expl="precondition" sum="ee8dba8cb75733dd105a9909857b4e06" proved="true" expanded="true">
<goal name="WP_parameter test_case.8" expl="precondition" sum="a1cfbe04c461ccf5f752259330b23e2a" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter test_case.9" expl="precondition" sum="7adcbaff11921c0911eb026afbc40290" proved="true" expanded="true">
<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 test_case.10" expl="precondition" sum="5f8f3627637f58e62b8be023254dde03" proved="true" expanded="true">
<goal name="WP_parameter test_case.10" expl="precondition" sum="afc510eb1a97bc3905c2751d0bc0a1c7" proved="true" expanded="true">
<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 test_case.11" expl="precondition" sum="6973eafeefa4ed74c5cd8060b663c837" proved="true" expanded="true">
<goal name="WP_parameter test_case.11" expl="precondition" sum="37e2143fb5c2f86b94b0cd005774e7c8" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter test_case.12" expl="assertion" sum="f2476ebf52fb88637bd9ca9ef47aa198" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal name="WP_parameter test_case.12" expl="precondition" sum="49eda2eaaedccb3481367929a48f5f66" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal name="WP_parameter test_case.13" expl="assertion" sum="23cd82d3fc14f110fd4dfd1909c4b7dd" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.33"/>
<goal name="WP_parameter test_case.13" expl="assertion" sum="9b57dd07077d6706a8d09a50cf6c0ef4" proved="true" expanded="true">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.24"/>
</proof>
</goal>
<goal name="WP_parameter test_case.14" expl="assertion" sum="aed016b10f13b1997416ecb34a90b656" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="3" edited="" obsolete="false">
<result status="valid" time="2.71"/>
</proof>
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
......
......@@ -31,25 +31,25 @@ run_dir () {
done
}
# echo "=== Logic ==="
# run_dir .
# echo ""
echo "=== Logic ==="
run_dir .
echo ""
# echo "=== BTS ==="
# run_dir bts
# echo ""
echo "=== BTS ==="
run_dir bts
echo ""
# echo "=== Programs ==="
# run_dir programs
# echo ""
echo "=== Programs ==="
run_dir programs
echo ""
echo "=== Programs in their own subdir ==="
run_dir programs/vacid_0_binary_heaps "-I programs/vacid_0_binary_heaps"
echo ""
# echo "=== Check Builtin translation ==="
# run_dir check-builtin
# echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
exit $res
......
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