Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
0e68a951
Commit
0e68a951
authored
May 23, 2017
by
Mário Pereira
Browse files
deleted ocaml32 driver
parent
70504c50
Changes
1
Hide whitespace changes
Inline
Side-by-side
drivers/ocaml32.drv
deleted
100644 → 0
View file @
70504c50
(* OCaml driver for 32-bit architecture
Note: module mach.int.Array32 is currently unsupported on a 32-bit OCaml *)
import "ocaml-gen.drv"
(*theory bv.BV32
syntax type t "Int32.t"
syntax constant zero "0l"
syntax constant ones "-1l"
syntax function bw_and "(Int32.logand %1 %2)"
syntax predicate eq "(%1 = %2)"
(* TODO ... *)
end*)
module mach.int.Int32
syntax val of_int "Why3extract.Why3__BigInt.to_int32"
syntax converter of_int "%1l"
syntax function to_int "(Why3extract.Why3__BigInt.of_int32 %1)"
syntax type int32 "Int32.t"
syntax val (+) "Int32.add"
syntax val (-) "Int32.sub"
syntax val (-_) "Int32.neg"
syntax val ( * ) "Int32.mul"
syntax val (/) "Int32.div"
syntax val (%) "Int32.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
syntax val to_bv "(fun x -> x)"
syntax val of_bv "(fun x -> x)"
end
module mach.int.UInt32
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax constant zero_unsigned "0L"
syntax type uint32 "Int64.t"
syntax val (+) "Int64.add"
syntax val (-) "Int64.sub"
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val (%) "Int64.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
(* direct realization of add_with_carry, add3, mul_with_carry.
Remember that parameters are assumed to denote unsigned integers
less than 2^{32} *)
syntax val add_with_carry "(fun x y c ->
let r = Int64.add x (Int64.add y c) in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
syntax val add3 "(fun x y z ->
let r = Int64.add x (Int64.add y z) in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
syntax val mul_double "(fun x y ->
let r = Int64.mul x y in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
end
module mach.int.Int63
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax type int63 "Int64.t"
syntax val (+) "Int64.add"
syntax val (-) "Int64.sub"
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val (%) "Int64.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.Int64
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax type int64 "Int64.t"
syntax val (+) "Int64.add"
syntax val (-) "Int64.sub"
syntax val (-_) "Int64.neg"
syntax val ( * ) "Int64.mul"
syntax val (/) "Int64.div"
syntax val (%) "Int64.mod"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment