Commit c9c143de authored by Andrei Paskevich's avatar Andrei Paskevich

update sessions

parent 7e80633b
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
......@@ -127,10 +127,10 @@
locfile="../resizable_array.mlw"
loclnum="87" loccnumb="6" loccnume="11"
expl="parameter test1"
sum="8ade502ea19d0945fbdf4c25f66bb53d"
sum="39b366ac29ac2ff9a6fe4b93707fd17d"
proved="true"
expanded="true"
shape="ainfix =CV0amk rarrayVVV4c7Aainfix =agetCV0amk rarrayVVV3c0c17Iainfix =agetCV0amk rarrayVVV3V9agetCV0amk rarrayVVCV13amk arrayVVV1V9Iainfix &lt;V9aminCV0amk rarrayVVV16c7Aainfix &lt;=c0V9FAainfix =CV0amk rarrayVVV4c7ACV0amk rarrayVVtACV0amk rarrayVVainfix &lt;=V4V2Aainfix &lt;=c0V4FAainfix &lt;=c0c7ACV0amk rarrayVVtICV0amk rarrayVVCV27amk arrayVVainfix =asetaeltsadataV0c0c17V1Aainfix =alengthadataV0V28Aainfix =alengthV0V26ACV0amk rarrayVVtACV0amk rarrayVVainfix &lt;=V32CV33amk arrayVVV34Aainfix &lt;=c0V32FAainfix &lt;c0alengthV0Aainfix &lt;=c0c0ACV0amk rarrayVVtAainfix =alengthV0c10ICV0amk rarrayVVtACV0amk rarrayVVainfix &lt;=V40alengthV41Aainfix &lt;=c0V40Lamakec10Aainfix &lt;=c0c10">
shape="ainfix =CV0amk rarrayVVV4c7Aainfix =agetCV0amk rarrayVVV3c0c17Iainfix =agetCV0amk rarrayVVV3V9agetCV0amk rarrayVVCV13amk arrayVVV1V9Iainfix &lt;V9aminCV0amk rarrayVVV16c7Aainfix &lt;=c0V9FAainfix =CV0amk rarrayVVV4c7ACV0amk rarrayVVtAainfix &lt;=CV0amk rarrayVVV4CV0amk rarrayVVV2Aainfix &lt;=c0CV0amk rarrayVVV4FAainfix &lt;=c0c7ACV0amk rarrayVVtICV0amk rarrayVVCV31amk arrayVVainfix =asetaeltsadataV0c0c17V1Aainfix =alengthadataV0V32Aainfix =alengthV0V30ACV0amk rarrayVVtAainfix &lt;=CV0amk rarrayVVV36CV0amk rarrayVVCV39amk arrayVVV40Aainfix &lt;=c0CV0amk rarrayVVV42FAainfix &lt;c0alengthV0Aainfix &lt;=c0c0ACV0amk rarrayVVtAainfix =alengthV0c10ICV0amk rarrayVVtAainfix &lt;=alengthV0alengthadataV0Aainfix &lt;=c0alengthV0Lamakec10Aainfix &lt;=c0c10">
<label
name="expl:parameter test1"/>
<proof
......@@ -147,10 +147,10 @@
locfile="../resizable_array.mlw"
loclnum="95" loccnumb="6" loccnume="11"
expl="parameter test2"
sum="f33c8620c5ce189d02b4f28c0934ba8e"
sum="7746498221775373ce71b78b761288d1"
proved="true"
expanded="true"
shape="ainfix =agetCV2amk rarrayVVCV8amk arrayVVV3c0c42Aainfix &lt;c0CV2amk rarrayVVV11Aainfix &lt;=c0c0ACV2amk rarrayVVtAainfix =agetCV0amk rarrayVVV5c10c42Aainfix &lt;c10CV0amk rarrayVVV6Aainfix &lt;=c0c10ACV0amk rarrayVVtAainfix =agetCV0amk rarrayVVV5c0c17Aainfix =CV0amk rarrayVVV6c20Iainfix =agetCV0amk rarrayVVV5V25agetCV2amk rarrayVVCV29amk arrayVVV3ainfix -V25CV0amk rarrayVVV32Iainfix &lt;=CV0amk rarrayVVV34V25Aainfix =agetCV0amk rarrayVVV5V25agetCV0amk rarrayVVCV39amk arrayVVV1V25Iainfix &lt;V25CV0amk rarrayVVV42Iainfix &lt;V25CV0amk rarrayVVV6Aainfix &lt;=c0V25FAainfix =CV0amk rarrayVVV6ainfix +CV0amk rarrayVVV48CV2amk rarrayVVV50ACV0amk rarrayVVtACV0amk rarrayVVainfix &lt;=V6V4Aainfix &lt;=c0V6FACV2amk rarrayVVtACV0amk rarrayVVtICV2amk rarrayVVCV61amk arrayVVainfix =asetaeltsadataV2c0c42V3Aainfix =alengthadataV2V62Aainfix =alengthV2V60ACV2amk rarrayVVtACV2amk rarrayVVainfix &lt;=V66CV67amk arrayVVV68Aainfix &lt;=c0V66FAainfix &lt;c0alengthV2Aainfix &lt;=c0c0ACV2amk rarrayVVtICV2amk rarrayVVtACV2amk rarrayVVainfix &lt;=V74alengthV75Aainfix &lt;=c0V74Lamakec10Aainfix &lt;=c0c10ICV0amk rarrayVVCV77amk arrayVVainfix =asetaeltsadataV0c0c17V1Aainfix =alengthadataV0V78Aainfix =alengthV0V76ACV0amk rarrayVVtACV0amk rarrayVVainfix &lt;=V82CV83amk arrayVVV84Aainfix &lt;=c0V82FAainfix &lt;c0alengthV0Aainfix &lt;=c0c0ACV0amk rarrayVVtICV0amk rarrayVVtACV0amk rarrayVVainfix &lt;=V90alengthV91Aainfix &lt;=c0V90Lamakec10Aainfix &lt;=c0c10">
shape="ainfix =agetCV2amk rarrayVVCV8amk arrayVVV3c0c42Aainfix &lt;c0CV2amk rarrayVVV11Aainfix &lt;=c0c0ACV2amk rarrayVVtAainfix =agetCV0amk rarrayVVV5c10c42Aainfix &lt;c10CV0amk rarrayVVV6Aainfix &lt;=c0c10ACV0amk rarrayVVtAainfix =agetCV0amk rarrayVVV5c0c17Aainfix =CV0amk rarrayVVV6c20Iainfix =agetCV0amk rarrayVVV5V25agetCV2amk rarrayVVCV29amk arrayVVV3ainfix -V25CV0amk rarrayVVV32Iainfix &lt;=CV0amk rarrayVVV34V25Aainfix =agetCV0amk rarrayVVV5V25agetCV0amk rarrayVVCV39amk arrayVVV1V25Iainfix &lt;V25CV0amk rarrayVVV42Iainfix &lt;V25CV0amk rarrayVVV6Aainfix &lt;=c0V25FAainfix =CV0amk rarrayVVV6ainfix +CV0amk rarrayVVV48CV2amk rarrayVVV50ACV0amk rarrayVVtAainfix &lt;=CV0amk rarrayVVV6CV0amk rarrayVVV4Aainfix &lt;=c0CV0amk rarrayVVV6FACV2amk rarrayVVtACV0amk rarrayVVtICV2amk rarrayVVCV65amk arrayVVainfix =asetaeltsadataV2c0c42V3Aainfix =alengthadataV2V66Aainfix =alengthV2V64ACV2amk rarrayVVtAainfix &lt;=CV2amk rarrayVVV70CV2amk rarrayVVCV73amk arrayVVV74Aainfix &lt;=c0CV2amk rarrayVVV76FAainfix &lt;c0alengthV2Aainfix &lt;=c0c0ACV2amk rarrayVVtICV2amk rarrayVVtAainfix &lt;=alengthV2alengthadataV2Aainfix &lt;=c0alengthV2Lamakec10Aainfix &lt;=c0c10ICV0amk rarrayVVCV83amk arrayVVainfix =asetaeltsadataV0c0c17V1Aainfix =alengthadataV0V84Aainfix =alengthV0V82ACV0amk rarrayVVtAainfix &lt;=CV0amk rarrayVVV88CV0amk rarrayVVCV91amk arrayVVV92Aainfix &lt;=c0CV0amk rarrayVVV94FAainfix &lt;c0alengthV0Aainfix &lt;=c0c0ACV0amk rarrayVVtICV0amk rarrayVVtAainfix &lt;=alengthV0alengthadataV0Aainfix &lt;=c0alengthV0Lamakec10Aainfix &lt;=c0c10">
<label
name="expl:parameter test2"/>
<proof
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
......@@ -419,10 +419,10 @@
locfile="../snapshotable_trees.mlw"
loclnum="157" loccnumb="6" loccnume="14"
expl="type invariant"
sum="8d8112f215fcb392403ede56f480046c"
sum="21fa764199c221ebb266476ca62df8b3"
proved="true"
expanded="false"
shape="t">
shape="abstV0IabstV0F">
<label
name="expl:parameter snapshot"/>
<proof
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
......@@ -20,10 +20,10 @@
locfile="../vstte10_aqueue.mlw"
loclnum="21" loccnumb="6" loccnume="11"
expl="parameter empty"
sum="f148b224bef0491026c5971839eb52c1"
sum="aea875c423b224787143908f6ec83ec2"
proved="true"
expanded="false"
shape="ainfix =ainfix ++aNilareverseaNilaNilAainfix =alengthV0c0Aainfix &gt;=c0alengthV0Aainfix =alengthaNilc0LaNil">
shape="ainfix =ainfix ++aNilareverseaNilaNilAainfix =alengthaNilc0Aainfix &gt;=c0alengthaNilAainfix =alengthaNilc0">
<label
name="expl:parameter empty"/>
<proof
......@@ -60,10 +60,10 @@
locfile="../vstte10_aqueue.mlw"
loclnum="32" loccnumb="6" loccnume="12"
expl="parameter create"
sum="105c38020da8b68175e86c584c7b3c0c"
sum="653d92fe520fa8b672e0d4cb3a2a30c4"
proved="true"
expanded="false"
shape="iainfix &gt;=V1V3ainfix =ainfix ++V0areverseV2ainfix ++V0areverseV2Aainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1ainfix =ainfix ++ainfix ++V0areverseV2areverseaNilainfix ++V0areverseV2Aainfix =alengthV5c0Aainfix &gt;=V4alengthV5Aainfix =alengthainfix ++V0areverseV2V4LaNilLainfix +V1V3Iainfix =V3alengthV2Aainfix =V1alengthV0F">
shape="iainfix &gt;=V1V3ainfix =ainfix ++V0areverseV2ainfix ++V0areverseV2Aainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1ainfix =ainfix ++ainfix ++V0areverseV2areverseaNilainfix ++V0areverseV2Aainfix =alengthaNilc0Aainfix &gt;=ainfix +V1V3alengthaNilAainfix =alengthainfix ++V0areverseV2ainfix +V1V3Iainfix =V3alengthV2Aainfix =V1alengthV0F">
<label
name="expl:parameter create"/>
<proof
......
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