updated DTD of sessions

Makefile.in

@@ -501,6 +501,17 @@ gallery::
 	  cd ../..; \
 	done
 
+########
+# XML DTD validation
+########
+
+.PHONY: xml-validate
+
+xml-validate:
+	@for x in `find examples/ -name why3session.xml`; do \
+	  xmllint --noout --valid $$x 2>&1 | head -1; \
+	done
+
 ########
 # Config
 ########

examples/bts/12475/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="bts/12475/why3session.xml">
+ name="./bts/12475/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -24,16 +24,15 @@
   expanded="false">
   <theory
    name="Stmt"
-   locfile="bts/12475/../12475.why"
+   locfile="./bts/12475/../12475.why"
    loclnum="1" loccnumb="7" loccnume="11"
    verified="true"
    expanded="true">
    <label
-    name="some_statement">
-    </label>
+    name="some_statement"/>
    <goal
     name="toto"
-    locfile="bts/12475/../12475.why"
+    locfile="./bts/12475/../12475.why"
     loclnum="6" loccnumb="7" loccnume="11"
     sum="bef94593fc244d7e427d59e3543a820b"
     proved="true"

examples/bts/12934/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="bts/12934/why3session.xml">
+ name="./bts/12934/why3session.xml">
  <prover
   id="0"
   name="Coq"
@@ -12,13 +12,13 @@
   expanded="false">
   <theory
    name="BTS12934"
-   locfile="bts/12934/../12934.why"
+   locfile="./bts/12934/../12934.why"
    loclnum="2" loccnumb="7" loccnume="15"
    verified="true"
    expanded="true">
    <goal
     name="t"
-    locfile="bts/12934/../12934.why"
+    locfile="./bts/12934/../12934.why"
     loclnum="8" loccnumb="7" loccnume="8"
     sum="9432f4497e1405d3077c8e5e4666a0fa"
     proved="true"

examples/bts/13849/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="bts/13849/why3session.xml">
+ name="./bts/13849/why3session.xml">
  <prover
   id="0"
   name="Coq"
@@ -12,13 +12,13 @@
   expanded="false">
   <theory
    name="T"
-   locfile="bts/13849/../13849.why"
+   locfile="./bts/13849/../13849.why"
    loclnum="4" loccnumb="7" loccnume="8"
    verified="true"
    expanded="true">
    <goal
     name="x"
-    locfile="bts/13849/../13849.why"
+    locfile="./bts/13849/../13849.why"
     loclnum="19" loccnumb="6" loccnume="7"
     sum="f9dfa1ef69ac351dd3f83658b2409a0d"
     proved="true"

examples/bts/13853/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="bts/13853/why3session.xml">
+ name="./bts/13853/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -12,13 +12,13 @@
   expanded="false">
   <theory
    name="WP T"
-   locfile="bts/13853/../13853.mlw"
+   locfile="./bts/13853/../13853.mlw"
    loclnum="10" loccnumb="7" loccnume="8"
    verified="true"
    expanded="true">
    <goal
     name="WP_parameter f"
-    locfile="bts/13853/../13853.mlw"
+    locfile="./bts/13853/../13853.mlw"
     loclnum="16" loccnumb="8" loccnume="9"
     expl="exceptional postcondition"
     sum="b94bdf7e8e0d350ccc769aa2abfed2a5"
@@ -26,8 +26,7 @@
     expanded="false"
     shape="t">
     <label
-     name="expl:parameter f">
-     </label>
+     name="expl:parameter f"/>
     <proof
      prover="0"
      timelimit="10"
@@ -38,7 +37,7 @@
    </goal>
    <goal
     name="WP_parameter g"
-    locfile="bts/13853/../13853.mlw"
+    locfile="./bts/13853/../13853.mlw"
     loclnum="18" loccnumb="7" loccnume="8"
     expl="exceptional postcondition"
     sum="290f50192a8d9eb5fed96206ef53b3b4"
@@ -46,8 +45,7 @@
     expanded="false"
     shape="t">
     <label
-     name="expl:parameter g">
-     </label>
+     name="expl:parameter g"/>
     <proof
      prover="0"
      timelimit="10"

examples/bts/13854/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="bts/13854/why3session.xml">
+ name="./bts/13854/why3session.xml">
  <prover
   id="0"
   name="Coq"
@@ -12,13 +12,13 @@
   expanded="false">
   <theory
    name="T"
-   locfile="bts/13854/../13854.why"
+   locfile="./bts/13854/../13854.why"
    loclnum="1" loccnumb="7" loccnume="8"
    verified="true"
    expanded="true">
    <goal
     name="g"
-    locfile="bts/13854/../13854.why"
+    locfile="./bts/13854/../13854.why"
     loclnum="6" loccnumb="7" loccnume="8"
     sum="0fd57a4666fe36603f9625e61ed1a171"
     proved="true"
@@ -35,7 +35,7 @@
    </goal>
    <goal
     name="x"
-    locfile="bts/13854/../13854.why"
+    locfile="./bts/13854/../13854.why"
     loclnum="8" loccnumb="7" loccnume="8"
     sum="c90085b1cee92272eb0fef6707c9b64e"
     proved="true"

examples/check-builtin/ac/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="check-builtin/ac/why3session.xml">
+ name="./check-builtin/ac/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -24,13 +24,13 @@
   expanded="false">
   <theory
    name="Test"
-   locfile="check-builtin/ac/../ac.why"
+   locfile="./check-builtin/ac/../ac.why"
    loclnum="1" loccnumb="7" loccnume="11"
    verified="true"
    expanded="true">
    <goal
     name="G1"
-    locfile="check-builtin/ac/../ac.why"
+    locfile="./check-builtin/ac/../ac.why"
     loclnum="5" loccnumb="12" loccnume="14"
     sum="1407925033bf3e71a98c24f86b8de2f8"
     proved="true"
@@ -67,7 +67,7 @@
    </goal>
    <goal
     name="G2"
-    locfile="check-builtin/ac/../ac.why"
+    locfile="./check-builtin/ac/../ac.why"
     loclnum="6" loccnumb="12" loccnume="14"
     sum="d3e5051a2fd2b6f6b99aab05848f7c06"
     proved="true"

examples/check-builtin/array/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="check-builtin/array/why3session.xml">
+ name="./check-builtin/array/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -24,13 +24,13 @@
   expanded="false">
   <theory
    name="Test_simplify_array"
-   locfile="check-builtin/array/../array.why"
+   locfile="./check-builtin/array/../array.why"
    loclnum="1" loccnumb="7" loccnume="26"
    verified="true"
    expanded="true">
    <goal
     name="G1"
-    locfile="check-builtin/array/../array.why"
+    locfile="./check-builtin/array/../array.why"
     loclnum="4" loccnumb="7" loccnume="9"
     sum="4b45d6270f4a53daefb6fce54b8ebff7"
     proved="true"
@@ -67,7 +67,7 @@
    </goal>
    <goal
     name="G2"
-    locfile="check-builtin/array/../array.why"
+    locfile="./check-builtin/array/../array.why"
     loclnum="6" loccnumb="7" loccnume="9"
     sum="6ccca0aeacb41ec5118c79435eb055a1"
     proved="true"
@@ -104,7 +104,7 @@
    </goal>
    <goal
     name="G3"
-    locfile="check-builtin/array/../array.why"
+    locfile="./check-builtin/array/../array.why"
     loclnum="10" loccnumb="7" loccnume="9"
     sum="6108a9e01a2539ed185406b5ade7ca86"
     proved="true"
@@ -141,7 +141,7 @@
    </goal>
    <goal
     name="G4"
-    locfile="check-builtin/array/../array.why"
+    locfile="./check-builtin/array/../array.why"
     loclnum="13" loccnumb="7" loccnume="9"
     sum="34fa3208c06f03a03e0897d791b6fa13"
     proved="true"

examples/check-builtin/bool/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="check-builtin/bool/why3session.xml">
+ name="./check-builtin/bool/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -24,13 +24,13 @@
   expanded="false">
   <theory
    name="Test"
-   locfile="check-builtin/bool/../bool.why"
+   locfile="./check-builtin/bool/../bool.why"
    loclnum="1" loccnumb="7" loccnume="11"
    verified="true"
    expanded="true">
    <goal
     name="G1"
-    locfile="check-builtin/bool/../bool.why"
+    locfile="./check-builtin/bool/../bool.why"
     loclnum="4" loccnumb="11" loccnume="13"
     sum="ca83f9c0bba83999ea519362a0f979d3"
     proved="true"
@@ -67,7 +67,7 @@
    </goal>
    <goal
     name="G2"
-    locfile="check-builtin/bool/../bool.why"
+    locfile="./check-builtin/bool/../bool.why"
     loclnum="5" loccnumb="11" loccnume="13"
     sum="5f38ad601b7696e2fe3ba2f557f615e0"
     proved="true"
@@ -104,7 +104,7 @@
    </goal>
    <goal
     name="G3"
-    locfile="check-builtin/bool/../bool.why"
+    locfile="./check-builtin/bool/../bool.why"
     loclnum="6" loccnumb="11" loccnume="13"
     sum="0787a194d06b1338870206245188cc68"
     proved="true"

