Skip to content

GitLab

Commit a7d6c9ad authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Fix problem with labelled variables to Alt-Ergo

parent 1dd432e7
Hide whitespace changes
Inline Side-by-side
examples/tests-provers/alt-ergo-models.mlw
View file @ a7d6c9ad
......@@ -25,13 +25,7 @@ module M1
use import module ref.Ref
let g (x "model:0": ref int) : int =
{ }
x := !x + 1;
if ("model:cond" !x >= 42) then !x + 3 else 0
{ "model:post" result <= 50 }
let g_no_label (x : ref int) : int =
let g (x : ref int) : int =
{ }
x := !x + 1;
if (!x >= 42) then !x + 3 else 0
......
examples/tests-provers/alt-ergo-models/why3session.xml
View file @ a7d6c9ad
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="alt-ergo-models/why3session.xml">
<prover
......@@ -29,11 +29,11 @@
name="expl:parameter f"/>
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
......@@ -49,11 +49,11 @@
name="expl:parameter f_no_lab"/>
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
......@@ -69,33 +69,11 @@
name="expl:parameter g"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
edited="altmnergomnmodels-WP_M1-WP_parameter_g_1.why"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter g_no_label"
locfile="alt-ergo-models/../alt-ergo-models.mlw"
loclnum="34" loccnumb="6" loccnume="16"
expl="parameter g_no_label"
sum="907795ff697c8edc23616ffdf2169e79"
proved="false"
expanded="true"
shape="iainfix &gt;=V1c42ainfix &lt;=ainfix +V1c3c50ainfix &lt;=c0c50Iainfix =V1ainfix +V0c1FF">
<label
name="expl:parameter g_no_label"/>
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
edited="altmnergomnmodels-WP_M1-WP_parameter_g_no_label_1.why"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
......@@ -120,11 +98,11 @@
shape="ainfix &lt;=ainfix +V0c3c50Iainfix &gt;=V0c42F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
......@@ -137,11 +115,11 @@
shape="ainfix &lt;=ainfix +V0c3c50Iainfix &gt;=V0c42F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
......@@ -154,28 +132,28 @@
shape="ainfix &lt;=ainfix +V0c3c50Iainfix &gt;=V0c42F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="g2_lab"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="16" loccnumb="7" loccnume="13"
sum="37fc380c22d847902ef0134ccfd8f656"
sum="3eba6df3534bc325081d7e9f0bf07e60"
proved="false"
expanded="true"
shape="ainfix &gt;=axV0F">
shape="ainfix &gt;=agV0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
......@@ -195,7 +173,7 @@
shape="ainfix &lt;V0c1Aainfix &lt;c0V0NF">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
......@@ -212,212 +190,229 @@
shape="ainfix &lt;=V0c1Aainfix &lt;=c0V0NF">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test2"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="31" loccnumb="5" loccnume="10"
sum="8f22d32b4d3abb09a850b419749f7c47"
sum="5e6dca613e5db62a2fdf2660ff535582"
proved="false"
expanded="true"
shape="ainfix =adivV0V0c1F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test_overflow"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="33" loccnumb="5" loccnume="18"
sum="8d26f2c25b69efd849617e699a7319ef"
sum="5d70de2b9f923a914310574254fad74c"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=c0ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=c0V1Aainfix &lt;=V0c65535Aainfix &lt;=c0V0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test_overflow2"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="37" loccnumb="5" loccnume="19"
sum="0f56ea71245d1f6a62700fa6bce1db36"
sum="f28b1eb3470cc50ea0c3650f107aab27"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=aprefix -c2ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=aprefix -c2V1Aainfix &lt;=V0c65535Aainfix &lt;=aprefix -c2V0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test_overflow_int16"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="43" loccnumb="5" loccnume="24"
sum="927286ccd54988f36d1dab791dafd515"
sum="f4e36e34b57f8458e7eb85dcd46be19d"
proved="false"
expanded="true"
shape="ais_int16ainfix +V0V1Iais_int16V1Aais_int16V0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="test_overflow_int16_alt"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="47" loccnumb="5" loccnume="28"
sum="bef9b5b701386cd82fede1553fe0c77a"
sum="bafb05d844a12e49d8d4e4837e79bde9"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix +V0V1c65535Aainfix &lt;=aprefix -c65536ainfix +V0V1Iainfix &lt;=V1c65535Aainfix &lt;=aprefix -c65536V1Aainfix &lt;=V0c65535Aainfix &lt;=aprefix -c65536V0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test_overflow_int16_bis"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="51" loccnumb="5" loccnume="28"
sum="ca168cfbbc15d3fca583ea1ec2e44550"
sum="7a83759f576461a70e4afa006e71c6b7"
proved="false"
expanded="true"
shape="ais_int16ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aais_int16V1Aais_int16V0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test_overflow_int32"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="57" loccnumb="5" loccnume="24"
sum="fa55a6e7efaa43cdd22cabdf66f49443"
loclnum="58" loccnumb="5" loccnume="24"
sum="c158b0c5a8c2a1438c120ee61ebfbbf9"
proved="false"
expanded="true"
shape="ais_int32ainfix +V0V1Iais_int32V1Aais_int32V0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test_overflow_int32_bis"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="61" loccnumb="5" loccnume="28"
sum="2f6bae3db74a9de9ef6b4d0ddebf25ee"
loclnum="62" loccnumb="5" loccnume="28"
sum="13278d5c6d1dc5f97c0ad379062d2771"
proved="false"
expanded="true"
shape="ais_int32ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aais_int32V1Aais_int32V0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test_overflow_int32_bis_inline"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="66" loccnumb="5" loccnume="35"
sum="f1f6b030b87db2b3aab57752ffac373f"
proved="false"
expanded="false"
shape="ainfix &lt;=ainfix +V0V1c2147483647Aainfix &lt;=aprefix -c2147483648ainfix +V0V1Iainfix &lt;=V0V1Aainfix &lt;=c0V0Aainfix &lt;=V1c2147483647Aainfix &lt;=aprefix -c2147483648V1Aainfix &lt;=V0c2147483647Aainfix &lt;=aprefix -c2147483648V0F">
<proof
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="ModelReal"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="67" loccnumb="7" loccnume="16"
loclnum="72" loccnumb="7" loccnume="16"
verified="false"
expanded="true">
<goal
name="test1"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="71" loccnumb="5" loccnume="10"
loclnum="76" loccnumb="5" loccnume="10"
sum="eca61bb8da58aab53b390824efa6096c"
proved="false"
expanded="true"
shape="ainfix &lt;V0c1.0Aainfix &lt;c0.0V0NF">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="test2"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="73" loccnumb="5" loccnume="10"
loclnum="78" loccnumb="5" loccnume="10"
sum="1db3567ffd1099c47db86de68de8b9ce"
proved="false"
expanded="true"
shape="ainfix =ainfix /V0V0c1.0F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.03"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="ModelArray"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="77" loccnumb="7" loccnume="17"
loclnum="82" loccnumb="7" loccnume="17"
verified="false"
expanded="true">
<goal
name="t1"
locfile="alt-ergo-models/../alt-ergo-models.why"
loclnum="81" loccnumb="5" loccnume="7"
loclnum="86" loccnumb="5" loccnume="7"
sum="80ac2844addd3bc5d617d1bfe18cfa0f"
proved="false"
expanded="true"
shape="ainfix =agetasetV0c0c42V1agetV0V1F">
<proof
prover="0"
timelimit="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
......
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