MARCHE Claude
52cc1f8f72
Merge branch 'rac-failure-log-environment' into 'master'
...
Log entire environment at RAC failure
See merge request why3/why3!1200
2025-03-27 08:36:53 +01:00
MARCHE Claude
997bdc53c1
add simple examples of iterators on sets with extraction to OCaml
...
The stdlib is augmented with iterator mechanisms
The OCaml extraction driver is augmented accordingly, using OCaml Seq
2025-03-26 17:20:01 +01:00
Claude Marche
534bd32d04
Do not introduce program variables for zero and one in int.Int module
2025-03-26 15:17:05 +01:00
Gerald Point
f94ce99222
add java extraction driver java.drv
2024-10-02 11:28:58 +02:00
Guillaume Melquiond
31856ab18a
Merge branch 'float-extraction' into 'master'
...
Add preliminary support for extraction of floating-point literals (fix #822 ).
Closes #822
See merge request why3/why3!1099
2024-10-02 10:58:02 +02:00
MARCHE Claude
7dd2b50449
Pmodule: t->t->t functions can be overloaded as X->X->t functions
...
allows to add program equality on Booleans
2024-09-19 10:54:24 +02:00
MARCHE Claude
59cb8a7de0
List length via peano
2024-09-03 11:09:30 +02:00
Claude Marche
4791086e9e
compute a list length as a 63-bit integer
2024-09-02 11:27:27 +02:00
Guillaume Melquiond
92d19d80f5
Correctly mark prefix C operators as right-associative.
...
This patch also adds some explicit spaces, to avoir interpreting "- -" as
the preincrement operator.
It also removes useless precedence from plain functions.
2024-07-08 10:28:12 +02:00
Guillaume Melquiond
2bcc571f31
Add preliminary support for extraction of floating-point literals.
2024-07-04 18:52:58 +02:00
MARCHE Claude
08b9dd878c
add int16 and uint16 and extraction to c
2024-05-15 21:19:34 +02:00
Guillaume Melquiond
b26ef64f77
Remove outdated extraction driver ( fix #843 ).
...
Support for it was removed between Why3 0.88 and 1.0.
2024-04-08 15:12:50 +02:00
Jean-Christophe Filliatre
4e5c3d648a
remove unsound module null.Null
...
this was unsound for the following reason:
- in WhyML, it is possible to make the difference between Null and (Value Null)
- in OCaml, the two would be the same
fix (and improve) example bag, which was the only use of null.Null so far
2024-01-27 10:58:19 +01:00
Jean-Christophe Filliatre
fabbd2e112
fixed ocaml driver for Stack/Queue.length
2024-01-24 14:54:14 +01:00
BONNOT Paul
58313caa48
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
Guillaume Melquiond
2e724c6e7d
Use Stdlib instead of Pervasives during extraction.
2023-01-13 13:33:46 +01:00
Guillaume Melquiond
dd28d01fbe
Move extraction drivers to their own directory.
2022-05-23 18:24:17 +02:00
