Skip to content

GitLab

Commit 6e6251a4 authored by Stefan Berghofer's avatar Stefan Berghofer
Browse files

Merge branch 'master'

parents bc646df4 ffd0d006
Expand all Hide whitespace changes
Inline Side-by-side
AUTHORS
View file @ 6e6251a4
......@@ -22,4 +22,3 @@ with contributions of
Asma Tafat
Piotr Trojanek
Makarius Wenzel
LICENSE
View file @ 6e6251a4
......@@ -14,6 +14,10 @@ of the Library that is distributed under the conditions defined in clause
however invalidate any other reasons why the executable file might be
covered by the GNU Lesser General Public License.
The files src/util/extmap.ml{i} are derived from the sources of
OCaml 3.12 standard library, and are distributed under the GNU
LGPL version 2 (see file OCAML-LICENSE).
Icon sets for the graphical interface of Why3 are subject to specific
licenses, some of them may forbid commercial usage. These specific
licenses are detailed in files share/icons/*/*.txt
......
Makefile.in
View file @ 6e6251a4
......@@ -81,12 +81,13 @@ INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
# 41 Ambiguous constructor or label name.
# 44 Open statement shadows an already defined identifier.
# 45 Open statement shadows an already defined label or constructor.
# 50 Unexpected documentation comment.
# - fatal:
# 5 Partially applied function: expression whose result has function
# type and is ignored.
# 48 Implicit elimination of optional arguments.
WARNINGS = A-4-9-41-44-45@5@48
WARNINGS = A-4-9-41-44-45-50@5@48
OFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
......
README
View file @ 6e6251a4
......@@ -42,6 +42,10 @@ The files src/util/extmap.ml{i} are derived from the sources of
OCaml 3.12 standard library, and are distributed under the GNU
LGPL version 2 (see file OCAML-LICENSE).
Icon sets for the graphical interface of Why3 are subject to specific
licenses, some of them may forbid commercial usage. These specific
licenses are detailed in files share/icons/*/*.txt
INSTALLATION
============
......
drivers/smt-libv2-bv.gen
View file @ 6e6251a4
......@@ -23,6 +23,8 @@ theory bv.BV_Gen
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_ones
remove prop two_power_size_val
remove prop max_int_val
remove prop eq_sub_equiv
remove prop Extensionality
remove prop Nth_bw_or
......@@ -104,6 +106,11 @@ theory bv.BV8
syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
end
theory bv.BVConverter_Gen
remove prop toSmall_to_uint
remove prop toBig_to_uint
end
theory bv.BVConverter_32_64
syntax function toBig "((_ zero_extend 32) %1)"
syntax function toSmall "((_ extract 31 0) %1)"
......
examples/binary_search/why3session.xml
View file @ 6e6251a4
......@@ -23,7 +23,7 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="b0206e6010f9baba3c77f13cd10417bd" expanded="true">
<theory name="BinarySearchInt32" sum="1532a4c6a55e25e07cb0fa8426dc924c" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
......@@ -33,7 +33,7 @@
<proof prover="5"><result status="valid" time="0.01" steps="75"/></proof>
</goal>
<goal name="WP_parameter binary_search.3" expl="3. integer overflow">
<proof prover="5"><result status="valid" time="0.12" steps="94"/></proof>
<proof prover="5"><result status="valid" time="0.12" steps="95"/></proof>
</goal>
<goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
<proof prover="5"><result status="valid" time="0.01" steps="76"/></proof>
......@@ -54,10 +54,10 @@
<proof prover="5"><result status="valid" time="0.04" steps="99"/></proof>
</goal>
<goal name="WP_parameter binary_search.10" expl="10. integer overflow">
<proof prover="5"><result status="valid" time="0.11" steps="116"/></proof>
<proof prover="5"><result status="valid" time="0.11" steps="117"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="5"><result status="valid" time="0.27" steps="136"/></proof>
<proof prover="5"><result status="valid" time="0.27" steps="138"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="5"><result status="valid" time="0.01" steps="91"/></proof>
......@@ -74,7 +74,7 @@
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="1.36" steps="180"/></proof>
<proof prover="5"><result status="valid" time="1.36" steps="182"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="99"/></proof>
......@@ -94,7 +94,7 @@
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="1.31" steps="181"/></proof>
<proof prover="5"><result status="valid" time="1.31" steps="183"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="5"><result status="valid" time="0.02" steps="101"/></proof>
......
examples/in_progress/bitcount.mlw → examples/bitcount.mlw
View file @ 6e6251a4
(* module BitCountSpec_2 *)
(* use import bv.BV32 *)
(* use import int.NumOf *)
(* function count_logic (a : t) : int *)
(* val count (bv:t) : t *)
(* ensures { to_uint result = count__logic bv } *)
(* end *)
module BitCount8bit_fact
use import int.Int
use import int.NumOf
use import mach.bv.BVCheck8
use import bv.BV8
use import ref.Ref
function nth_as_bv (a i : t) : t =
......@@ -95,15 +82,15 @@ module BitCount8bit_fact
=
let x = ref n in
x := sub_check !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55));
x := sub !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55));
let ghost x1 = !x in
x := add_check
x := add
(bw_and !x (of_int 0x33))
(bw_and (lsr_bv !x (of_int 2)) (of_int (0x33)));
let ghost x2 = !x in
x := bw_and (add_check !x (lsr_bv !x (of_int 4))) (of_int 0x0F);
x := bw_and (add !x (lsr_bv !x (of_int 4))) (of_int 0x0F);
prove n x1 x2 !x;
......@@ -115,7 +102,7 @@ module BitCount32bit_fact
use import int.Int
use import int.NumOf
use import mach.bv.BVCheck32
use import bv.BV32
use import ref.Ref
function count_logic (bv:t) : int = numof (nth bv) 0 32
......@@ -260,43 +247,43 @@ module BitCount32bit_fact
=
let x = ref n in
assert { ule (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555)) !x };
(* assert { ule (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555)) !x }; *)
(* x = x - ( (x >> 1) & 0x55555555) *)
x := sub_check !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555));
x := sub !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555));
let ghost x1 = !x in
assert { ule (bw_and !x (of_int 0x33333333))
(of_int 0x33333333) };
assert { ule (bw_and (lsr_bv !x (of_int 2)) (of_int (0x33333333)))
(of_int (0x33333333)) };
(* assert { ule (bw_and !x (of_int 0x33333333)) *)
(* (of_int 0x33333333) }; *)
(* assert { ule (bw_and (lsr_bv !x (of_int 2)) (of_int (0x33333333))) *)
(* (of_int (0x33333333)) }; *)
(* x = (x & 0x33333333) + ((x >> 2) & 0x33333333) *)
x := add_check
x := add
(bw_and !x (of_int 0x33333333))
(bw_and (lsr_bv !x (of_int 2)) (of_int (0x33333333)));
let ghost x2 = !x in
assert { ule !x (of_int 0x6666_6666) };
assert { ule (lsr_bv !x (of_int 4)) (of_int 0x0666_6666) };
(* assert { ule !x (of_int 0x6666_6666) }; *)
(* assert { ule (lsr_bv !x (of_int 4)) (of_int 0x0666_6666) }; *)
(* x = (x + (x >> 4)) & 0x0F0F0F0F *)
x := bw_and (add_check !x (lsr_bv !x (of_int 4))) (of_int 0x0F0F0F0F);
x := bw_and (add !x (lsr_bv !x (of_int 4))) (of_int 0x0F0F0F0F);
let ghost x3 = !x in
assert {ult !x (of_int 0x0F0F0F0F)};
assert {ult (lsr_bv !x (of_int 8)) (of_int 0x000F0F0F)};
assert {uint_in_range 0x0F0F0F0F /\ uint_in_range 0x000F0F0F};
(* assert {ult !x (of_int 0x0F0F0F0F)}; *)
(* assert {ult (lsr_bv !x (of_int 8)) (of_int 0x000F0F0F)}; *)
(* assert {uint_in_range 0x0F0F0F0F /\ uint_in_range 0x000F0F0F}; *)
(* x = x + (x >> 8) *)
x := add_check !x (lsr_bv !x (of_int 8));
x := add !x (lsr_bv !x (of_int 8));
let ghost x4 = !x in
assert {ult !x (of_int 0x0F000000)};
assert {ult (lsr_bv !x (of_int 8)) (of_int 0x000F0000)};
(* assert {ult !x (of_int 0x0F000000)}; *)
(* assert {ult (lsr_bv !x (of_int 8)) (of_int 0x000F0000)}; *)
(* x = x + (x >> 16) *)
x := add_check !x (lsr_bv !x (of_int 16));
x := add !x (lsr_bv !x (of_int 16));
prove n x1 x2 x3 x4 !x;
......@@ -363,9 +350,9 @@ module AsciiCode
use import BitCount32bit_fact
constant one : t = of_int 1
constant lastbit : t = sub size one
constant lastbit : t = sub size_bv one
(* let lastbit () = (sub_check size one) : t *)
(* let lastbit () = (sub_check size_bv one) : t *)
(** {2 ASCII cheksum }
In the beginning the encoding of an ascii character was done on 8
......@@ -410,7 +397,7 @@ module AsciiCode
requires { bw_and b c = zero }
ensures { count_logic (bw_or b c) = count_logic b + count_logic c }
=
assert { forall i. ult i size ->
assert { forall i. ult i size_bv ->
not (nth_bv b i) \/ not (nth_bv c i) };
assert { forall i. not (nth_bv b (of_int i)) \/ not (nth_bv c (of_int i))
-> not (nth b i) \/ not (nth c i) };
......@@ -474,7 +461,7 @@ module GrayCode
use Hamming
constant one : t = of_int 1
constant lastbit : t = sub size one
constant lastbit : t = sub size_bv one
(** {2 Gray code}
Gray codes are bit-wise representations of integers with the
......@@ -535,7 +522,7 @@ module GrayCode
integer *)
lemma nthBinary: forall b i.
ult i size ->
ult i size_bv ->
nth_bv (fromGray b) i <-> even (count_logic (lsr_bv b i))
(** The last property that we check is that if an integer is even
......
examples/bitvector_examples/why3session.xml
View file @ 6e6251a4
......@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="1aca3c7bef635dbd5aecf175ff827b71" expanded="true">
<theory name="Test_proofinuse" sum="6fb94f39a17f6d336d37a4eb24fc9921" expanded="true">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter shift_is_div.1" expl="1. assertion" expanded="true">
......@@ -36,11 +36,11 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="ttt" expanded="true">
<proof prover="0"><result status="valid" time="0.91" steps="706"/></proof>
<proof prover="0"><result status="valid" time="0.91" steps="754"/></proof>
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="36d4b67a06ae48dc17c7462056da280d" expanded="true">
<theory name="Hackers_delight" sum="2139469570f2b3a43db49a99fd43c918" expanded="true">
<goal name="DM1" expanded="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -103,7 +103,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" sum="67f9a61e4ed788c2b8acae3d1081c0e0" expanded="true">
<theory name="Hackers_delight_mod" sum="df93f6196fe77d1d941fdbcbcaace732" expanded="true">
<goal name="WP_parameter dm1" expl="VC for dm1" expanded="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -172,7 +172,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="cb6416d5f85dca726fc4b756e7e46b0c" expanded="true">
<theory name="Test_imperial_violet" sum="0916a7dc63483a6d85503c2aea8ed311" expanded="true">
<goal name="bv32_bounds_bv" expanded="true">
<proof prover="0"><result status="valid" time="0.13" steps="144"/></proof>
<proof prover="1"><result status="valid" time="0.25"/></proof>
......@@ -192,46 +192,46 @@
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="bv32_bounds" expanded="true">
<proof prover="0"><result status="valid" time="0.03" steps="74"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add" expanded="true">
<proof prover="1"><result status="valid" time="0.95"/></proof>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="5500775d7c19e733a69515bfb7464569" expanded="true">
<theory name="Test_from_bitvector_example" sum="69d7af24e60703d28350a145d0e363f9" expanded="true">
<goal name="Test1" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="98"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="101"/></proof>
<proof prover="1"><result status="valid" time="0.22"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Test2" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="134"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="109"/></proof>
<proof prover="1"><result status="valid" time="0.33"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Test3" expanded="true">
<proof prover="0"><result status="valid" time="0.06" steps="88"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="87"/></proof>
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Test4" expanded="true">
<proof prover="0"><result status="valid" time="0.04" steps="133"/></proof>
<proof prover="1"><result status="valid" time="0.36"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="113"/></proof>
<proof prover="1"><result status="valid" time="0.20"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Test5" expanded="true">
<proof prover="0"><result status="valid" time="0.06" steps="92"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="93"/></proof>
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Test6" expanded="true">
<proof prover="0"><result status="valid" time="0.06" steps="133"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="114"/></proof>
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -252,49 +252,49 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr28" expl="VC for lsr28" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.37"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr27" expl="VC for lsr27" expanded="true">
<proof prover="0"><result status="valid" time="0.18" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr26" expl="VC for lsr26" expanded="true">
<proof prover="0"><result status="valid" time="0.16" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.16" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr20" expl="VC for lsr20" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.41"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr13" expl="VC for lsr13" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr8" expl="VC for lsr8" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.51"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00000001" expanded="true">
<proof prover="0"><result status="valid" time="0.20" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.20" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00000003" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.38"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -305,25 +305,25 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x0000000F" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.38"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x0000001F" expanded="true">
<proof prover="0"><result status="valid" time="0.20" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.20" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.42"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x0000003F" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.42"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x0000007F" expanded="true">
<proof prover="0"><result status="valid" time="0.21" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.21" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.41"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -334,79 +334,79 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x000001FF" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x000003FF" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.43"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x000007FF" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.45"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00000FFF" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.11" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00001FFF" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.51"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x00003FFF" expanded="true">
<proof prover="0"><result status="valid" time="0.21" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.21" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.45"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x00007FFF" expanded="true">
<proof prover="0"><result status="valid" time="0.18" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x0000FFFF" expanded="true">
<proof prover="0"><result status="valid" time="0.19" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.43"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x0001FFFF" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.46"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x0003FFFF" expanded="true">
<proof prover="0"><result status="valid" time="0.13" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x0007FFFF" expanded="true">
<proof prover="0"><result status="valid" time="0.18" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x000FFFFF" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00FFFFFF" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="172"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="171"/></proof>
<proof prover="1"><result status="valid" time="0.55"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......
examples/bitwalker.mlw
View file @ 6e6251a4
......@@ -16,22 +16,6 @@ module Bitwalker
use import mach.bv.BV
*)
predicate in_small_range (x:BV32.t) = BV32.ule x (BV32.of_int BV8.max_int)
predicate in_small_range2 (x:BV64.t) = BV64.ule x (BV64.of_int BV32.max_int)
lemma toBig_to_uint: forall x:BV8.t.
BV32.to_uint (C8_32.toBig x) = BV8.to_uint x
lemma toSmall_to_uint: forall x:BV32.t. in_small_range x ->
BV32.to_uint x = BV8.to_uint (C8_32.toSmall x)
lemma toBig_to_uint2: forall x:BV32.t.
BV64.to_uint (C32_64.toBig x) = BV32.to_uint x
lemma toSmall_to_uint2: forall x:BV64.t. in_small_range2 x ->
BV64.to_uint x = BV32.to_uint (C32_64.toSmall x)
function nth8_stream (stream : array BV8.t) (pos : int) : bool =
BV8.nth stream[div pos 8] (7 - mod pos 8)
......
examples/bitwalker/why3session.xml
View file @ 6e6251a4
This diff is collapsed.
examples/hackers-delight.mlw
View file @ 6e6251a4
......@@ -12,7 +12,7 @@ theory Utils
constant one : t = of_int 1
constant two : t = of_int 2
constant lastbit : t = sub size one
constant lastbit : t = sub size_bv one
function max (x y : t) : t = (if ult x y then y else x)
function min (x y : t) : t = (if ult x y then x else y)
......@@ -238,7 +238,7 @@ module Hackers_delight
integer *)
lemma nthBinary: forall b i.
ult i size ->
ult i size_bv ->
nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zero
(** The last property that we check is that if an integer is even
......@@ -342,7 +342,7 @@ module Hackers_delight
(** {6 Shifts and rotates} *)
(** shift right and arithmetic shift right (p.20)*)
lemma SR1: forall x n. ult n size ->
lemma SR1: forall x n. ult n size_bv ->
bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (of_int 31) )) (sub (of_int 31) n))
= asr_bv x n
......
examples/hackers-delight/why3session.xml
View file @ 6e6251a4
......@@ -6,16 +6,17 @@
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.3" timelimit="70" memlimit="1000"/>
<file name="../hackers-delight.mlw" expanded="true">