Commit c08f38e3 authored by MARCHE Claude's avatar MARCHE Claude

solved merged conflicts

parents b4711106 b0092599
...@@ -141,7 +141,9 @@ orphaned-proofs.prf ...@@ -141,7 +141,9 @@ orphaned-proofs.prf
pvsbin/ pvsbin/
# Isabelle # Isabelle
/lib/isabelle/bool/
/lib/isabelle/int/ /lib/isabelle/int/
/lib/isabelle/number/
/lib/isabelle/list/ /lib/isabelle/list/
/lib/isabelle/map/ /lib/isabelle/map/
/lib/isabelle/set/ /lib/isabelle/set/
...@@ -217,9 +219,12 @@ pvsbin/ ...@@ -217,9 +219,12 @@ pvsbin/
/examples/use_api/runstrat/makejob.opt /examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt /examples/use_api/runstrat/runstrat.opt
/examples/vstte10_max_sum/*__*.ml /examples/vstte10_max_sum/*__*.ml
/examples/euler001/euler001__*.ml /examples/euler001/*__*.ml
/examples/sudoku/sudoku__*.ml /examples/sudoku/*__*.ml
/examples/in_progress/defunctionalization/defunctionalization__*.ml /examples/defunctionalization/*__*.ml
examples/vstte12_combinators/jsmain.js
examples/vstte12_combinators/*__*.ml
# modules # modules
/modules/string/ /modules/string/
...@@ -229,6 +234,7 @@ pvsbin/ ...@@ -229,6 +234,7 @@ pvsbin/
/modules/mach/array/ /modules/mach/array/
/modules/mach/int/ /modules/mach/int/
# jessie3 # jessie3
/src/jessie/.depend /src/jessie/.depend
/src/jessie/Jessie3_DEP /src/jessie/Jessie3_DEP
...@@ -238,6 +244,7 @@ pvsbin/ ...@@ -238,6 +244,7 @@ pvsbin/
/src/jessie/Makefile /src/jessie/Makefile
/src/jessie/literals.ml /src/jessie/literals.ml
/src/jessie/ptests_local_config.ml /src/jessie/ptests_local_config.ml
/src/jessie/tests/basic/frama_c_journal.ml
/src/jessie/tests/basic/result/*.log /src/jessie/tests/basic/result/*.log
/src/jessie/tests/demo/result/*.log /src/jessie/tests/demo/result/*.log
/trash /trash
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
locfile="../add_list.mlw" locfile="../add_list.mlw"
loclnum="32" loccnumb="8" loccnume="11" loclnum="32" loccnumb="8" loccnume="11"
expl="VC for sum" expl="VC for sum"
sum="0a492f8ad504c050cdce87f294c7e321" sum="0ad629c2956d434cdf621a03e0b7c7ba"
proved="true" proved="true"
expanded="true" expanded="true"
shape="Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FACfaNilainfix =V7V2aConswVV0aConsVVV0F"> shape="Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FACfaNilainfix =V7V2aConswVV0aConsVVV0F">
...@@ -71,7 +71,7 @@ ...@@ -71,7 +71,7 @@
locfile="../add_list.mlw" locfile="../add_list.mlw"
loclnum="45" loccnumb="4" loccnume="8" loclnum="45" loccnumb="4" loccnume="8"
expl="VC for main" expl="VC for main"
sum="e4ee17c3f0db6f44050cfe5e902ce0cf" sum="6b4e350cd7d1b4015bab61dc01e96aec"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil"> shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil">
...@@ -106,7 +106,7 @@ ...@@ -106,7 +106,7 @@
locfile="../add_list.mlw" locfile="../add_list.mlw"
loclnum="64" loccnumb="4" loccnume="7" loclnum="64" loccnumb="4" loccnume="7"
expl="VC for sum" expl="VC for sum"
sum="0f9b53b209abc77940c4947079bdeb93" sum="82f58e47d4e58d15d59a87efee2a6ad8"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilCfaNilainfix =V8V7aConswVV1Aainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVCfaNilainfix =V13V12aConswVV1Aainfix =ainfix +.V11aadd_realV12aadd_realV0Aainfix =ainfix +V3aadd_intV12aadd_intV0Iainfix =V12V10FIainfix =V11ainfix +.V2V9FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F"> shape="ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilCfaNilainfix =V8V7aConswVV1Aainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVCfaNilainfix =V13V12aConswVV1Aainfix =ainfix +.V11aadd_realV12aadd_realV0Aainfix =ainfix +V3aadd_intV12aadd_intV0Iainfix =V12V10FIainfix =V11ainfix +.V2V9FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
...@@ -134,7 +134,7 @@ ...@@ -134,7 +134,7 @@
locfile="../add_list.mlw" locfile="../add_list.mlw"
loclnum="88" loccnumb="4" loccnume="8" loclnum="88" loccnumb="4" loccnume="8"
expl="VC for main" expl="VC for main"
sum="bd44a1ba46c51b25c11a2cfdaf1b3abd" sum="9051692e9ac1a4d1f56386a0fd7d440f"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil"> shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil">
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
locfile="../assigning_meanings_to_programs.mlw" locfile="../assigning_meanings_to_programs.mlw"
loclnum="12" loccnumb="6" loccnume="9" loclnum="12" loccnumb="6" loccnume="9"
expl="VC for sum" expl="VC for sum"
sum="329d3acbda193f226c9e300474bf832a" sum="08be4365a1bbf3642e32e902d58a4e3c"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix =V3asumV1c1ainfix +V2c1ainfix <ainfix -V2V6ainfix -V2V4Aainfix <=c0ainfix -V2V4Aainfix =V5asumV1c1V6Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV1V4FAainfix <V4V0Aainfix <=c0V4ainfix <=V4V2Iainfix =V3asumV1c1V4Aainfix <=V4ainfix +V2c1Aainfix <=c1V4FAainfix =c0asumV1c1c1Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Aainfix <=c0V2Aainfix <=c0V0F"> shape="iainfix =V3asumV1c1ainfix +V2c1ainfix <ainfix -V2V6ainfix -V2V4Aainfix <=c0ainfix -V2V4Aainfix =V5asumV1c1V6Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV1V4FAainfix <V4V0Aainfix <=c0V4ainfix <=V4V2Iainfix =V3asumV1c1V4Aainfix <=V4ainfix +V2c1Aainfix <=c1V4FAainfix =c0asumV1c1c1Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Aainfix <=c0V2Aainfix <=c0V0F">
...@@ -51,7 +51,7 @@ ...@@ -51,7 +51,7 @@
locfile="../assigning_meanings_to_programs.mlw" locfile="../assigning_meanings_to_programs.mlw"
loclnum="38" loccnumb="6" loccnume="14" loclnum="38" loccnumb="6" loccnume="14"
expl="VC for division" expl="VC for division"
sum="188bd14860a30ee027c058f8c34ad87a" sum="5a077cf4ab2c23e67ed74619034dc338"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix >=V2V1Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0F"> shape="iainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix >=V2V1Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0F">
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
name="closest" name="closest"
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="34" loccnumb="8" loccnume="15" loclnum="34" loccnumb="8" loccnume="15"
sum="95d8e3e83400477156b0c6fbd6ebe59e" sum="472a5d038bef87fcbfb94fa2e7253191"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix <=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix <=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0F"> shape="ainfix <=aabsainfix -ainfix *V0V1V2aabsainfix -ainfix *V0V3V2FIainfix <=aabsainfix -ainfix *ainfix *c2V0V1ainfix *c2V2V0F">
...@@ -54,7 +54,7 @@ ...@@ -54,7 +54,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="VC for bresenham" expl="VC for bresenham"
sum="7ba5580c4640dde414e2e5c479466406" sum="c273b5a8d99bf83f043f35169bda938e"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <=V5ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V5Aainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1Fainfix <=V6ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V6Aainfix =V6ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V6ainfix +V1ainfix *c2ay2Fainfix <V1c0AabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFAainfix <=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Aainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix <=c0V0Lax2"> shape="iainfix <=V5ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V5Aainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1Fainfix <=V6ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V6Aainfix =V6ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V6ainfix +V1ainfix *c2ay2Fainfix <V1c0AabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFAainfix <=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Aainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix <=c0V0Lax2">
...@@ -69,7 +69,7 @@ ...@@ -69,7 +69,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="1. loop invariant init" expl="1. loop invariant init"
sum="73bac718d188f399d95c94526ff00d45" sum="ed65b836fad1f9e81238b52f26b3793b"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix <=c0V0Lax2"> shape="loop invariant initainfix =ainfix -ainfix *c2ay2ax2ainfix -ainfix *ainfix *c2ainfix +c0c1ay2ainfix *ainfix +ainfix *c2c0c1ax2Iainfix <=c0V0Lax2">
...@@ -105,7 +105,7 @@ ...@@ -105,7 +105,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="2. loop invariant init" expl="2. loop invariant init"
sum="d3ff8f58676f65292f348f1e01ad13c6" sum="1f431337ccd802b522a98f30abadccae"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix <=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Iainfix <=c0V0Lax2"> shape="loop invariant initainfix <=ainfix -ainfix *c2ay2ax2ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2ainfix -ainfix *c2ay2ax2Iainfix <=c0V0Lax2">
...@@ -125,7 +125,7 @@ ...@@ -125,7 +125,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="3. assertion" expl="3. assertion"
sum="145816b0641871a72f5fd04fc38bd8af" sum="34351a2fcaf0596c940f5c34b7545156"
proved="true" proved="true"
expanded="true" expanded="true"
shape="assertionabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2"> shape="assertionabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2">
...@@ -153,7 +153,7 @@ ...@@ -153,7 +153,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="4. loop invariant preservation" expl="4. loop invariant preservation"
sum="0c464430697f406b20cf1199bd5adfb9" sum="74d2dd38d47dd2952bd12873b5e1bd85"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V4ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix <V1c0IabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2"> shape="loop invariant preservationainfix =V4ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix <V1c0IabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2">
...@@ -189,7 +189,7 @@ ...@@ -189,7 +189,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="5. loop invariant preservation" expl="5. loop invariant preservation"
sum="4b9a313a3ab1ccca4f6b19eb2c6d673f" sum="49fe8a7e169678e5aaf592b78ff8cebd"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix <=V4ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V4Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix <V1c0IabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2"> shape="loop invariant preservationainfix <=V4ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V4Iainfix =V4ainfix +V1ainfix *c2ay2FIainfix <V1c0IabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2">
...@@ -209,7 +209,7 @@ ...@@ -209,7 +209,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="6. loop invariant preservation" expl="6. loop invariant preservation"
sum="8c9dfb21ea36fe4493a3fe323019ebd6" sum="3ac02f3d978219fa286a8d3d74638379"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix <V1c0IabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2"> shape="loop invariant preservationainfix =V5ainfix -ainfix *ainfix *c2ainfix +ainfix +V3c1c1ay2ainfix *ainfix +ainfix *c2V4c1ax2Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix <V1c0IabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2">
...@@ -237,7 +237,7 @@ ...@@ -237,7 +237,7 @@
locfile="../bresenham.mlw" locfile="../bresenham.mlw"
loclnum="39" loccnumb="6" loccnume="15" loclnum="39" loccnumb="6" loccnume="15"
expl="7. loop invariant preservation" expl="7. loop invariant preservation"
sum="c4eeab8e74f4cc05b9c39bab40e5a4b7" sum="ff4fa86e8ee958cfa266e050e0feb12a"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix <=V5ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V5Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix <V1c0IabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2"> shape="loop invariant preservationainfix <=V5ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V5Iainfix =V5ainfix +V1ainfix *c2ainfix -ay2ax2FIainfix =V4ainfix +V2c1FINainfix <V1c0IabestV3V2Iainfix <=V1ainfix *c2ay2Aainfix <=ainfix *c2ainfix -ay2ax2V1Aainfix =V1ainfix -ainfix *ainfix *c2ainfix +V3c1ay2ainfix *ainfix +ainfix *c2V2c1ax2Iainfix <=V3V0Aainfix <=c0V3FFIainfix <=c0V0Lax2">
......
...@@ -27,7 +27,7 @@ ...@@ -27,7 +27,7 @@
locfile="../13375.mlw" locfile="../13375.mlw"
loclnum="51" loccnumb="5" loccnume="12" loclnum="51" loccnumb="5" loccnume="12"
expl="VC for to_int_" expl="VC for to_int_"
sum="32f921fac01c5c8809e2cb26c095e80a" sum="b4f0541b4c4377308ec8f3fecd53df95"
proved="true" proved="true"
expanded="true" expanded="true"
shape="t"> shape="t">
......
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
locfile="../13853.mlw" locfile="../13853.mlw"
loclnum="16" loccnumb="8" loccnume="9" loclnum="16" loccnumb="8" loccnume="9"
expl="VC for f" expl="VC for f"
sum="b02952dbc728d0247c4fc708f2e40d93" sum="9275b68b643d54fa046901827105e2ab"
proved="true" proved="true"
expanded="true" expanded="true"
shape="t"> shape="t">
...@@ -40,7 +40,7 @@ ...@@ -40,7 +40,7 @@
locfile="../13853.mlw" locfile="../13853.mlw"
loclnum="17" loccnumb="8" loccnume="9" loclnum="17" loccnumb="8" loccnume="9"
expl="VC for g" expl="VC for g"
sum="1457d9f96317c678855684b7f490c772" sum="7c3013c5e05d7f356eafae2533104334"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix <c0c1Aainfix <=c0c1"> shape="ainfix <c0c1Aainfix <=c0c1">
......
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
name="l_false" name="l_false"
locfile="../fsetint.why" locfile="../fsetint.why"
loclnum="5" loccnumb="9" loccnume="16" loclnum="5" loccnumb="9" loccnume="16"
sum="0158150de9c97af9dd9820938313b4d5" sum="a7f81fb4ac311e211b36f45d9d999cd6"
proved="false" proved="false"
expanded="true" expanded="true"
shape="f"> shape="f">
...@@ -91,7 +91,7 @@ ...@@ -91,7 +91,7 @@
name="mem_integer" name="mem_integer"
locfile="../fsetint.why" locfile="../fsetint.why"
loclnum="13" loccnumb="8" loccnume="19" loclnum="13" loccnumb="8" loccnume="19"
sum="3658829cdb3f859e8fd24937b2513f62" sum="5b36021da6d9a18bf73dd4b4cdb0c704"
proved="false" proved="false"
expanded="true" expanded="true"
shape="amemV0aintegerF"> shape="amemV0aintegerF">
...@@ -140,7 +140,7 @@ ...@@ -140,7 +140,7 @@
name="foo" name="foo"
locfile="../fsetint.why" locfile="../fsetint.why"
loclnum="15" loccnumb="7" loccnume="10" loclnum="15" loccnumb="7" loccnume="10"
sum="99afe7ade68f07f16139a57d95d5df7e" sum="39c6d770ebced41b90789c3603ed5789"
proved="false" proved="false"
expanded="true" expanded="true"
shape="f"> shape="f">
......
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="VC for routine" expl="VC for routine"
sum="b6b5481cb51b7e0c70ff9af6915ef113" sum="2a3138957b573908bd8c821b1b0617b7"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix =V1afactV0iainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1Fainfix <ainfix -V2V7ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix =V6ainfix *V7afactV2Aainfix <=V7ainfix +V2c1Aainfix <=c1V7Iainfix =V7ainfix +V3c1FIainfix =V6ainfix +V4V1Fainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FAainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1ainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FAainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F"> shape="iainfix =V1afactV0iainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1Fainfix <ainfix -V2V7ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix =V6ainfix *V7afactV2Aainfix <=V7ainfix +V2c1Aainfix <=c1V7Iainfix =V7ainfix +V3c1FIainfix =V6ainfix +V4V1Fainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FAainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1ainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FAainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F">
...@@ -39,7 +39,7 @@ ...@@ -39,7 +39,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="1. loop invariant init" expl="1. loop invariant init"
sum="0eb61307b91c2331318ee93f9effac3c" sum="afec874cfd61e3b6ff015773aaaa8868"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F"> shape="loop invariant initainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F">
...@@ -59,7 +59,7 @@ ...@@ -59,7 +59,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="2. loop invariant init" expl="2. loop invariant init"
sum="17cdb36ee2341f2279e0cf83995fdb58" sum="5130fcaaff0833e7b93714bbbffc19ae"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F"> shape="loop invariant initainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F">
...@@ -79,7 +79,7 @@ ...@@ -79,7 +79,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="3. loop invariant preservation" expl="3. loop invariant preservation"
sum="1ace46d516a0fdf573b4e9bb4b8a4e0c" sum="2214e2fd2699bf390895e7c267f4a9d8"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F"> shape="loop invariant preservationainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F">
...@@ -99,7 +99,7 @@ ...@@ -99,7 +99,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="4. loop variant decrease" expl="4. loop variant decrease"
sum="1578eeea58be86a10c85e40060cec867" sum="a0acf28c828789341b1be0d02b429fa6"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop variant decreaseainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F"> shape="loop variant decreaseainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F">
...@@ -119,7 +119,7 @@ ...@@ -119,7 +119,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="5. loop invariant preservation" expl="5. loop invariant preservation"
sum="eefe4b3483bb694f5ca92a7722cbd546" sum="53a5157a6d458e37609beab5b57bd549"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FINainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F"> shape="loop invariant preservationainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FINainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F">
...@@ -139,7 +139,7 @@ ...@@ -139,7 +139,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="6. loop variant decrease" expl="6. loop variant decrease"
sum="7a85e21f66f49405053c48f4d8c159e3" sum="ce4d1ffe271a50ff4ae32737dfada01c"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop variant decreaseainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =V5ainfix +V2c1FINainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F"> shape="loop variant decreaseainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =V5ainfix +V2c1FINainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F">
...@@ -159,7 +159,7 @@ ...@@ -159,7 +159,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="7. postcondition" expl="7. postcondition"
sum="c8d4f9bc758f1be2b89ead1120ac33dc" sum="bca737a26ee2cb7df8c1431e29e6971c"
proved="true" proved="true"
expanded="true" expanded="true"
shape="postconditionainfix =V1afactV0INainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F"> shape="postconditionainfix =V1afactV0INainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FIainfix >=V0c0F">
...@@ -181,7 +181,7 @@ ...@@ -181,7 +181,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="VC for routine2" expl="VC for routine2"
sum="cd3b8e0513993bb30efb41ed23ef34d4" sum="eeb8e8edfb22e083b7dedabd95f5aa56"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V2afactV0Iainfix =V2afactainfix +V1c1Aainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3Aainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix <=V5V3Aainfix <=c1V5FFAainfix =V2ainfix *c1afactV3Iainfix <=c1V3Aainfix =V2afactainfix +V3c1Iainfix >c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFAainfix =c1afactc0Iainfix <=c0V1Aainfix =c1afactV0Iainfix >c0V1Lainfix -V0c1Iainfix >=V0c0F"> shape="ainfix =V2afactV0Iainfix =V2afactainfix +V1c1Aainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3Aainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix <=V5V3Aainfix <=c1V5FFAainfix =V2ainfix *c1afactV3Iainfix <=c1V3Aainfix =V2afactainfix +V3c1Iainfix >c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFAainfix =c1afactc0Iainfix <=c0V1Aainfix =c1afactV0Iainfix >c0V1Lainfix -V0c1Iainfix >=V0c0F">
...@@ -196,7 +196,7 @@ ...@@ -196,7 +196,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="1. postcondition" expl="1. postcondition"
sum="f18d3e5252e4c202abc17515531067ba" sum="8c9c9bb26b7166590a130cd8ee5417e5"
proved="true" proved="true"
expanded="true" expanded="true"
shape="postconditionainfix =c1afactV0Iainfix >c0V1Lainfix -V0c1Iainfix >=V0c0F"> shape="postconditionainfix =c1afactV0Iainfix >c0V1Lainfix -V0c1Iainfix >=V0c0F">
...@@ -216,7 +216,7 @@ ...@@ -216,7 +216,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="2. loop invariant init" expl="2. loop invariant init"
sum="309ddfa2c36dc1b8fde6e7e1721c83d2" sum="21ee890b789548fb281a2912e53018ea"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =c1afactc0Iainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F"> shape="loop invariant initainfix =c1afactc0Iainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F">
...@@ -236,7 +236,7 @@ ...@@ -236,7 +236,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="3. loop invariant preservation" expl="3. loop invariant preservation"
sum="4e9f02c291b0686631a49ed6e54e654f" sum="5cbc0a707337ba24d10e8f6d4efa547b"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V2afactainfix +V3c1Iainfix >c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F"> shape="loop invariant preservationainfix =V2afactainfix +V3c1Iainfix >c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F">
...@@ -256,7 +256,7 @@ ...@@ -256,7 +256,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="4. loop invariant init" expl="4. loop invariant init"
sum="32c64d5b033a385d1394b180d6b835aa" sum="138e1aff1a2d170a82d5a444e79dc037"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant initainfix =V2ainfix *c1afactV3Iainfix <=c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F"> shape="loop invariant initainfix =V2ainfix *c1afactV3Iainfix <=c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F">
...@@ -276,7 +276,7 @@ ...@@ -276,7 +276,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="5. loop invariant preservation" expl="5. loop invariant preservation"
sum="f2da4444521bc9d9f94f1edd54098af3" sum="98f84ee0629e2d03ebd9bcd00f47e2e5"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix <=V5V3Aainfix <=c1V5FFIainfix <=c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F"> shape="loop invariant preservationainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix <=V5V3Aainfix <=c1V5FFIainfix <=c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F">
...@@ -296,7 +296,7 @@ ...@@ -296,7 +296,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="6. loop invariant preservation" expl="6. loop invariant preservation"
sum="e98222c8a5d88bb129eb443e02c662df" sum="842cd4f4c5cebaff76e716747e8f4963"
proved="true" proved="true"
expanded="true" expanded="true"
shape="loop invariant preservationainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3FIainfix <=c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F"> shape="loop invariant preservationainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3FIainfix <=c1V3Iainfix =V2afactV3Iainfix <=V3V1Aainfix <=c0V3FFIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F">
...@@ -316,7 +316,7 @@ ...@@ -316,7 +316,7 @@
locfile="../checking_a_large_routine.mlw" locfile="../checking_a_large_routine.mlw"
loclnum="32" loccnumb="6" loccnume="14" loclnum="32" loccnumb="6" loccnume="14"
expl="7. postcondition" expl="7. postcondition"
sum="cec5ffbe4cde68dfe5c00dd13ee15719" sum="5caa517862996f00123b80203c73e7d5"
proved="true" proved="true"
expanded="true" expanded="true"
shape="postconditionainfix =V2afactV0Iainfix =V2afactainfix +V1c1FIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F"> shape="postconditionainfix =V2afactV0Iainfix =V2afactainfix +V1c1FIainfix <=c0V1Lainfix -V0c1Iainfix >=V0c0F">
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="VC for division" expl="VC for division"
sum="17325b12d2a5ee97ba9722c3e954bfbb" sum="3be80ec9874e12458fe48adae254a8f8"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <V4V1Aainfix <=c0V4Aainfix =ainfix +ainfix *V3V1V4V0Eainfix <V6V2Aainfix <=c0V2Aainfix <=c0V6Aainfix =ainfix +ainfix *V5V1V6V0Iainfix =V6ainfix -V2V1FIainfix =V5ainfix +V3c1Fainfix >=V2V1Iainfix <=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FAainfix <=c0V0Aainfix =ainfix +ainfix *c0V1V0V0Iainfix <c0V1Aainfix <=c0V0F"> shape="iainfix <V4V1Aainfix <=c0V4Aainfix =ainfix +ainfix *V3V1V4V0Eainfix <V6V2Aainfix <=c0V2Aainfix <=c0V6Aainfix =ainfix +ainfix *V5V1V6V0Iainfix =V6ainfix -V2V1FIainfix =V5ainfix +V3c1Fainfix >=V2V1Iainfix <=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FAainfix <=c0V0Aainfix =ainfix +ainfix *c0V1V0V0Iainfix <c0V1Aainfix <=c0V0F">
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="1. loop invariant init" expl="1. loop invariant init"
sum="23210e55ab366e193f6469f3dd8a7dc9" sum="394a2b099ea6779d53ed1135f9bca956"
proved="true" proved="true"
expanded="false" expanded="false"
shape="loop invariant initainfix <=c0V0Aainfix =ainfix +ainfix *c0V1V0V0Iainfix <c0V1Aainfix <=c0V0F"> shape="loop invariant initainfix <=c0V0Aainfix =ainfix +ainfix *c0V1V0V0Iainfix <c0V1Aainfix <=c0V0F">
...@@ -55,7 +55,7 @@ ...@@ -55,7 +55,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="2. loop invariant preservation" expl="2. loop invariant preservation"
sum="4f68a1a401e16e01cbc0584a2d13e5a8" sum="bc8662e540975908b079798415968d9f"
proved="true" proved="true"
expanded="false" expanded="false"
shape="loop invariant preservationainfix <=c0V5Aainfix =ainfix +ainfix *V4V1V5V0Iainfix =V5ainfix -V2V1FIainfix =V4ainfix +V3c1FIainfix >=V2V1Iainfix <=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix <c0V1Aainfix <=c0V0F"> shape="loop invariant preservationainfix <=c0V5Aainfix =ainfix +ainfix *V4V1V5V0Iainfix =V5ainfix -V2V1FIainfix =V4ainfix +V3c1FIainfix >=V2V1Iainfix <=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix <c0V1Aainfix <=c0V0F">
...@@ -75,7 +75,7 @@ ...@@ -75,7 +75,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="3. loop variant decrease" expl="3. loop variant decrease"
sum="dbc2a65014dce06f159a71dd16dc7fff" sum="304a17bede656d31971976da48e433a5"
proved="true" proved="true"
expanded="false" expanded="false"
shape="loop variant decreaseainfix <V5V2Aainfix <=c0V2Iainfix =V5ainfix -V2V1FIainfix =V4ainfix +V3c1FIainfix >=V2V1Iainfix <=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix <c0V1Aainfix <=c0V0F"> shape="loop variant decreaseainfix <V5V2Aainfix <=c0V2Iainfix =V5ainfix -V2V1FIainfix =V4ainfix +V3c1FIainfix >=V2V1Iainfix <=c0V2Aainfix =ainfix +ainfix *V3V1V2V0FIainfix <c0V1Aainfix <=c0V0F">
...@@ -95,7 +95,7 @@ ...@@ -95,7 +95,7 @@
locfile="../division.mlw" locfile="../division.mlw"
loclnum="9" loccnumb="6" loccnume="14" loclnum="9" loccnumb="6" loccnume="14"
expl="4. postcondition" expl="4. postcondition"
sum="0e720ad9c169791b83d053e9325c9ee3"