Matteo Manighetti
cde6ba24c9
Merge remote-tracking branch 'why3-inria/master' into why3-devel
2024-02-20 11:14:13 +01:00
Matteo Manighetti
f60074fd3f
Facilitate proof of arithmetic on bitvectors by Alt-Ergo
2024-02-20 11:10:10 +01:00
Yannick Moy
04c21853f9
Fcilitate proof of arithmetic on bitvectors by Alt-Ergo
...
Add three new lemmas on addition, subtraction and negation on
bitvectors, that are used by Alt-Ergo. Remove them in the driver
targetting SMTLIBv2.
Also remove upper bound in guard of lemma to_uint_sub_bounded which
is not needed.
Change-Id: I2ed9651d1d7d9dbe56a79af42e715f99166ac9c3
2024-02-01 09:01:29 +00: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
BONNOT Paul
85c4b4917a
Forward propagation of rounding errors
...
New theory for unbounded floats, with propagation lemmas
Examples of use
2024-01-18 10:31:14 +00:00
Matteo Manighetti
d5b86b98fc
Merge remote-tracking branch 'why3-inria/master' into merge_inria_why3_1_7_0
2024-01-11 18:00:47 +01:00
Guillaume Melquiond
09a71c74c0
Fix occurrences of "occurences".
2023-11-23 19:04:11 +01:00
Matteo Manighetti
34c38667a5
Revert "Simplify euclidean to computer division"
...
This reverts commit 7fc778f1d5
2023-10-19 12:12:59 +02:00
MARCHE Claude
149ef043b4
library ieee_float: added conversions between floats and signed bitvectors
...
with appropriate mappings to SMTLIB
2023-09-20 17:56:18 +00:00
Claude Marche
d08d6c287d
reinforce pre-conditions of safe machine floats operations
2023-09-18 17:42:25 +02:00
Andrei Paskevich
fe3bf96cd1
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
BONNOT Paul
58313caa48
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
BONNOT Paul
29c71dbd51
add a meta to mark a symbol as never removed by remove_unused*
...
mark some lemmas on division of real as removable if not needed
2023-06-15 15:18:48 +00:00
MARCHE Claude
06f1e7e62d
fix mistake in MR 882
2023-05-23 13:58:54 +00:00
MARCHE Claude
434c724281
Fix issue 759 by providing early error messages
2023-05-22 13:10:06 +00:00
Matteo Manighetti
dabd0d669c
Merge attemp
2023-05-17 11:15:20 +02:00
BONNOT Paul
8c839099bb
max_int and max_real values not defined as an axiom
...
Transform eliminate_big_constant for dReal prover
2023-04-04 13:00:22 +00:00
MARCHE Claude
113366e478
add metas for remove_unused:dep for bv relations ult ugt slt ugt
2023-04-03 15:23:00 +00:00
Johannes Kanig
41eac08831
Merging upstream Why3 into AdaCore master
2023-03-28 10:24:25 +09:00
Guillaume Melquiond
e278f4f8d5
Fix documentation typo.
2023-03-17 11:06:39 +01:00
MARCHE Claude
49bc8beb00
Changed the unsecure trusted_wf attribute mechanism into a more secure one
2023-02-22 13:50:29 +00:00
Johannes Kanig
c2d19bee32
W120-033 add rewriting of to_int/of_int pairs
...
We add of_int markers to the stdlib (the of_int markers are in gnat2why
library) and add rewriting code acting upon those markers.
* bv.mlw
add rewrite markers to the of_int function
* gnat_rewrite.ml
add rules for of_int/to_int and to_int/of_int
2023-01-30 08:40:03 +09:00
Solène Moreau
be1023970d
(W112-001) Merge Why3/master into SPARK
...
Change-Id: Iefffe9ad9367fbc1c590efdca96cf6311a02481d
Depends-On: If1f1bbd27aeeee421c8c6adb86fef670a924907a
Depends-On: I6be95441469218c8f9dfef8934764b92453c1727
2023-01-13 14:55:39 +01:00
MARCHE Claude
3718457464
Merge branch 'dreal' into 'master'
...
Support for dreal prover
See merge request why3/why3!749
2022-11-17 15:24:52 +00:00
Jean-Christophe Filliatre
bf06311f78
micro-Python: add_list can be used in logic
2022-11-14 14:58:24 +01:00