examples/check-builtin/euclideandivision/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="check-builtin/euclideandivision/why3session.xml">
+ name="./check-builtin/euclideandivision/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -24,13 +24,13 @@
   expanded="false">
   <theory
    name="Test"
-   locfile="check-builtin/euclideandivision/../euclideandivision.why"
+   locfile="./check-builtin/euclideandivision/../euclideandivision.why"
    loclnum="1" loccnumb="7" loccnume="11"
    verified="true"
    expanded="true">
    <goal
     name="G1"
-    locfile="check-builtin/euclideandivision/../euclideandivision.why"
+    locfile="./check-builtin/euclideandivision/../euclideandivision.why"
     loclnum="3" loccnumb="12" loccnume="14"
     sum="c9dce8acf8d17f8bb9290708121a5df2"
     proved="true"
@@ -67,7 +67,7 @@
    </goal>
    <goal
     name="G2"
-    locfile="check-builtin/euclideandivision/../euclideandivision.why"
+    locfile="./check-builtin/euclideandivision/../euclideandivision.why"
     loclnum="4" loccnumb="12" loccnume="14"
     sum="24ab638db2f4cd2b0ad27a15918707d1"
     proved="true"

examples/check-builtin/floats/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="check-builtin/floats/why3session.xml">
+ name="./check-builtin/floats/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -24,13 +24,13 @@
   expanded="false">
   <theory
    name="TestGappa"
-   locfile="check-builtin/floats/../floats.why"
+   locfile="./check-builtin/floats/../floats.why"
    loclnum="2" loccnumb="7" loccnume="16"
    verified="true"
    expanded="true">
    <goal
     name="Round_single_01"
-    locfile="check-builtin/floats/../floats.why"
+    locfile="./check-builtin/floats/../floats.why"
     loclnum="11" loccnumb="7" loccnume="22"
     sum="573c0411296e0cd6234d1297e8b577c1"
     proved="true"
@@ -46,7 +46,7 @@
    </goal>
    <goal
     name="Round_double_01"
-    locfile="check-builtin/floats/../floats.why"
+    locfile="./check-builtin/floats/../floats.why"
     loclnum="14" loccnumb="7" loccnume="22"
     sum="5a42446f594a536207f1c027b72d61b8"
     proved="true"
@@ -62,7 +62,7 @@
    </goal>
    <goal
     name="Test00"
-    locfile="check-builtin/floats/../floats.why"
+    locfile="./check-builtin/floats/../floats.why"
     loclnum="17" loccnumb="8" loccnume="14"
     sum="44e3f9d032bf5fc4ad04532da6e3bb0f"
     proved="true"
@@ -99,7 +99,7 @@
    </goal>
    <goal
     name="Test01"
-    locfile="check-builtin/floats/../floats.why"
+    locfile="./check-builtin/floats/../floats.why"
     loclnum="19" loccnumb="8" loccnume="14"
     sum="6440deaa9c1e9cc1a060d2a89682f3a6"
     proved="true"
@@ -115,7 +115,7 @@
    </goal>
    <goal
     name="Test02"
-    locfile="check-builtin/floats/../floats.why"
+    locfile="./check-builtin/floats/../floats.why"
     loclnum="25" loccnumb="8" loccnume="14"
     sum="bb80fe9c2379b43f0811b9d6bef035dc"
     proved="true"
@@ -131,7 +131,7 @@
    </goal>
    <goal
     name="Test03"
-    locfile="check-builtin/floats/../floats.why"
+    locfile="./check-builtin/floats/../floats.why"
     loclnum="32" loccnumb="8" loccnume="14"
     sum="fc3b0598d700e955653b407c87d29fda"
     proved="true"

examples/check-builtin/int/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="check-builtin/int/why3session.xml">
+ name="./check-builtin/int/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -24,13 +24,13 @@
   expanded="false">
   <theory
    name="Test"
-   locfile="check-builtin/int/../int.why"
+   locfile="./check-builtin/int/../int.why"
    loclnum="1" loccnumb="7" loccnume="11"
    verified="true"
    expanded="true">
    <goal
     name="G1"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="3" loccnumb="7" loccnume="9"
     sum="899a24cba5a3807f5638a16c2915002b"
     proved="true"
@@ -67,7 +67,7 @@
    </goal>
    <goal
     name="G2"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="4" loccnumb="7" loccnume="9"
     sum="15fea215e0e38f93607b4c66cdf45712"
     proved="true"
@@ -104,7 +104,7 @@
    </goal>
    <goal
     name="CompatOrderAdd"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="6" loccnumb="7" loccnume="21"
     sum="1b02d100b4d433ff30662e69e3b9a17b"
     proved="true"
