Skip to content

GitLab

Commit bec791f5 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Fix parsing of session with &apos change into &#39 

Also fix session for isqrt_von_neumann
parent 64b99863
Hide whitespace changes
Inline Side-by-side
examples/in_progress/isqrt_von_neumann/why3session.xml
View file @ bec791f5
......@@ -6,9 +6,9 @@
<prover id="2" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../isqrt_von_neumann.mlw" proved="true">
<theory name="VonNeumann16" proved="true" sum="db8b040e903a2c035bb41ec603ff581b">
<theory name="VonNeumann16" proved="true" sum="7527676c975863f85bbe982b8d57ec90">
<goal name="sqr_add" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.54"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="WP_parameter isqrt16" expl="VC for isqrt16" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -135,9 +135,13 @@
</transf>
</goal>
</theory>
<theory name="VonNeumann32" proved="true" sum="746298fe886ad2963f62629b7e7c9def">
<theory name="VonNeumann32" proved="true" sum="c653c0d708e3429d78f15d4b17bbb5a8">
<goal name="sqr_add" proved="true">
<proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="8.47"/></proof>
<transf name="unfold" proved="true" arg1="sqr">
<goal name="sqr_add.0" proved="true">
<proof prover="2" timelimit="20"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter isqrt32" expl="VC for isqrt32" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -205,7 +209,7 @@
<proof prover="3"><result status="valid" time="0.59"/></proof>
</goal>
<goal name="WP_parameter isqrt32.21" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.14"/></proof>
<proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="WP_parameter isqrt32.22" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.11"/></proof>
......@@ -250,11 +254,10 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt32.36" expl="loop invariant preservation" proved="true">
<proof prover="2" timelimit="100"><result status="timeout" time="100.00"/></proof>
<proof prover="3" timelimit="100"><result status="valid" time="74.18"/></proof>
<proof prover="3" timelimit="100"><result status="valid" time="113.42"/></proof>
</goal>
<goal name="WP_parameter isqrt32.37" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
<proof prover="3"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter isqrt32.38" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.22"/></proof>
......@@ -265,7 +268,7 @@
</transf>
</goal>
</theory>
<theory name="VonNeumann64" proved="true" sum="f3744af4e1b960b3ad3b97fc0a4aeb7a">
<theory name="VonNeumann64" proved="true" sum="d204c15eca5382a7d977c890f4b62b1a">
<goal name="sqr_add" proved="true">
<transf name="unfold" proved="true" arg1="sqr">
<goal name="sqr_add.0" proved="true">
......@@ -313,7 +316,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt64.10" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.28"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter isqrt64.11" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -328,16 +331,16 @@
<proof prover="3"><result status="valid" time="1.32"/></proof>
</goal>
<goal name="WP_parameter isqrt64.15" expl="assertion" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="3.66"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.73"/></proof>
</goal>
<goal name="WP_parameter isqrt64.16" expl="assertion" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.62"/></proof>
</goal>
<goal name="WP_parameter isqrt64.17" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="1.75"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="1.87"/></proof>
</goal>
<goal name="WP_parameter isqrt64.18" expl="assertion" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="3.08"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="3.60"/></proof>
</goal>
<goal name="WP_parameter isqrt64.19" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.55"/></proof>
......@@ -346,10 +349,10 @@
<proof prover="3"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="WP_parameter isqrt64.21" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="3.90"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.54"/></proof>
</goal>
<goal name="WP_parameter isqrt64.22" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="1.14"/></proof>
<proof prover="3"><result status="valid" time="0.76"/></proof>
</goal>
<goal name="WP_parameter isqrt64.23" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.79"/></proof>
......@@ -358,7 +361,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt64.25" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.79"/></proof>
<proof prover="3"><result status="valid" time="1.08"/></proof>
</goal>
<goal name="WP_parameter isqrt64.26" expl="loop invariant preservation" proved="true">
<transf name="rewrite" proved="true" arg1="H21">
......@@ -377,7 +380,7 @@
<goal name="WP_parameter isqrt64.26.0.0.0.0.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="rewrite" proved="true" arg1="H17">
<goal name="WP_parameter isqrt64.26.0.0.0.0.0.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="3.49"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="4.81"/></proof>
</goal>
</transf>
</goal>
......@@ -421,10 +424,10 @@
<proof prover="3"><result status="valid" time="0.64"/></proof>
</goal>
<goal name="WP_parameter isqrt64.32" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="4.80"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="3.80"/></proof>
</goal>
<goal name="WP_parameter isqrt64.33" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="1.36"/></proof>
<proof prover="3"><result status="valid" time="1.07"/></proof>
</goal>
<goal name="WP_parameter isqrt64.34" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -450,7 +453,7 @@
<goal name="WP_parameter isqrt64.39.0.0.0" expl="VC for isqrt64" proved="true">
<transf name="assert" proved="true" arg1="(x = add (sqr res_g) num)">
<goal name="WP_parameter isqrt64.39.0.0.0.0" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.36"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="1.84"/></proof>
</goal>
<goal name="WP_parameter isqrt64.39.0.0.0.1" expl="VC for isqrt64" proved="true">
<transf name="unfold" proved="true" arg1="sqr">
......@@ -478,7 +481,7 @@
<transf name="rewrite" proved="true" arg1="h">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.0.0.1.0.1.0" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="295"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="2.95"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="3.68"/></proof>
</goal>
</transf>
</goal>
......@@ -505,7 +508,7 @@
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0" expl="VC for isqrt64" proved="true">
<transf name="unfold" proved="true" arg1="pred" arg2="in" arg3="h2">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0" expl="VC for isqrt64" proved="true">
<transf name="assert" proved="true" arg1="(forall a b c. t&apos;int b + t&apos;int c &lt; two_power_size -&gt; ule a b -&gt; ule (add a c) (add b c))">
<transf name="assert" proved="true" arg1="(forall a b c. t&#39;int b + t&#39;int c &lt; two_power_size -&gt; ule a b -&gt; ule (add a c) (add b c))">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="137"/></proof>
</goal>
......@@ -546,7 +549,7 @@
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.0.0.1.0.1" proved="true">
<transf name="split_all_wp" proved="true" >
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.0.0.1.0.1.0" proved="true">
<transf name="assert" proved="true" arg1="(0 &lt;= t&apos;int b - t&apos;int (1:t))">
<transf name="assert" proved="true" arg1="(0 &lt;= t&#39;int b - t&#39;int (1:t))">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.0.0.1.0.1.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.06" steps="226"/></proof>
</goal>
......@@ -590,7 +593,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1" proved="true">
<transf name="replace" proved="true" arg1="(t&apos;int (2:t))" arg2="2">
<transf name="replace" proved="true" arg1="(t&#39;int (2:t))" arg2="2">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0" proved="true">
<transf name="rewrite" proved="true" arg1="h">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0" proved="true">
......@@ -598,7 +601,7 @@
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0" proved="true">
<transf name="rewrite" proved="true" arg1="&lt;-" arg2="to_uint_add_bounded">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0.0" proved="true">
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="5.56" steps="44447"/></proof>
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="7.70" steps="44446"/></proof>
</goal>
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0.1" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.60"/></proof>
......@@ -639,11 +642,11 @@
<proof prover="1"><result status="valid" time="0.02" steps="103"/></proof>
</goal>
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1" proved="true">
<transf name="replace" proved="true" arg1="(t&apos;int (2:t))" arg2="2">
<transf name="replace" proved="true" arg1="(t&#39;int (2:t))" arg2="2">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0" proved="true">
<transf name="rewrite" proved="true" arg1="h">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0" proved="true">
<transf name="assert" proved="true" arg1="(((t&apos;int bits_g1 + t&apos;int res_g) * (t&apos;int bits_g1 + t&apos;int res_g)) &lt;= two_power_size)">
<transf name="assert" proved="true" arg1="(((t&#39;int bits_g1 + t&#39;int res_g) * (t&#39;int bits_g1 + t&#39;int res_g)) &lt;= two_power_size)">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0" proved="true">
<transf name="replace" proved="true" arg1="two_power_size" arg2="(0x100000000 * 0x100000000)">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0" proved="true">
......@@ -687,12 +690,12 @@
</transf>
</goal>
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.1.0.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.34"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="1.67"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1.1.0.0.1.1.1.0.0.1.0.1.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="2.38"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="2.81"/></proof>
</goal>
</transf>
</goal>
......@@ -758,7 +761,7 @@
<proof prover="3"><result status="valid" time="0.58"/></proof>
</goal>
<goal name="WP_parameter isqrt64.40.1" expl="VC for isqrt64" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.74"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.00"/></proof>
</goal>
</transf>
</goal>
......
src/session/xml.mll
View file @ bec791f5
......@@ -167,6 +167,9 @@ and string_val = parse
| "&apos;"
{ Buffer.add_char buf '\'';
string_val lexbuf }
| "&#39;"
{ Buffer.add_char buf '\'';
string_val lexbuf }
| "&amp;"
{ Buffer.add_char buf '&';
string_val lexbuf }
......
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