9 Commits

Author SHA1 Message Date
BONNOT Paul
58313caa48 Resolve "Give values to BV constants when cloning" 2023-06-16 08:44:32 +00:00
Andrei Paskevich
eae547d95f stdlib, examples: remove redundant "import" 2018-06-15 16:45:58 +02:00
Andrei Paskevich
7b0929a761 WhyML: "use/clone T" imports by default (in absence of "as")
For the previous behaviour (no import), write "use/clone T as T".

This shortens the most used "use/clone import" to simply "use/clone".
2018-06-15 16:45:58 +02:00
Jean-Christophe Filliatre
6af5c23793 simpler variants in bitvector examples 2018-05-31 19:28:36 +02:00
Claude Marche
b7787a0143 fix examples using bitvectors 2017-04-28 14:09:39 +02:00
Clément Fumex
f05478680f Add the ability to
* declare range types and float types,
* use integer (resp. real) literals for those types through casting,
* specify how to print them in drivers.

Change in syntax
* use

  type t = < range 1 2 >   (* integers from 1 to 2 *)
  type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)

  the two projections :
  t'int
  t''real

  and the predicate :
  t''isFinite

* Restrict the use of "'" in whyml:
  Users are not allowed to introduce names where a quote symbol
  is followed by a letter. Thus, the following identifiers are
  valid:

  t'
  toto'0''
  toto'_phi

  whereas toto'phi is not.

Note: we do not yet support negative numbers in range declaration
and casting of a literal.
2017-02-28 16:31:36 +01:00
Clément Fumex
3a2d2ca99c change zero to zeros in bv theory 2016-01-28 17:30:17 +01:00
Claude Marche
528975716b Bit-vector: changes spec of rotations + updated sessions 2015-11-19 15:10:24 +01:00
Clément Fumex
0cf707a85a removing theory/bv and refactorisation of module/bitvec in module/bv 2015-04-16 17:54:43 +02:00