Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit f810eab3 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch '205-get-rid-of-clause-syntax-converter-in-drivers' into 'master'

Resolve "Get rid of clause `syntax converter` in drivers"

Closes #205

See merge request !41
parents cc748e4f 6b6e68e3
......@@ -10,9 +10,8 @@ module ref.Ref
syntax type ref "%1"
syntax val ref "%1"
syntax val (!_) "%1"
syntax converter (!_) "%1"
syntax val (:=) "%1 = %2"
syntax converter contents "%1"
syntax val contents "%1"
end
module mach.int.Unsigned
......@@ -22,10 +21,9 @@ module mach.int.Unsigned
end
module mach.int.Int32
syntax val of_int "%1"
syntax converter of_int "%1"
syntax type int32 "int32_t"
syntax literal int32 "%d"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
......@@ -44,15 +42,14 @@ module mach.int.UInt32Gen
syntax type uint32 "uint32_t"
syntax converter max_uint32 "0xffffffff"
syntax converter length "32"
syntax val max_uint32 "0xffffffff"
syntax val length "32"
end
module mach.int.UInt32
syntax converter of_int "%1U"
syntax literal uint32 "0x%8xU"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
......@@ -183,7 +180,7 @@ struct __lsld32_result
struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
"
syntax converter of_int "%1U"
syntax literal uint32 "0x%8xU"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
......@@ -222,10 +219,8 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
end
module mach.int.Int64
syntax val of_int "%1"
syntax converter of_int "%1"
syntax type int64 "int64_t"
syntax literal int64 "%dLL"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
......@@ -244,14 +239,14 @@ module mach.int.UInt64Gen
syntax type uint64 "uint64_t"
syntax converter max_uint64 "0xffffffffffffffff"
syntax converter length "64"
syntax val max_uint64 "0xffffffffffffffff"
syntax val length "64"
end
module mach.int.UInt64
syntax converter of_int "%1ULL"
syntax literal uint64 "0x%16xULL"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
......@@ -506,7 +501,9 @@ static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
return result;
}
"
syntax converter of_int "%1ULL"
syntax literal uint64 "0x%16xULL"
syntax val uint64_max "0xffffffffffffffffULL"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
......
......@@ -6,21 +6,26 @@ theory bv.BV_Gen
end
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
(* mapping of_int to int2bv is disabled because it breaks proofs
in examples/bitcount, examples/esterel,
examples/isqrt_von_neumann, examples/rightmostbittrick,
examples/bitwalker *)
(* syntax function of_int "((_ int2bv 64) %1)" *)
syntax function t'int "(bv2nat %1)"
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
(* syntax function of_int "((_ int2bv 32) %1)" *)
syntax function t'int "(bv2nat %1)"
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
(* syntax function of_int "((_ int2bv 16) %1)" *)
syntax function t'int "(bv2nat %1)"
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
(* syntax function of_int "((_ int2bv 8) %1)" *)
syntax function t'int "(bv2nat %1)"
end
......@@ -138,8 +138,7 @@ module matrix.Matrix
end
module mach.int.Int31
syntax val of_int "(fun x -> x)"
syntax converter of_int "%1"
syntax val of_int "%1"
syntax function to_int "(%1)"
......@@ -157,8 +156,7 @@ module mach.int.Int31
syntax val (>) "(>)"
end
module mach.int.Int63
syntax val of_int "(fun x -> x)"
syntax converter of_int "%1"
syntax val of_int "%1"
syntax function to_int "(%1)"
......@@ -234,4 +232,3 @@ module mach.matrix.Matrix63
syntax val make "Array.make_matrix"
syntax val copy "(Array.map Array.copy)"
end
......@@ -206,7 +206,6 @@ module mach.int.Int63
syntax type int63 "int"
syntax literal int63 "%1"
syntax converter of_int "%1"
syntax val of_int "Z.to_int %1"
syntax val to_int "Z.of_int %1"
......@@ -311,8 +310,6 @@ module mach.onetime.OneTime
syntax val eq "%1 = %2"
syntax val ne "%1 <> %2"
syntax converter to_peano "%1"
syntax val transfer "%1"
syntax val neg "-%1"
syntax val abs "abs %1"
......
......@@ -76,30 +76,3 @@ theory real.Trigonometry
end
*)
(* REMOVED: we do not use BV theory from Z3 in 4.3.2 but starting from 4.4.0
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
end
*)
\ No newline at end of file
......@@ -6,7 +6,10 @@ theory bv.BV_Gen
end
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
(* mapping of_int to int2bv is disabled because it breaks proofs
in examples/queens_bv, examples/bitwalker *)
(* syntax function of_int "((_ int2bv 64) %1)" *)
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
......@@ -14,7 +17,7 @@ theory bv.BV64
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
(* syntax function of_int "((_ int2bv 32) %1)" *)
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
......@@ -22,7 +25,7 @@ theory bv.BV32
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
(* syntax function of_int "((_ int2bv 16) %1)" *)
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
......@@ -30,7 +33,7 @@ theory bv.BV16
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
(* syntax function of_int "((_ int2bv 8) %1)" *)
syntax function t'int "(bv2int %1)"
remove prop Nth_bv_is_nth
......
......@@ -47,7 +47,7 @@
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC binary_mult.11" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.73"/></proof>
<proof prover="3"><result status="valid" time="1.00"/></proof>
</goal>
<goal name="VC binary_mult.12" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......
......@@ -368,7 +368,7 @@ module AsciiCode
ensures { eq_sub_bv result b zeros lastbit }
ensures { validAscii result }
let c = count b in
let maskbit = lsl_check c (of_int 31) in
let maskbit = lsl_check c (31:t) in
assert { bw_and b maskbit = zeros };
assert { even (t'int c) ->
not (nth_bv c zeros)
......
......@@ -3,6 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="5" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
......@@ -299,7 +300,7 @@
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC proof1.6.2" expl="VC for proof1" proved="true">
<proof prover="4"><result status="valid" time="1.00"/></proof>
<proof prover="4"><result status="valid" time="1.32"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="96"/></proof>
</goal>
</transf>
......@@ -775,39 +776,29 @@
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.11"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.09" steps="97"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.09" steps="81"/></proof>
</goal>
<goal name="VC ascii.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC ascii.2" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC ascii.2.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.08" steps="87"/></proof>
</goal>
<goal name="VC ascii.2.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
<proof prover="6"><result status="valid" time="0.18" steps="403"/></proof>
</goal>
<goal name="VC ascii.3" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC ascii.3.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.02" steps="88"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.02" steps="89"/></proof>
</goal>
<goal name="VC ascii.3.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.14"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.16" steps="321"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.04" steps="157"/></proof>
</goal>
<goal name="VC ascii.3.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
<proof prover="4"><result status="valid" time="0.11"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.24" steps="280"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.02" steps="111"/></proof>
</goal>
<goal name="VC ascii.3.3" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.09"/></proof>
......@@ -815,18 +806,16 @@
</transf>
</goal>
<goal name="VC ascii.4" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.11"/></proof>
<proof prover="6"><result status="valid" time="0.05" steps="86"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC ascii.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.11"/></proof>
<proof prover="4"><result status="valid" time="1.58"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC ascii.6" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.52"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.21" steps="362"/></proof>
<proof prover="6"><result status="valid" time="0.21" steps="374"/></proof>
</goal>
</transf>
</goal>
......
......@@ -29,15 +29,15 @@ module Bitwalker
(* *)
let function maxvalue (len : BV32.t) : BV64.t =
BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)
BV64.lsl_bv (1:BV64.t) (C32_64.toBig len)
let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
requires { BV32.t'int len < 64}
ensures { BV64.eq_sub x BV64.zeros (BV32.t'int len) (64 - BV32.t'int len)
<-> BV64.t'int x < BV64.t'int (maxvalue len) }
=
assert { BV32.ult len (BV32.of_int 64) };
assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (BV64.of_int 64) (C32_64.toBig len))
assert { BV32.ult len (64:BV32.t) };
assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (64:BV64.t) (C32_64.toBig len))
<-> BV64.ult x (maxvalue len) }
(** return `value` with the bit of index `left` from the left set to `flag` *)
......@@ -47,13 +47,13 @@ module Bitwalker
BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - BV32.t'int left) }
=
assert { BV32.ult left (BV32.of_int 64) };
assert { BV32.ult left (64:BV32.t) };
begin
ensures { forall i:BV32.t. i <> BV32.sub (BV32.of_int 63) left ->
ensures { forall i:BV32.t. i <> BV32.sub (63:BV32.t) left ->
BV64.nth_bv result (C32_64.toBig i) =
BV64.nth_bv value (C32_64.toBig i) }
ensures { flag = BV64.nth_bv result
(C32_64.toBig (BV32.sub (BV32.of_int 63) left)) }
(C32_64.toBig (BV32.sub (63:BV32.t) left)) }
let mask =
BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.sub_check (63:BV32.t) left))
......@@ -75,13 +75,13 @@ module Bitwalker
ensures { flag = BV64.nth result (63 - left) }
=
let ghost left_bv = BV64.of_int left in
assert { BV64.ult left_bv (BV64.of_int 64) };
assert { (BV64.sub (BV64.of_int 63) left_bv) = BV64.of_int (63 - left) };
assert { BV64.ult left_bv (64:BV64.t) };
assert { (BV64.sub (63:BV64.t) left_bv) = BV64.of_int (63 - left) };
begin
ensures { forall i:BV64.t. BV64.ule i (BV64.of_int 63) ->
i <> BV64.sub (BV64.of_int 63) left_bv ->
ensures { forall i:BV64.t. BV64.ule i (63:BV64.t) ->
i <> BV64.sub (63:BV64.t) left_bv ->
BV64.nth_bv result i = BV64.nth_bv value i }
ensures { flag = BV64.nth_bv result (BV64.sub (BV64.of_int 63) left_bv) }
ensures { flag = BV64.nth_bv result (BV64.sub (63:BV64.t) left_bv) }
let mask =
BV64.lsl_bv (1:BV64.t) (BV64.of_int (63 - left))
in
......@@ -99,11 +99,11 @@ module Bitwalker
requires { 0 <= BV32.t'int left < 8 }
ensures { result = BV8.nth byte (7 - BV32.t'int left) }
=
assert {BV32.ult left (BV32.of_int 8)};
assert {BV32.ult left (8:BV32.t)};
begin
ensures {
result = BV8.nth_bv
byte (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))}
byte (BV8.sub (7:BV8.t) (C8_32.toSmall left))}
let mask =
BV32.lsl_bv (1:BV32.t) (BV32.sub_check (7:BV32.t) left)
in
......@@ -140,7 +140,7 @@ module Bitwalker
let retval = ref BV64.zeros in
let i = ref BV32.zeros in
let lstart = BV32.sub_check (BV32.of_int 64) len in
let lstart = BV32.sub_check (64:BV32.t) len in
while BV32.ult !i len do variant{ BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
......@@ -167,10 +167,10 @@ module Bitwalker
requires {BV32.t'int left < 64}
ensures {result = BV64.nth value (63 - BV32.t'int left)}
=
assert {BV32.ult left (BV32.of_int 64)};
assert {BV32.ult left (64:BV32.t)};
begin
ensures {result = BV64.nth_bv value
(BV64.sub (BV64.of_int 63) (C32_64.toBig left))}
(BV64.sub (63:BV64.t) (C32_64.toBig left))}
let mask = BV64.lsl_bv (1:BV64.t)
(C32_64.toBig (BV32.sub_check (63:BV32.t) left)) in
not (BV64.eq (BV64.bw_and value mask) BV64.zeros)
......@@ -192,13 +192,13 @@ module Bitwalker
BV8.nth result i = BV8.nth byte i }
ensures { BV8.nth result (7 - BV32.t'int left) = flag }
=
assert { BV32.ult left (BV32.of_int 8) };
assert { BV32.ult left (8:BV32.t) };
begin
ensures { forall i:BV32.t. BV32.ult i (BV32.of_int 8) ->
i <> BV32.sub (BV32.of_int 7) left ->
ensures { forall i:BV32.t. BV32.ult i (8:BV32.t) ->
i <> BV32.sub (7:BV32.t) left ->
BV8.nth_bv result (C8_32.toSmall i)
= BV8.nth_bv byte (C8_32.toSmall i) }
ensures { BV8.nth_bv result (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))
ensures { BV8.nth_bv result (BV8.sub (7:BV8.t) (C8_32.toSmall left))
= flag }
let mask = BV8.lsl_bv (1:BV8.t) (BV8.sub_check (7:BV8.t) (C8_32.toSmall left)) in
match flag with
......@@ -251,7 +251,7 @@ module Bitwalker
-2 (*error: value_too_big*)
else
let lstart = BV32.sub_check (BV32.of_int 64) len in
let lstart = BV32.sub_check (64:BV32.t) len in
let i = ref BV32.zeros in
while BV32.ult !i len do variant { BV32.t'int len - BV32.t'int !i }
......
......@@ -3,6 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.7.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="12" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitwalker.mlw" proved="true">
......@@ -16,13 +19,15 @@
<goal name="VC nth_ultpre0" expl="VC for nth_ultpre0" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC nth_ultpre0.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="166"/></proof>
<proof prover="11"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC nth_ultpre0.1" expl="assertion" proved="true">
<proof prover="12"><result status="valid" time="0.08"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC nth_ultpre0.2" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.58"/></proof>
<proof prover="2"><result status="valid" time="0.10" steps="512"/></proof>
<proof prover="11"><result status="valid" time="0.65"/></proof>
</goal>
</transf>
</goal>
......@@ -35,16 +40,16 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke_64bit_bv.2" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.12"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC poke_64bit_bv.3" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC poke_64bit_bv.4" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC poke_64bit_bv.5" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.12"/></proof>
<proof prover="11"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
......@@ -60,10 +65,10 @@
<proof prover="12"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC poke_64bit.3" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC poke_64bit.4" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC poke_64bit.5" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
......@@ -79,7 +84,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek_8bit_bv.2" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC peek_8bit_bv.3" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.05"/></proof>
......@@ -123,10 +128,10 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek.5" expl="loop invariant init" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC peek.6" expl="loop invariant init" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="185"/></proof>
</goal>
<goal name="VC peek.7" expl="loop invariant init" proved="true">
<proof prover="11"><result status="valid" time="0.02"/></proof>
......@@ -138,13 +143,13 @@
<proof prover="12"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC peek.10" expl="precondition" proved="true">
<proof prover="11"><result status="valid" time="0.08"/></proof>
<proof prover="11"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC peek.11" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek.12" expl="precondition" proved="true">
<proof prover="11"><result status="valid" time="0.06"/></proof>
<proof prover="11"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC peek.13" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
......@@ -153,13 +158,13 @@
<proof prover="12"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC peek.15" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.16"/></proof>
<proof prover="11"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC peek.16" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="1.36"/></proof>
<proof prover="11"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="VC peek.17" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.12"/></proof>
<proof prover="2"><result status="valid" time="0.25" steps="651"/></proof>
</goal>
<goal name="VC peek.18" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
......@@ -168,7 +173,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek.20" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.06"/></proof>
<proof prover="11"><result status="valid" time="0.22"/></proof>
</goal>
</transf>
</goal>
......@@ -181,7 +186,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC peek_64bit.2" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC peek_64bit.3" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.41"/></proof>
......@@ -194,13 +199,13 @@
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke_8bit.1" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC poke_8bit.2" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC poke_8bit.3" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC poke_8bit.4" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.07"/></proof>
......@@ -232,17 +237,17 @@
<goal name="VC poke_8bit_array.5.0" expl="postcondition" proved="true">
<transf name="case" proved="true" arg1="(div i 8 = o)">
<goal name="VC poke_8bit_array.5.0.0" expl="true case (postcondition)" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="258"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="267"/></proof>
</goal>
<goal name="VC poke_8bit_array.5.0.1" expl="false case (postcondition)" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="176"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="181"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC poke_8bit_array.6" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="169"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="174"/></proof>
</goal>
</transf>
</goal>
......@@ -273,7 +278,7 @@
<proof prover="12"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC poke.8" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.18"/></proof>
<proof prover="11"><result status="valid" time="0.26"/></proof>
</goal>