Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
3a2d2ca9
Commit
3a2d2ca9
authored
Jan 28, 2016
by
Clément Fumex
Browse files
change zero to zeros in bv theory
parent
590a8eb5
Changes
16
Hide whitespace changes
Inline
Side-by-side
drivers/smt-libv2-bv-realization.gen
View file @
3a2d2ca9
...
...
@@ -33,7 +33,7 @@ theory bv.BV_Gen
remove prop size_pos
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_zero
s
remove prop Nth_ones
remove prop Nth_bw_and
remove prop Nth_bw_or
...
...
@@ -41,13 +41,13 @@ theory bv.BV_Gen
remove prop Nth_bw_not
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop lsr_zero
remove prop lsr_zero
s
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop asr_zero
remove prop asr_zero
s
remove prop Lsl_nth_high
remove prop Lsl_nth_low
remove prop lsl_zero
remove prop lsl_zero
s
remove prop Nth_rotate_right
remove prop Nth_rotate_left
...
...
@@ -62,7 +62,7 @@ theory bv.BV_Gen
remove prop to_uint_bounds
remove prop to_uint_of_int
remove prop Of_int_zero
remove prop Of_int_zero
s
remove prop Of_int_ones
(** Arithmetic operators *)
...
...
@@ -105,7 +105,7 @@ end
theory bv.BV64
syntax type t "(_ BitVec 64)"
syntax function zero "#x0000000000000000"
syntax function zero
s
"#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function nth_bv
...
...
@@ -121,7 +121,7 @@ end
theory bv.BV32
syntax type t "(_ BitVec 32)"
syntax function zero "#x00000000"
syntax function zero
s
"#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function nth_bv
...
...
@@ -134,7 +134,7 @@ end
theory bv.BV16
syntax type t "(_ BitVec 16)"
syntax function zero "#x0000"
syntax function zero
s
"#x0000"
syntax function ones "#xFFFF"
syntax function nth_bv
...
...
@@ -147,7 +147,7 @@ end
theory bv.BV8
syntax type t "(_ BitVec 8)"
syntax function zero "#x00"
syntax function zero
s
"#x00"
syntax function ones "#xFF"
syntax function nth_bv
...
...
drivers/smt-libv2-bv.gen
View file @
3a2d2ca9
...
...
@@ -24,7 +24,7 @@ theory bv.BV_Gen
remove prop size_pos
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_zero
s
remove prop Nth_ones
remove prop two_power_size_val
remove prop max_int_val
...
...
@@ -34,13 +34,13 @@ theory bv.BV_Gen
remove prop Nth_bw_not
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop lsr_zero
remove prop lsr_zero
s
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop asr_zero
remove prop asr_zero
s
remove prop Lsl_nth_low
remove prop Lsl_nth_high
remove prop lsl_zero
remove prop lsl_zero
s
remove prop Nth_rotate_left
remove prop Nth_rotate_right
...
...
@@ -48,7 +48,7 @@ theory bv.BV_Gen
remove prop to_uint_bounds
remove prop to_int_extensionality
remove prop Of_int_zero
remove prop Of_int_zero
s
remove prop Of_int_ones
remove prop to_uint_add
...
...
@@ -78,7 +78,7 @@ end
theory bv.BV64
syntax type t "(_ BitVec 64)"
syntax function zero "#x0000000000000000"
syntax function zero
s
"#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
...
...
@@ -88,7 +88,7 @@ end
theory bv.BV32
syntax type t "(_ BitVec 32)"
syntax function zero "#x00000000"
syntax function zero
s
"#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
...
...
@@ -98,7 +98,7 @@ end
theory bv.BV16
syntax type t "(_ BitVec 16)"
syntax function zero "#x0000"
syntax function zero
s
"#x0000"
syntax function ones "#xFFFF"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
...
...
@@ -108,7 +108,7 @@ end
theory bv.BV8
syntax type t "(_ BitVec 8)"
syntax function zero "#x00"
syntax function zero
s
"#x00"
syntax function ones "#xFF"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
...
...
examples/bitcount.mlw
View file @
3a2d2ca9
...
...
@@ -8,7 +8,7 @@ module BitCount8bit_fact
function nth_as_bv (a i : t) : t =
if nth_bv a i
then (of_int 1)
else zero
else zero
s
function nth_as_int (a : t) (i : int) : int =
if nth a i
...
...
@@ -328,8 +328,8 @@ module AsciiCode
let lemma bv_even (b:t)
ensures { even (to_uint b) <-> not (nth b 0) }
=
assert { not (nth_bv b zero) <-> b = mul (of_int 2) (lsr_bv b one) };
assert { (exists k. b = mul (of_int 2) k) -> not (nth_bv b zero) };
assert { not (nth_bv b zero
s
) <-> b = mul (of_int 2) (lsr_bv b one) };
assert { (exists k. b = mul (of_int 2) k) -> not (nth_bv b zero
s
) };
assert { (exists k. to_uint b = 2 * k) -> (exists k. b = mul (of_int 2) k) };
assert { not (nth b 0) <-> to_uint b = 2 * to_uint (lsr b 1) }
...
...
@@ -350,7 +350,7 @@ module AsciiCode
numof_or p q a (b-1)
let lemma count_or (b c : t)
requires { bw_and b c = zero }
requires { bw_and b c = zero
s
}
ensures { count_logic (bw_or b c) = count_logic b + count_logic c }
=
assert { forall i. ult i size_bv ->
...
...
@@ -366,16 +366,16 @@ module AsciiCode
number is odd, set the 8th bit to 1 if not, do nothing:*)
let ascii (b : t) =
requires { not (nth_bv b lastbit) }
ensures { eq_sub_bv result b zero lastbit }
ensures { eq_sub_bv result b zero
s
lastbit }
ensures { validAscii result }
let c = count b in
let maskbit = lsl_check c lastbit in
assert { bw_and b maskbit = zero };
assert { bw_and b maskbit = zero
s
};
assert { even (to_uint c) ->
not (nth_bv c zero)
not (nth_bv c zero
s
)
&& count_logic maskbit = 0 };
assert { odd (to_uint c) ->
nth_bv c zero
nth_bv c zero
s
&& nth maskbit 31
&& (forall i. 0 <= i < 31 -> not (nth maskbit i))
&& count_logic maskbit = 1 };
...
...
@@ -458,7 +458,7 @@ module GrayCode
assert { b <> ones -> toGray (add b one) = bw_xor (toGray b) (bw_and (bw_not b) (add b one)) };
assert { b <> ones -> exists k. (bw_and (bw_not b) (add b one)) = lsl one k };
assert { b <> ones -> count_logic (bw_and (bw_not b) (add b one)) = 1 };
assert { b = ones -> (toGray b) = of_int 0x80000000 /\ (toGray (add b one)) = zero }
assert { b = ones -> (toGray b) = of_int 0x80000000 /\ (toGray (add b one)) = zero
s
}
(** Now, a couple of property between the Gray code and the binary
representation.
...
...
@@ -488,7 +488,7 @@ module GrayCode
encoding has an odd number of 1-bits. *)
lemma evenOdd : forall b.
nth_bv b zero <-> even (count_logic (toGray b))
nth_bv b zero
s
<-> even (count_logic (toGray b))
end
...
...
examples/bitvector_examples.mlw
View file @
3a2d2ca9
...
...
@@ -94,7 +94,7 @@ theory Hackers_delight
bw_not( sub x y ) = add (bw_not x) y
goal DMtest: forall x.
zero = bw_not( bw_or x (neg( add x (of_int 1))))
zero
s
= bw_not( bw_or x (neg( add x (of_int 1))))
(* inequality *)
...
...
@@ -112,7 +112,7 @@ theory Hackers_delight
(* shift right and arithmetic shift right *)
goal SR1: forall x n. ( ule zero n /\ ule n (of_int 31)) ->
goal SR1: forall x n. ( ule zero
s
n /\ ule n (of_int 31)) ->
bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (of_int 31) )) (sub (of_int 31) n))
= asr_bv x n
...
...
@@ -129,12 +129,12 @@ theory Hackers_delight
goal BP1: forall a b c d x y.
( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
( ule b (add b d) /\ ule d (add b d) ) -> (* no overflow in addition *)
ule (bw_or x y) (add b d) /\ ule zero (bw_and x y)
ule (bw_or x y) (add b d) /\ ule zero
s
(bw_and x y)
goal BP2: forall a b c d x y.
( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
( ule b (add b d) /\ ule d (add b d) ) -> (* no overflow in addition *)
ule zero (bw_xor x y) /\ ule (bw_xor x y) (add b d)
ule zero
s
(bw_xor x y) /\ ule (bw_xor x y) (add b d)
goal BP3: forall a b c d x y.
( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->
...
...
@@ -181,7 +181,7 @@ module Hackers_delight_mod
bw_not( sub x y )
let dmtest (x : t) =
ensures{ result = zero }
ensures{ result = zero
s
}
bw_not( bw_or x (neg( add x (of_int 1))))
(* inequality *)
...
...
@@ -207,7 +207,7 @@ module Hackers_delight_mod
(* shift right and arithmetic shift right *)
let sr1 (x : t) (n : t) =
requires{ ule zero n /\ ule n (of_int 31) }
requires{ ule zero
s
n /\ ule n (of_int 31) }
ensures{ result = asr_bv x n }
bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (of_int 31) )) (sub (of_int 31) n))
...
...
@@ -234,14 +234,14 @@ module Hackers_delight_mod
requires{ ule a x /\ ule x b }
requires{ ule c y /\ ule y d }
requires{ ule b (add b d) /\ ule d (add b d) } (* no overflow in addition *)
ensures{ ule zero result }
ensures{ ule zero
s
result }
bw_and x y
let bp2 (a b c d x y : t) =
requires{ ule a x /\ ule x b }
requires{ ule c y /\ ule y d }
requires{ ule b (add b d) /\ ule d (add b d) } (* no overflow in addition *)
ensures{ ule zero result }
ensures{ ule zero
s
result }
ensures{ ule result (add b d) }
bw_xor x y
...
...
@@ -264,7 +264,7 @@ module Test_imperial_violet
(* to_int and bounds *)
lemma bv32_bounds_bv:
forall b. ule zero b /\ ule b ones
forall b. ule zero
s
b /\ ule b ones
lemma to_int_ule:
forall b c. ule b c -> to_uint b <= to_uint c
...
...
@@ -288,7 +288,7 @@ module Test_imperial_violet
ult b[i] (of_int 0x8000_0000) }
ensures{ forall i. 0 <= i < length result ->
to_uint result[i] = to_uint a[i] + to_uint b[i] }
let sum = make (length a) zero in
let sum = make (length a) zero
s
in
for i = 0 to length a - 1 do
invariant{ forall j. 0 <= j < i -> sum[j] = add a[j] b[j] }
invariant{ forall j. 0 <= j < i -> to_uint sum[j] = to_uint a[j] + to_uint b[j] }
...
...
@@ -304,7 +304,7 @@ module Test_from_bitvector_example
use import bv.BV32
goal Test1:
let b = bw_and zero ones in nth_bv b (of_int 1) = False
let b = bw_and zero
s
ones in nth_bv b (of_int 1) = False
goal Test2:
let b = lsr_bv ones (of_int 16) in nth_bv b (of_int 15) = True
...
...
examples/bitwalker.mlw
View file @
3a2d2ca9
...
...
@@ -32,11 +32,11 @@ module Bitwalker
let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
requires { BV32.to_uint len < 64}
ensures { BV64.eq_sub x BV64.zero (BV32.to_uint len) (64 - BV32.to_uint len)
ensures { BV64.eq_sub x BV64.zero
s
(BV32.to_uint len) (64 - BV32.to_uint len)
<-> BV64.to_uint x < BV64.to_uint (maxvalue len) }
=
assert { BV32.ult len (BV32.of_int 64) };
assert { BV64.eq_sub_bv x BV64.zero (C32_64.toBig len) (BV64.sub (BV64.of_int 64) (C32_64.toBig len))
assert { BV64.eq_sub_bv x BV64.zero
s
(C32_64.toBig len) (BV64.sub (BV64.of_int 64) (C32_64.toBig len))
<-> BV64.ult x (maxvalue len) }
(** return [value] with the bit of index [left] from the left set to [flag] *)
...
...
@@ -106,7 +106,7 @@ module Bitwalker
let mask =
BV32.lsl_bv (BV32.int_check 1) (BV32.sub_check (BV32.int_check 7) left)
in
BV32.bw_and (C8_32.toBig byte) mask <> BV32.zero
BV32.bw_and (C8_32.toBig byte) mask <> BV32.zero
s
end
(* return the bit of the [left]/8 element of [addr] at position mod [left] 8 starting from the left *)
...
...
@@ -124,7 +124,7 @@ module Bitwalker
requires { BV32.to_uint start + BV32.to_uint len < BV32.two_power_size }
requires { 8 * length addr < BV32.two_power_size }
ensures { BV32.to_uint start + BV32.to_uint len > (8 * length addr) ->
result = BV64.zero }
result = BV64.zero
s
}
ensures { BV32.to_uint start + BV32.to_uint len <= (8 * length addr) ->
(forall i:int. 0 <= i < BV32.to_uint len ->
BV64.nth result i
...
...
@@ -134,11 +134,11 @@ module Bitwalker
=
if (BV32.to_uint (BV32.add_check start len) > ( 8 *length addr ))
then
BV64.zero
BV64.zero
s
else
let retval = ref BV64.zero in
let i = ref BV32.zero in
let retval = ref BV64.zero
s
in
let i = ref BV32.zero
s
in
let lstart = BV32.sub_check (BV32.of_int 64) len in
while BV32.ult !i len do variant{ !i with BV32.ugt }
...
...
@@ -172,7 +172,7 @@ module Bitwalker
(BV64.sub (BV64.of_int 63) (C32_64.toBig left))}
let mask = BV64.lsl_bv (BV64.int_check 1)
(C32_64.toBig (BV32.sub_check (BV32.int_check 63) left)) in
BV64.bw_and value mask <> BV64.zero
BV64.bw_and value mask <> BV64.zero
s
end
(*
...
...
@@ -251,7 +251,7 @@ module Bitwalker
else
let lstart = BV32.sub_check (BV32.of_int 64) len in
let i = ref BV32.zero in
let i = ref BV32.zero
s
in
'Init:
while BV32.ult !i len do variant { !i with BV32.ugt }
...
...
examples/hackers-delight.mlw
View file @
3a2d2ca9
...
...
@@ -51,11 +51,11 @@ module Utils_Spec
(** {6 count correctness } *)
(** Let's start by checking that there are no 1-bits in the
bitvector "zero": *)
bitvector "zero
s
": *)
lemma countZero: count zero = zero
lemma countZero: count zero
s
= zero
s
lemma numOfZero: NumOf.numof (\i. nth zero i) 0 32 = 0
lemma numOfZero: NumOf.numof (\i. nth zero
s
i) 0 32 = 0
(** Now, for b a bitvector with n 1-bits, we check that if its
first bit is 0 then shifting b by one on the right doesn't
...
...
@@ -63,8 +63,8 @@ module Utils_Spec
there are n-1 1-bits in the shifting of b by one on the right. *)
lemma countStep: forall b.
(not (nth_bv b zero) <-> count (lsr_bv b one) = count b) /\
(nth_bv b zero <-> count (lsr_bv b one) = sub (count b) one)
(not (nth_bv b zero
s
) <-> count (lsr_bv b one) = count b) /\
(nth_bv b zero
s
<-> count (lsr_bv b one) = sub (count b) one)
let rec lemma numof_shift (p q : int -> bool) (a b k: int) : unit
requires {forall i. q i = p (i + k)}
...
...
@@ -78,12 +78,12 @@ module Utils_Spec
variant {bv with ult}
ensures {to_uint (count bv) = NumOf.numof (nth bv) 0 32}
=
if bv = zero then ()
if bv = zero
s
then ()
else
begin
countSpec_Aux (lsr_bv bv one);
assert {
let x = (if nth_bv bv zero then 1 else 0) in
let x = (if nth_bv bv zero
s
then 1 else 0) in
let f = nth bv in
let g = nth (lsr_bv bv one) in
let h = \i. nth bv (i+1) in
...
...
@@ -117,7 +117,7 @@ module Utils_Spec
lemma symmetric: forall a b. hammingD a b = hammingD b a
lemma separation: forall a b. hammingD a b = zero <-> a = b
lemma separation: forall a b. hammingD a b = zero
s
<-> a = b
function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x
...
...
@@ -160,7 +160,7 @@ module Hackers_delight
(** A ascii character is valid if its number of bits is even.
(Remember that a binary number is odd if and only if its first
bit is 1) *)
predicate validAscii (b : t) = (nth_bv (count b) zero) = False
predicate validAscii (b : t) = (nth_bv (count b) zero
s
) = False
(** The ascii checksum aim is to make any character valid in the
sens that we just defined. One way to implement it is to count
...
...
@@ -181,7 +181,7 @@ module Hackers_delight
will be invalid, hence the validity of the encoding. *)
lemma asciiProp: forall a b.
((validAscii a /\ not validAscii b) \/ (validAscii b /\ not
validAscii a)) <-> nth_bv (hammingD a b) zero
validAscii a)) <-> nth_bv (hammingD a b) zero
s
(** {2 Gray code}
Gray codes are bit-wise representations of integers with the
...
...
@@ -239,14 +239,14 @@ module Hackers_delight
lemma nthBinary: forall b i.
ult i size_bv ->
nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zero
nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zero
s
(** The last property that we check is that if an integer is even
its encoding has an even number of 1-bits, and if it is odd, its
encoding has an odd number of 1-bits. *)
lemma evenOdd : forall b.
nth_bv b zero <-> nth_bv (count (toGray b)) zero
nth_bv b zero
s
<-> nth_bv (count (toGray b)) zero
s
(** {2 Various (in)equalities between bitvectors. } *)
...
...
@@ -279,7 +279,7 @@ module Hackers_delight
bw_not( sub x y ) = add (bw_not x) y
lemma DMtest: forall x.
zero = bw_not( bw_or x (neg( add x (of_int 1))))
zero
s
= bw_not( bw_or x (neg( add x (of_int 1))))
(** {6 Addition Combined with Logical Operations (p.16)} *)
...
...
@@ -364,8 +364,8 @@ module Hackers_delight
( ule a x /\ ule x b /\ ule c y /\ ule y d ) -> (* a <= x <= b and c <= y <= d *)
addDontOverflow b d ->
ule (max a c) (bw_or x y) /\ ule (bw_or x y) (add b d) /\ (* max a c <= x | y <= b + d *)
ule zero (bw_and x y) /\ ule (bw_and x y) (min b d) /\
(* 0 <= x & y <= min b d *)
ule zero (bw_xor x y) /\ ule (bw_xor x y) (add b d) /\
(* 0 <= x xor y <= b + d *)
ule zero
s
(bw_and x y) /\ ule (bw_and x y) (min b d) /\ (* 0 <= x & y <= min b d *)
ule zero
s
(bw_xor x y) /\ ule (bw_xor x y) (add b d) /\ (* 0 <= x xor y <= b + d *)
ule (bw_not b) (bw_not x) /\ ule (bw_not x) (bw_not a) (* not b <= not x <= not a *)
end
examples/queens_bv.mlw
View file @
3a2d2ca9
...
...
@@ -152,13 +152,13 @@ module Bits "the 1-bits of an integer, as a set of integers"
let empty () : t
ensures { is_empty result.mdl }
=
{ bv = zero; mdl = empty }
{ bv = zero
s
; mdl = empty }
let is_empty (x:t) : bool
ensures { result <-> is_empty x.mdl }
=
assert {is_empty x.mdl -> BV32.eq x.bv zero};
x.bv = zero
assert {is_empty x.mdl -> BV32.eq x.bv zero
s
};
x.bv = zero
s
let remove_singleton (a b: t) : t
requires { b.mdl = singleton (min_elt b.mdl) }
...
...
@@ -195,14 +195,14 @@ module Bits "the 1-bits of an integer, as a set of integers"
{ bv = bw_and a.bv (bw_not b.bv);
mdl = diff a.mdl b.mdl }
predicate bits_interval_is_zero_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) =
eq_sub_bv a zero i n
predicate bits_interval_is_zero
s
_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) =
eq_sub_bv a zero
s
i n
predicate bits_interval_is_one_bv (a:BV32.t) (i:BV32.t) (n:BV32.t) =
eq_sub_bv a ones i n
predicate bits_interval_is_zero (a:BV32.t) (i : int) (n : int) =
eq_sub a zero i n
predicate bits_interval_is_zero
s
(a:BV32.t) (i : int) (n : int) =
eq_sub a zero
s
i n
predicate bits_interval_is_one (a:BV32.t) (i : int) (n : int) =
eq_sub a ones i n
...
...
@@ -213,13 +213,13 @@ module Bits "the 1-bits of an integer, as a set of integers"
=
let ghost n = min_elt a.mdl in
let ghost n_bv = of_int n in
assert {bits_interval_is_zero_bv a.bv zero n_bv};
assert {bits_interval_is_zero
s
_bv a.bv zero
s
n_bv};
assert {nth_bv a.bv n_bv};
assert {nth_bv (neg a.bv) n_bv};
let res = bw_and a.bv (neg a.bv) in
assert {forall i. 0 <= i < n -> not (nth res i)};
assert {bits_interval_is_zero_bv res (add n_bv (of_int 1)) (sub (of_int 31) n_bv )};
assert {bits_interval_is_zero res (n + 1) (31 - n)};
assert {bits_interval_is_zero
s
_bv res (add n_bv (of_int 1)) (sub (of_int 31) n_bv )};
assert {bits_interval_is_zero
s
res (n + 1) (31 - n)};
{ bv = res;
mdl = singleton n }
...
...
examples/queens_bv/why3session.xml
View file @
3a2d2ca9
...
...
@@ -106,7 +106,7 @@
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
</theory>
<theory
name=
"NQueensBits"
sum=
"
8c27bb54fc3d9e15efa7c17b4978a559
"
>
<theory
name=
"NQueensBits"
sum=
"
a825c274c9dc4b1ad2af530c895eda81
"
>
<goal
name=
"WP_parameter t"
expl=
"VC for t"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"WP_parameter t.1"
expl=
"1. assertion"
>
...
...
@@ -353,11 +353,6 @@
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"nth"
/>
</ls_pos>
<ls_pos
name=
"zero"
id=
"4945"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"zero"
/>
</ls_pos>
<ls_pos
name=
"ones"
id=
"4948"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
...
...
@@ -1208,11 +1203,6 @@
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"nth_out_of_bound"
/>
</pr_pos>
<pr_pos
name=
"Nth_zero"
id=
"4946"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"Nth_zero"
/>
</pr_pos>
<pr_pos
name=
"Nth_ones"
id=
"4949"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
...
...
@@ -1248,11 +1238,6 @@
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"Lsr_nth_high"
/>
</pr_pos>
<pr_pos
name=
"lsr_zero"
id=
"4988"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"lsr_zero"
/>
</pr_pos>
<pr_pos
name=
"Asr_nth_low"
id=
"4992"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
...
...
@@ -1263,11 +1248,6 @@
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"Asr_nth_high"
/>
</pr_pos>
<pr_pos
name=
"asr_zero"
id=
"5002"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"asr_zero"
/>
</pr_pos>
<pr_pos
name=
"Lsl_nth_high"
id=
"5006"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
...
...
@@ -1278,11 +1258,6 @@
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"Lsl_nth_low"
/>
</pr_pos>
<pr_pos
name=
"lsl_zero"
id=
"5016"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
<ip_qualid
name=
"lsl_zero"
/>
</pr_pos>
<pr_pos
name=
"Nth_rotate_right"
id=
"5020"
ip_theory=
"BV32"
>
<ip_library
name=
"bv"
/>
...
...
@@ -1502,9 +1477,6 @@
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"4940"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"4945"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"4948"
/>
</meta>
...
...
@@ -2012,9 +1984,6 @@
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"4941"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"4946"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"4949"
/>
</meta>
...
...
@@ -2036,27 +2005,18 @@
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"4983"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"4988"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"4992"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"4997"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"5002"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"5006"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"5011"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"5016"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"5020"
/>
</meta>
...
...
@@ -2211,7 +2171,7 @@
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.29"
/></proof>
</goal>
<goal
name=
"WP_parameter t.22.2"
expl=
"2. assertion"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"
6.28
"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"
7.04
"
/></proof>
</goal>
</transf>
</goal>
...
...
@@ -2219,7 +2179,7 @@
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.09"
/></proof>
</goal>
<goal
name=
"WP_parameter t.24"
expl=
"24. assertion"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"1.
15
"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"1.
47
"
/></proof>
</goal>
<goal
name=
"WP_parameter t.25"
expl=
"25. precondition"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.10"
/></proof>
...
...
@@ -2296,7 +2256,7 @@
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.15"
/></proof>
</goal>
<goal
name=
"WP_parameter t.48.2"
expl=
"2. loop invariant preservation"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"2.
31
"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"2.
76
"
/></proof>
</goal>
<goal
name=
"WP_parameter t.48.3"
expl=
"3. loop invariant preservation"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.29"
/></proof>
...
...
@@ -2315,8 +2275,8 @@
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.11"
/></proof>
</goal>
<goal
name=
"WP_parameter t.49.3"
expl=
"3. loop invariant preservation"
>
<proof
prover=
"3"
timelimit=
"60"
><result
status=
"valid"
time=
"
32.07
"
/></proof>
<proof
prover=
"6"
timelimit=
"60"
><result
status=
"valid"
time=
"
5.64
"
/></proof>
<proof
prover=
"3"
timelimit=
"60"
><result
status=
"valid"
time=
"
43.41
"
/></proof>
<proof
prover=
"6"
timelimit=
"60"
><result
status=
"valid"
time=
"
8.49
"
/></proof>