@@ -141,7 +141,7 @@
    </goal>
    <goal
     name="CompatOrderMult"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="7" loccnumb="7" loccnume="22"
     sum="7a34aecb05d3edc2b9ec4c9d5d672ce1"
     proved="true"
@@ -178,7 +178,7 @@
    </goal>
    <goal
     name="InvMult"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="9" loccnumb="7" loccnume="14"
     sum="2c3e1f709768ff692a56f392c66c8d6b"
     proved="true"
@@ -215,7 +215,7 @@
    </goal>
    <goal
     name="InvSquare"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="10" loccnumb="7" loccnume="16"
     sum="65639547594360d52d18d4f1f673482a"
     proved="true"
@@ -252,7 +252,7 @@
    </goal>
    <goal
     name="ZeroMult"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="11" loccnumb="7" loccnume="15"
     sum="3ad2b227ce15783b5d94003f4f806a91"
     proved="true"
@@ -289,7 +289,7 @@
    </goal>
    <goal
     name="SquareNonNeg1"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="12" loccnumb="7" loccnume="20"
     sum="3a1830da7c435b4a368232b4378a9bb9"
     proved="true"
@@ -326,7 +326,7 @@
    </goal>
    <goal
     name="SquareNonNeg"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="13" loccnumb="7" loccnume="19"
     sum="22a3331ee0912a82bdc49173fb9adbdf"
     proved="true"
@@ -363,7 +363,7 @@
    </goal>
    <goal
     name="ZeroLessOne"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="14" loccnumb="7" loccnume="18"
     sum="6604e319a9bbef2cd14445ca8d994b6f"
     proved="true"
@@ -401,13 +401,13 @@
   </theory>
   <theory
    name="MinMax"
-   locfile="check-builtin/int/../int.why"
+   locfile="./check-builtin/int/../int.why"
    loclnum="17" loccnumb="7" loccnume="13"
    verified="true"
    expanded="true">
    <goal
     name="G"
-    locfile="check-builtin/int/../int.why"
+    locfile="./check-builtin/int/../int.why"
     loclnum="20" loccnumb="7" loccnume="8"
     sum="643339a43f3afaa85a6ac97651acc476"
     proved="true"

examples/check-builtin/intreal/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
 <why3session
- name="check-builtin/intreal/why3session.xml">
+ name="./check-builtin/intreal/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -44,13 +44,13 @@
   expanded="false">
   <theory
    name="IntReal"
-   locfile="check-builtin/intreal/../intreal.why"
+   locfile="./check-builtin/intreal/../intreal.why"
    loclnum="2" loccnumb="7" loccnume="14"
    verified="true"
    expanded="true">
    <goal
     name="G1"
-    locfile="check-builtin/intreal/../intreal.why"
+    locfile="./check-builtin/intreal/../intreal.why"
     loclnum="8" loccnumb="7" loccnume="9"
     sum="a3dff87b8d8fedb505c6359dde79722f"
     proved="true"
@@ -108,7 +108,7 @@
    </goal>
    <goal
     name="G2"
-    locfile="check-builtin/intreal/../intreal.why"
+    locfile="./check-builtin/intreal/../intreal.why"
     loclnum="9" loccnumb="7" loccnume="9"
     sum="d4b897b0551e058df4a9a889d20d247c"
     proved="true"
@@ -152,7 +152,7 @@
    </goal>
    <goal
     name="G3"
-    locfile="check-builtin/intreal/../intreal.why"
+    locfile="./check-builtin/intreal/../intreal.why"
     loclnum="10" loccnumb="7" loccnume="9"
     sum="92820ed54136bf4354490d405f16c848"
     proved="true"
@@ -196,7 +196,7 @@
    </goal>
    <goal
     name="G4"
-    locfile="check-builtin/intreal/../intreal.why"
+    locfile="./check-builtin/intreal/../intreal.why"
     loclnum="11" loccnumb="7" loccnume="9"
     sum="b7c53145c92254d781ba372f7a4a128b"
     proved="true"
@@ -247,7 +247,7 @@
    </goal>
    <goal
     name="G5"
-    locfile="check-builtin/intreal/../intreal.why"
+    locfile="./check-builtin/intreal/../intreal.why"
     loclnum="12" loccnumb="7" loccnume="9"
     sum="87b623f4677e9fef5a35fc06bd420bc8"
     proved="true"
@@ -291,7 +291,7 @@
    </goal>
    <goal
     name="G6"
-    locfile="check-builtin/intreal/../intreal.why"
+    locfile="./check-builtin/intreal/../intreal.why"
     loclnum="13" loccnumb="7" loccnume="9"
     sum="d3a0d063178687050ff7243e9938885c"
     proved="true"
@@ -349,7 +349,7 @@
    </goal>
    <goal
     name="G7"