Commit bea0483f authored by MARCHE Claude's avatar MARCHE Claude

added Tuyen's example in regtests

parent afd870e2
......@@ -47,18 +47,12 @@ why3.conf
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3realize.byte
/bin/why3realize.opt
/bin/why3realize
/bin/why3ml.byte
/bin/why3ml.opt
/bin/why3ml
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
/bin/why3gui.byte
/bin/why3gui.opt
/bin/why3gui
/bin/why3-cpulimit
/bin/why3-cpulimit.exe
/bin/why3config.byte
......@@ -145,9 +139,6 @@ why3.conf
/src/parser/parser.mli
/src/parser/parser.output
# /src/ide/
/src/ide/xml.ml
# /src/why3doc/
/src/why3doc/doc_lexer.ml
......
......@@ -39,7 +39,7 @@
locfile="power2/../power2.why"
loclnum="1" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
expanded="false">
<goal
name="Power_1"
locfile="power2/../power2.why"
......@@ -3461,7 +3461,7 @@
loclnum="103" loccnumb="8" loccnume="26"
sum="742640b78c6f8972a42743290fdb56c5"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =apow2V0c0.0NIainfix &gt;=V0c0F">
<proof
prover="5"
......@@ -3518,7 +3518,7 @@
loclnum="105" loccnumb="8" loccnume="21"
sum="2cbd515615e025e022da59b7fe3978d4"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =apow2aprefix -V0ainfix /.c1.0apow2V0Iainfix &gt;=V0c0F">
<proof
prover="5"
......@@ -3528,14 +3528,6 @@
archived="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="5"
......@@ -3544,14 +3536,6 @@
archived="false">
<result status="timeout" time="5.13"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="failure" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
......@@ -3575,7 +3559,7 @@
loclnum="107" loccnumb="8" loccnume="22"
sum="e76a0e7bb90eb5890c701551fc6bc41c"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =apow2V0c0.0NF">
<proof
prover="5"
......@@ -3657,7 +3641,7 @@
loclnum="111" loccnumb="8" loccnume="21"
sum="f172c7e0f52f667bb7b9c8653216ef40"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =apow2ainfix +V0V1ainfix *.apow2V0apow2V1Iainfix &gt;=V1c0F">
<proof
prover="5"
......@@ -3667,14 +3651,6 @@
archived="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="5"
......@@ -3683,14 +3659,6 @@
archived="false">
<result status="timeout" time="5.14"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="failure" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
......@@ -3714,7 +3682,7 @@
loclnum="113" loccnumb="8" loccnume="17"
sum="763c6533a99370f6102384b6bb2768d3"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =apow2ainfix +V0V1ainfix *.apow2V0apow2V1F">
<proof
prover="5"
......@@ -3724,14 +3692,6 @@
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="5"
......@@ -3740,14 +3700,6 @@
archived="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="failure" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
......@@ -3771,7 +3723,7 @@
loclnum="118" loccnumb="8" loccnume="21"
sum="514327c3c11c2e923c55fc4ee15c6412"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =apow2V0afrom_intapow2V0Iainfix &gt;=V0c0F">
<proof
prover="5"
......@@ -3781,14 +3733,6 @@
archived="false">
<result status="timeout" time="5.13"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="failure" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
......@@ -3797,14 +3741,6 @@
archived="false">
<result status="timeout" time="5.44"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="failure" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
......
......@@ -48,10 +48,19 @@ run_dir () {
done
}
echo "=== Logic ==="
run_dir .
echo ""
echo "=== Tests Provers ==="
run_dir tests-provers
echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
echo "=== BTS ==="
run_dir bts
echo ""
......@@ -63,10 +72,7 @@ echo ""
echo "=== Programs in their own subdir ==="
run_dir programs/vacid_0_binary_heaps "-I programs/vacid_0_binary_heaps"
run_dir hoare_logic "-I hoare_logic"
echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
run_dir bitvectors "-I bitvectors"
echo ""
echo "Summary: $success/$total"
......
......@@ -38,5 +38,27 @@ theory TestGappa
end
theory GappaEq
use import real.Real
use import real.Abs
use import floating_point.Rounding
use import floating_point.Double
constant a : double
constant r : double
function f int : double
lemma Test1:
value r = round NearestTiesToEven 0.1 ->
a = r ->
abs (value a - 0.1) <= 0x1.p-53
lemma Test2:
value r = round NearestTiesToEven 0.1 ->
f 0 = r ->
abs (value (f 0) - 0.1) <= 0x1.p-53
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="gappa/why3session.xml">
<prover
id="0"
name="Gappa"
version="0.16.0"/>
<file
name="../gappa.why"
verified="true"
expanded="true">
<theory
name="TestGappa"
locfile="gappa/../gappa.why"
loclnum="2" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
<goal
name="Round_single_01"
locfile="gappa/../gappa.why"
loclnum="11" loccnumb="8" loccnume="23"
sum="573c0411296e0cd6234d1297e8b577c1"
proved="true"
expanded="false"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Round_double_01"
locfile="gappa/../gappa.why"
loclnum="14" loccnumb="8" loccnume="23"
sum="eaa3135990893cf76a4dbd2cf022e49f"
proved="true"
expanded="false"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test00"
locfile="gappa/../gappa.why"
loclnum="17" loccnumb="9" loccnume="15"
sum="cd7f01f2104c006abdb886ad2fc8750b"
proved="true"
expanded="false"
shape="ainfix &lt;=aprefix -c3.0V0Iainfix &lt;=aabsV0c2.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test01"
locfile="gappa/../gappa.why"
loclnum="19" loccnumb="9" loccnume="15"
sum="477fea058e6582dd0cd7f4c240c1b59d"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix &lt;=avalueV0c2.0Aainfix &lt;=aprefix -c2.0avalueV0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test02"
locfile="gappa/../gappa.why"
loclnum="25" loccnumb="9" loccnume="15"
sum="be878bbcd8a7071916db56887c40a03b"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix &lt;=aabsavalueV0c2.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test03"
locfile="gappa/../gappa.why"
loclnum="32" loccnumb="9" loccnume="15"
sum="1ee7edead5fb6bdddd992317a358694d"
proved="true"
expanded="false"
shape="ainfix &lt;=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c2.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="GappaEq"
locfile="gappa/../gappa.why"
loclnum="41" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
<goal
name="Test1"
locfile="gappa/../gappa.why"
loclnum="52" loccnumb="8" loccnume="13"
sum="345de352b19b61f5c2777a487b74b999"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -avalueaac0.1c0x1.p-53Iainfix =aaarIainfix =avalueararoundaNearestTiesToEvenc0.1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test2"
locfile="gappa/../gappa.why"
loclnum="57" loccnumb="8" loccnume="13"
sum="4a04f8e7c92503df80076b2020c48f89"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -avalueafc0c0.1c0x1.p-53Iainfix =afc0arIainfix =avalueararoundaNearestTiesToEvenc0.1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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