Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 2d4bf231 authored by MARCHE Claude's avatar MARCHE Claude

test gappa on terms with labels

parent c41a4218
......@@ -91,10 +91,7 @@ theory GappaEq2
goal G2 : forall q:double. q = result ->
value q - value q1 * value q2 <= 0x1.p-52
constant q : double
axiom H3 : q = result
goal G3 : value q - value q1 * value q2 <= 0x1.p-52
goal G3 : forall q:double. ("lab1" q) = result ->
value ("lab2" q) - value q1 * value q2 <= 0x1.p-52
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="tests-provers/gappa/why3session.xml">
name="gappa/why3session.xml">
<prover
id="0"
name="Gappa"
version="0.16.0"/>
<file
name="../gappa.why"
verified="false"
expanded="false">
verified="true"
expanded="true">
<theory
name="TestGappa"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="2" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
<goal
name="Round_single_01"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="11" loccnumb="8" loccnume="23"
sum="573c0411296e0cd6234d1297e8b577c1"
proved="true"
......@@ -35,7 +35,7 @@
</goal>
<goal
name="Round_double_01"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="14" loccnumb="8" loccnume="23"
sum="eaa3135990893cf76a4dbd2cf022e49f"
proved="true"
......@@ -52,7 +52,7 @@
</goal>
<goal
name="Test00"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="17" loccnumb="9" loccnume="15"
sum="cd7f01f2104c006abdb886ad2fc8750b"
proved="true"
......@@ -69,7 +69,7 @@
</goal>
<goal
name="Test01"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="19" loccnumb="9" loccnume="15"
sum="477fea058e6582dd0cd7f4c240c1b59d"
proved="true"
......@@ -86,7 +86,7 @@
</goal>
<goal
name="Test02"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="25" loccnumb="9" loccnume="15"
sum="be878bbcd8a7071916db56887c40a03b"
proved="true"
......@@ -103,7 +103,7 @@
</goal>
<goal
name="Test03"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="32" loccnumb="9" loccnume="15"
sum="1ee7edead5fb6bdddd992317a358694d"
proved="true"
......@@ -121,13 +121,13 @@
</theory>
<theory
name="GappaEq"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="41" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
<goal
name="Test1"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="53" loccnumb="8" loccnume="13"
sum="2fe71c9c60fb2a1dae0426af19a3174b"
proved="true"
......@@ -144,7 +144,7 @@
</goal>
<goal
name="Test2"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="58" loccnumb="8" loccnume="13"
sum="d480649bec039f956c05ad4bccfdf3b8"
proved="true"
......@@ -161,7 +161,7 @@
</goal>
<goal
name="Test3"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="63" loccnumb="8" loccnume="13"
sum="85e367570f184a60bfad8e958b16ad25"
proved="true"
......@@ -179,13 +179,13 @@
</theory>
<theory
name="GappaEq2"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="72" loccnumb="7" loccnume="15"
verified="false"
verified="true"
expanded="true">
<goal
name="G1"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="89" loccnumb="7" loccnume="9"
sum="10127df3703deb4dc62eee6dd0e08f8f"
proved="true"
......@@ -202,7 +202,7 @@
</goal>
<goal
name="G2"
locfile="tests-provers/gappa/../gappa.why"
locfile="gappa/../gappa.why"
loclnum="91" loccnumb="7" loccnume="9"
sum="584bf8809239d409f578d27a534924c5"
proved="true"
......@@ -219,19 +219,19 @@
</goal>
<goal
name="G3"
locfile="tests-provers/gappa/../gappa.why"
loclnum="98" loccnumb="7" loccnume="9"
sum="9469b135d544f3a9e1746b6492709b0f"
proved="false"
locfile="gappa/../gappa.why"
loclnum="94" loccnumb="7" loccnume="9"
sum="4cbf48d318e4ed7319e003e85af8d8b5"
proved="true"
expanded="true"
shape="ainfix &lt;=ainfix -avalueaqainfix *avalueaq1avalueaq2c0x1.p-52">
shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
<proof
prover="0"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="valid" 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