ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
16,366 Commits 65 Branches 1 Tag
23.2
Commit Graph

278 Commits

Author SHA1 Message Date
Solène Moreau
74914e7651 (V719-014) Merging Inria/master into SPARK/master 
Change-Id: I2144736b2dbb76966fbe4eae6238a8751799a3d2
Depends-On: I5a522521b64c6e676113695f30625b9618461867
Depends-On: I51bf388c10a7d73401ebb48c7c3c07828da4af12
 2022-07-19 14:57:03 +02:00
MARCHE Claude
99b3693442 Resolve "Constant max_int of ieee_float.GenericFloat should be given a value in its clones" 2022-07-08 17:18:36 +00:00
Claude Marche
c8614700f3 Reimplement the transf in two phases and tail recursive functions 2022-07-07 12:24:42 +02:00
Claude Marche
549f987180 fix elimination of constants. 
Update oracles

Add elimination also in Alt-Ergo >= 2.4.0 and Z3 >= 4.4.0
 2022-06-02 12:37:23 +02:00
Claude Marche
5f830d7c5e more dependency metas 2022-06-02 09:44:06 +02:00
Claude Marche
abe993e76a Use the new meta for eliminating int.abs when not needed 2022-06-02 08:36:36 +02:00
Solène Moreau
a29b8b930c V325-031 Merging Why3/Inria master into Why3/SPARK master 
Change-Id: Ib12de95cfa922bd1b8c1f5ad1ba269de9c90894c
Depends-On: I3c3e37849899e4436210701c67ddf0049aa08204
Depends-On: I28a9ef2ea1b11448bea50d1f4c4c799e8255fda8
 2022-04-26 09:17:30 +02:00
MARCHE Claude
bcfef9818c Resolve "Fix drivers for SMT-LIB strings" 2022-04-06 14:29:41 +00:00
Solène Moreau
524b938a9d V325-031 Merge with upstream Why3 
Change-Id: I2e98bd5ec8c138751713811f4dad164be6a4463a
 2022-03-29 10:47:33 +02:00
Yannick Moy
5040c670ae UB05-006 Add theories and drivers for extended floats 
This adds the support for 80-bits so-called extended floating-point types
to the IEEE theory of floats in Why3.

[changelog]
* drivers/smt-libv2-floats.gen:
(ieee_float.Float80): Use native support and remove propositions.
(ieee_float.FloatConverter): Remove propositions on this generic theory.
(ieee_float.Float32_64_Converter): Adapt from previous binding.
(ieee_float.Float80_BV_Converter): Similar to other BV converters.
* plugins/gnat_json/gnat_ast_to_ptree.ml: Adapt to new Float80 theory.
* stdlib/ieee_float.mlw:
(Float80): New module.
(FloatConverter): Make module abstract in small/large fp types.
(Float32_64_Converter): New name for previous FloatConverter.
(Float32_80_Converter): New conversion module.
(Float64_80_Converter): New conversion module.
(Float_BV_Converter): Delay axiom of_ubv64_to_real at instantiation.
(Float32_BV_Converter): Provide axiom for of_ubv64_to_real.
(Float64_BV_Converter): Provide axiom for of_ubv64_to_real.
(Float80_BV_Converter): New conversion module.

Change-Id: I8feba3c3440878c4a6a20c511b86b8cd69eef328
 2021-11-08 15:28:43 +01:00
Jean-Christophe Filliatre
08712c15ac micro-Python: added support for built-in function pow 2021-10-29 15:57:14 +02:00
Claude Marche
32e3b0514a fix from Guillaume's remarks 2021-09-29 15:28:00 +02:00
Claude Marche
1b9355cf1a Merge branch 'master' into 551-module-mach-bv-should-provide-purely-bitvector-based-pre-conditions 
# Conflicts:
#	bench/ce/oracles/threshold_Z3,4.8.4_SP.oracle
#	bench/ce/oracles/threshold_Z3,4.8.4_WP.oracle
 2021-09-29 09:19:01 +02:00
Claude Marche
621aff44a7 Several renamings and fix a few pre and post-conditions 2021-09-29 08:57:02 +02:00
Guillaume Melquiond
38e4098f57 Document module "io" (fix #554). 2021-09-23 15:11:55 +02:00
Guillaume Melquiond
7b4b4fb26e Fix some typos. 2021-09-22 16:57:26 +02:00
Guillaume Melquiond
ea123b5e95 Improve documentation of standard library. 2021-09-21 18:00:14 +02:00
Benedikt Becker
d919886b0c T127-015 Merge with upstream Why3 
Change-Id: Ic6472dd67180667554db718c8f328f9832b1e8fb
 2021-09-07 13:50:44 +02:00
Guillaume Cluzel
7fd1e0cad6 Correct the precondition of some functions 2021-08-31 06:56:15 +02:00
Guillaume Cluzel
5c9c185312 Ues BV 128 to check the precondition of mach.bv operations 2021-08-23 11:23:04 +02:00
Claude Marche
761f826c83 convert to 128 bit for checks 2021-07-13 16:40:34 +02:00
Jean-Christophe Filliâtre
6b427d7458 Merge branch 'internship-2021-LMF' into 'master' 
TryWhy3: All in one

See merge request why3/why3!553
 2021-07-08 13:42:09 +00:00
Quentin Garchery
8087958624 cardinal of finite products 2021-06-27 13:21:36 +02:00
Quentin Garchery
55f778f310 add Set.product 2021-06-27 12:01:18 +02:00
Quentin Garchery
b26dc512ec add Set.filter 2021-06-27 11:50:21 +02:00