Commit d82953a2 authored by MARCHE Claude's avatar MARCHE Claude

explanation for absurd

parent 79f8a416
......@@ -106,10 +106,10 @@
locfile="../add_list.mlw"
loclnum="63" loccnumb="4" loccnume="7"
expl="VC for sum"
sum="3b3017f3af26037f138ec976b52d04a1"
sum="9a09cd5512c73c6f39d19ebad452bf9b"
proved="true"
expanded="true"
shape="CV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
shape="itCV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FfIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
<label
name="expl:VC for sum"/>
<proof
......
......@@ -35,10 +35,10 @@
locfile="../duplets.mlw"
loclnum="43" loccnumb="6" loccnume="12"
expl="VC for duplet"
sum="32ad34e7b21551c66269d489fd496405"
sum="1a6899210a0c444805408422aa8b679e"
proved="true"
expanded="true"
shape="ais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix &lt;V5V0Aainfix &lt;V4V5Aainfix &lt;V4ainfix +ainfix -V0c2c1Aainfix &lt;=c0V4FNAiCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix &lt;V11V0Aainfix &lt;V10V11Aainfix &lt;V10ainfix +V7c1Aainfix &lt;=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix &lt;V14V0Aainfix &lt;V13V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FIais_dupletV3V7V16NIainfix &lt;V16ainfix +ainfix -V0c1c1Aainfix &lt;V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =V19V17Aainfix =V18V7Fais_dupletV3V7V21NIainfix &lt;V21ainfix +V17c1Aainfix &lt;V7V21FAainfix &lt;V17V0Aainfix &lt;=c0V17Iais_dupletV3V7V22NIainfix &lt;V22V17Aainfix &lt;V7V22FIainfix &lt;=V17ainfix -V0c1Aainfix &lt;=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix &lt;V23ainfix +V7c1Aainfix &lt;V7V23FIainfix &lt;=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix &lt;V25V0Aainfix &lt;V24V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FIainfix &gt;ainfix +V7c1ainfix -V0c1LagetV2V7Aainfix &lt;V7V0Aainfix &lt;=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix &lt;V28V0Aainfix &lt;V27V28Aainfix &lt;V27V7Aainfix &lt;=c0V27FIainfix &lt;=V7ainfix -V0c2Aainfix &lt;=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FIainfix &lt;=c0ainfix -V0c2Aainfix &gt;c0ainfix -V0c2NICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix &lt;=c2V0Aainfix &lt;=c0V0Lamk arrayV0V2FF">
shape="fIais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix &lt;V5V0Aainfix &lt;V4V5Aainfix &lt;V4ainfix +ainfix -V0c2c1Aainfix &lt;=c0V4FAiCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix &lt;V11V0Aainfix &lt;V10V11Aainfix &lt;V10ainfix +V7c1Aainfix &lt;=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix &lt;V14V0Aainfix &lt;V13V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FIais_dupletV3V7V16NIainfix &lt;V16ainfix +ainfix -V0c1c1Aainfix &lt;V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =V19V17Aainfix =V18V7Fais_dupletV3V7V21NIainfix &lt;V21ainfix +V17c1Aainfix &lt;V7V21FAainfix &lt;V17V0Aainfix &lt;=c0V17Iais_dupletV3V7V22NIainfix &lt;V22V17Aainfix &lt;V7V22FIainfix &lt;=V17ainfix -V0c1Aainfix &lt;=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix &lt;V23ainfix +V7c1Aainfix &lt;V7V23FIainfix &lt;=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix &lt;V25V0Aainfix &lt;V24V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FIainfix &gt;ainfix +V7c1ainfix -V0c1LagetV2V7Aainfix &lt;V7V0Aainfix &lt;=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix &lt;V28V0Aainfix &lt;V27V28Aainfix &lt;V27V7Aainfix &lt;=c0V27FIainfix &lt;=V7ainfix -V0c2Aainfix &lt;=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FIainfix &lt;=c0ainfix -V0c2AfIainfix &gt;c0ainfix -V0c2ICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix &lt;=c2V0Aainfix &lt;=c0V0Lamk arrayV0V2FF">
<label
name="expl:VC for duplet"/>
<proof
......
......@@ -16,7 +16,7 @@
<prover
id="3"
name="Coq"
version="8.3pl4"/>
version="8.4"/>
<prover
id="4"
name="Z3"
......@@ -56,10 +56,10 @@
locfile="../vacid_0_sparse_array.mlw"
loclnum="67" loccnumb="6" loccnume="10"
expl="VC for test"
sum="499a2e023c70626ddf813faea11bb7d4"
sum="07e02ff7c522a2120cdc08a0e3496f69"
proved="true"
expanded="false"
shape="iainfix &lt;=c0agetV7V4iainfix &lt;agetV7V4V5ais_eltV9V4qainfix =agetV6V10V4Aainfix &lt;V10V2Aainfix &lt;=c0V10LagetV7V4Aainfix &lt;V4V1Aainfix &lt;=c0V4ais_eltV9V4NAainfix &lt;V4V1Aainfix &lt;=c0V4ais_eltV9V4NAainfix &lt;V4V1Aainfix &lt;=c0V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V2Aainfix &lt;=c0V1Aainfix &lt;=c0V0Aainfix =agetV7agetV6V11V11Aainfix &lt;agetV6V11V0Aainfix &lt;=c0agetV6V11Iainfix &lt;V11V5Aainfix &lt;=c0V11FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V5V0Aainfix &lt;=c0V5Lamk sparse_arrayamk arrayV0V8amk arrayV1V7amk arrayV2V6V5V3FF">
shape="iainfix &lt;V10V5Aainfix &lt;=c0V10ais_eltV9V4qainfix =agetV6V11V4Aainfix &lt;V11V2Aainfix &lt;=c0V11LagetV7V4Aainfix &lt;V4V1Aainfix &lt;=c0V4ais_eltV9V4NLagetV7V4Aainfix &lt;V4V1Aainfix &lt;=c0V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V2Aainfix &lt;=c0V1Aainfix &lt;=c0V0Aainfix =agetV7agetV6V12V12Aainfix &lt;agetV6V12V0Aainfix &lt;=c0agetV6V12Iainfix &lt;V12V5Aainfix &lt;=c0V12FAainfix =V1V2Aainfix =V0V1Aainfix &lt;=V0amaxlenAainfix &lt;=V5V0Aainfix &lt;=c0V5Lamk sparse_arrayamk arrayV0V8amk arrayV1V7amk arrayV2V6V5V3FF">
<label
name="expl:VC for test"/>
<proof
......@@ -106,7 +106,7 @@
edited="vacid_0_sparse_array_2_SparseArray_permutation_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.71"/>
<result status="valid" time="1.30"/>
</proof>
</goal>
<goal
......@@ -416,7 +416,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.48"/>
<result status="valid" time="2.07"/>
</proof>
</goal>
</transf>
......
......@@ -5010,10 +5010,10 @@
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="199" loccnumb="4" loccnume="11"
expl="VC for compare"
sum="9a05cb67191a96523927942a91615aaf"
sum="ff5b17b7c6a54aed4d6683e372d642d1"
proved="true"
expanded="false"
shape="iainfix =V1V2altV4V2V1Iainfix &gt;c0c0AaltV4V1V2Iainfix &lt;c0c0Aainfix =V1V2Iainfix =c0c0iainfix =ainfix +V1V5V0altV4V2V1Iainfix &gt;aprefix -c1c0AaltV4V1V2Iainfix &lt;aprefix -c1c0Aainfix =V1V2Iainfix =aprefix -c1c0iainfix =ainfix +V2V5V0altV4V2V1Iainfix &gt;c1c0AaltV4V1V2Iainfix &lt;c1c0Aainfix =V1V2Iainfix =c1c0iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5altV4V2V1Iainfix &gt;aprefix -c1c0AaltV4V1V2Iainfix &lt;aprefix -c1c0Aainfix =V1V2Iainfix =aprefix -c1c0altV4V2V1Iainfix &gt;c1c0AaltV4V1V2Iainfix &lt;c1c0Aainfix =V1V2Iainfix =c1c0Aainfix &gt;agetV3ainfix +V1V5agetV3ainfix +V2V5Aainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Aainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Aainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Aainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iais_longest_common_prefixV4V1V2V5FAainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
expanded="true"
shape="iainfix =V1V2altV4V2V1Iainfix &gt;c0c0AaltV4V1V2Iainfix &lt;c0c0Aainfix =V1V2Iainfix =c0c0iainfix =ainfix +V1V5V0altV4V2V1Iainfix &gt;aprefix -c1c0AaltV4V1V2Iainfix &lt;aprefix -c1c0Aainfix =V1V2Iainfix =aprefix -c1c0iainfix =ainfix +V2V5V0altV4V2V1Iainfix &gt;c1c0AaltV4V1V2Iainfix &lt;c1c0Aainfix =V1V2Iainfix =c1c0iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5altV4V2V1Iainfix &gt;aprefix -c1c0AaltV4V1V2Iainfix &lt;aprefix -c1c0Aainfix =V1V2Iainfix =aprefix -c1c0iainfix &gt;agetV3ainfix +V1V5agetV3ainfix +V2V5altV4V2V1Iainfix &gt;c1c0AaltV4V1V2Iainfix &lt;c1c0Aainfix =V1V2Iainfix =c1c0fAainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Aainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Aainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Aainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iais_longest_common_prefixV4V1V2V5FAainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
<label
name="expl:VC for compare"/>
<transf
......@@ -6824,11 +6824,11 @@
name="WP_parameter compare.19"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="199" loccnumb="4" loccnume="11"
expl="19."
sum="4d535f7c00a1266cf93057d8bb896832"
expl="19. postcondition"
sum="20d0fcf6431f6573fee1132135d427b2"
proved="true"
expanded="false"
shape="ainfix &gt;agetV3ainfix +V1V5agetV3ainfix +V2V5Iainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix =ainfix +V2V5V0NIainfix =ainfix +V1V5V0NIais_longest_common_prefixV4V1V2V5FIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix =V1V2NIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
shape="ainfix =V1V2Iainfix =c1c0Iainfix &gt;agetV3ainfix +V1V5agetV3ainfix +V2V5Iainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix =ainfix +V2V5V0NIainfix =ainfix +V1V5V0NIais_longest_common_prefixV4V1V2V5FIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix =V1V2NIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
<label
name="expl:VC for compare"/>
<proof
......@@ -6837,7 +6837,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -6853,7 +6853,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
......@@ -6861,7 +6861,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.09"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
......@@ -6869,7 +6869,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.18"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -6877,7 +6877,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.17"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
......@@ -6885,7 +6885,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="9.98"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
......@@ -6893,7 +6893,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="10.00"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="10"
......@@ -6901,7 +6901,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.38"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="11"
......@@ -6909,7 +6909,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.14"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="12"
......@@ -6917,7 +6917,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.15"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -6925,10 +6925,10 @@
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="199" loccnumb="4" loccnume="11"
expl="20. postcondition"
sum="1e36d5f260d39efec1f1baf5653a2e61"
sum="dc59e031f17edc6314abed6596563e15"
proved="true"
expanded="false"
shape="ainfix =V1V2Iainfix =c1c0Iainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix =ainfix +V2V5V0NIainfix =ainfix +V1V5V0NIais_longest_common_prefixV4V1V2V5FIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix =V1V2NIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
shape="altV4V1V2Iainfix &lt;c1c0Iainfix &gt;agetV3ainfix +V1V5agetV3ainfix +V2V5Iainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix =ainfix +V2V5V0NIainfix =ainfix +V1V5V0NIais_longest_common_prefixV4V1V2V5FIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix =V1V2NIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
<label
name="expl:VC for compare"/>
<proof
......@@ -6937,7 +6937,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -6953,7 +6953,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
......@@ -6961,7 +6961,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
......@@ -6969,7 +6969,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
......@@ -6977,7 +6977,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="8"
......@@ -6985,7 +6985,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="9"
......@@ -6993,7 +6993,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="10"
......@@ -7025,10 +7025,10 @@
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="199" loccnumb="4" loccnume="11"
expl="21. postcondition"
sum="09b5339de31c4b88cd68314744715b9e"
sum="2f448692fcb252939a59d10fc059b603"
proved="true"
expanded="false"
shape="altV4V1V2Iainfix &lt;c1c0Iainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix =ainfix +V2V5V0NIainfix =ainfix +V1V5V0NIais_longest_common_prefixV4V1V2V5FIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix =V1V2NIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
shape="altV4V2V1Iainfix &gt;c1c0Iainfix &gt;agetV3ainfix +V1V5agetV3ainfix +V2V5Iainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix =ainfix +V2V5V0NIainfix =ainfix +V1V5V0NIais_longest_common_prefixV4V1V2V5FIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix =V1V2NIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
<label
name="expl:VC for compare"/>
<proof
......@@ -7037,7 +7037,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.10"/>
</proof>
<proof
prover="1"
......@@ -7061,7 +7061,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="unknown" time="0.14"/>
</proof>
<proof
prover="4"
......@@ -7069,7 +7069,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="timeout" time="10.24"/>
</proof>
<proof
prover="5"
......@@ -7077,7 +7077,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.07"/>
</proof>
<proof
prover="8"
......@@ -7085,7 +7085,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="timeout" time="9.98"/>
</proof>
<proof
prover="9"
......@@ -7093,7 +7093,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="unknown" time="20.06"/>
</proof>
<proof
prover="10"
......@@ -7101,7 +7101,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="timeout" time="10.12"/>
</proof>
<proof
prover="11"
......@@ -7109,7 +7109,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="timeout" time="10.15"/>
</proof>
<proof
prover="12"
......@@ -7117,18 +7117,18 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="timeout" time="10.17"/>
</proof>
</goal>
<goal
name="WP_parameter compare.22"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="199" loccnumb="4" loccnume="11"
expl="22. postcondition"
sum="746c7a6fefed09a2a34e2d5e2c85c519"
expl="22. unreachable point"
sum="ef287d2b768c08a7afbe62ef4eccc522"
proved="true"
expanded="false"
shape="altV4V2V1Iainfix &gt;c1c0Iainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix =ainfix +V2V5V0NIainfix =ainfix +V1V5V0NIais_longest_common_prefixV4V1V2V5FIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix =V1V2NIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
shape="fIainfix &gt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix &lt;agetV3ainfix +V1V5agetV3ainfix +V2V5NIainfix &lt;ainfix +V1V5V0Aainfix &lt;=c0ainfix +V1V5Iainfix &lt;ainfix +V2V5V0Aainfix &lt;=c0ainfix +V2V5Iainfix =ainfix +V2V5V0NIainfix =ainfix +V1V5V0NIais_longest_common_prefixV4V1V2V5FIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Iainfix =V1V2NIainfix &lt;=V2V0Aainfix &lt;=c0V2Aainfix &lt;=V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Lamk arrayV0V3FF">
<label
name="expl:VC for compare"/>
<proof
......@@ -7137,7 +7137,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="1"
......@@ -7161,7 +7161,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.14"/>
<result status="unknown" time="0.09"/>
</proof>
<proof
prover="4"
......@@ -7169,7 +7169,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.24"/>
<result status="unknown" time="0.18"/>
</proof>
<proof
prover="5"
......@@ -7177,7 +7177,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.15"/>
<result status="timeout" time="10.17"/>
</proof>
<proof
prover="8"
......@@ -7193,7 +7193,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="10.01"/>
<result status="unknown" time="19.99"/>
</proof>
<proof
prover="10"
......@@ -7201,7 +7201,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.45"/>
<result status="unknown" time="2.82"/>
</proof>
<proof
prover="11"
......@@ -7209,7 +7209,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.15"/>
<result status="timeout" time="10.14"/>
</proof>
<proof
prover="12"
......@@ -7217,7 +7217,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.17"/>
<result status="timeout" time="10.15"/>
</proof>
</goal>
</transf>
......@@ -16424,7 +16424,7 @@
<theory
name="LRS_test"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="478" loccnumb="7" loccnume="15"
loclnum="474" loccnumb="7" loccnume="15"
verified="true"
expanded="false">
</theory>
......
......@@ -123,6 +123,7 @@ let expl_xpost = Ident.create_label "expl:exceptional postcondition"
let expl_assume = Ident.create_label "expl:assumption"
let expl_assert = Ident.create_label "expl:assertion"
let expl_check = Ident.create_label "expl:check"
let expl_absurd = Ident.create_label "expl:unreachable point"
let expl_type_inv = Ident.create_label "expl:type invariant"
let expl_loop_init = Ident.create_label "expl:loop invariant init"
let expl_loop_keep = Ident.create_label "expl:loop invariant preservation"
......@@ -693,7 +694,7 @@ and wp_desc env e q xq = match e.e_node with
let f = wp_expl expl_assume f in
wp_implies (wp_label e f) q
| Eabsurd ->
wp_label e t_absurd
wp_label e (t_label_add expl_absurd t_absurd)
| Eany spec ->
let p = wp_label e (wp_expl expl_pre spec.c_pre) in
let p = t_label ?loc:e.e_loc p.t_label p in
......@@ -891,7 +892,7 @@ let bool_to_prop env f =
(* replace t_absurd with t_false *)
let rec unabsurd f = match f.t_node with
| Tapp (ls, []) when ls_equal ls ls_absurd ->
t_label_copy f t_false
t_label_copy f (t_label_add keep_on_simp_label t_false)
| _ ->
t_map unabsurd f
......
......@@ -48,4 +48,16 @@ module Termination
end
end
module Absurd
use import int.Int
let f (x:int) : int =
if x = 0 then 0 else
if x > 0 then (assert {1=1} ; 1) else
if x < 0 then -1 else(assert {1=1}; absurd)
end
\ No newline at end of file
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