355 Commits

Author	SHA1	Message	Date
MARCHE Claude	89a894b47a	do not map IEEE floats theory to Alt-Ergo's own theory ... Upgrade to AE 2.6.2	2025-06-18 10:45:29 +09:00
Matteo Manighetti	c04b008016	Merge remote-tracking branch 'why3-inria/master' into why3-devel	2024-12-13 17:34:11 +01:00
Guillaume Melquiond	137c1472a4	Remove some trailing spaces.	2024-12-07 09:01:55 +01:00
Claude Marche	cabea44347	fix realizations	2024-11-13 19:10:42 +01:00
Guillaume Melquiond	46d53c02a9	Mark some types as having an extensional equality.	2024-11-13 19:04:52 +01:00
Claude Marche	c000797178	Additional operators for fmaps	2024-11-08 10:15:33 +01:00
MARCHE Claude	5ced5ae2b7	Adding a function from_real in the theory of IEEE floats	2024-11-03 21:13:10 +01:00
MARCHE Claude	6ce01d8b7e	Resolve "provide axioms for sdiv and smod in theory bitvector theory"	2024-11-02 08:36:31 +01:00
Jean-Christophe Filliâtre	da82f89b3f	Merge branch 'whyml2java' into 'master' ... Whyml2java See merge request why3/why3!1064	2024-10-31 21:14:12 +01:00
Matteo Manighetti	dca6530002	Merge remote-tracking branch 'why3-inria/master' into why3-devel	2024-10-30 14:11:24 +01:00
MARCHE Claude	4d04b4f698	add metas for unused-dependencies on sequences ... also fix split_full that was losing metas for unused dependency	2024-10-29 16:12:46 +01:00
Matteo Manighetti	1c65544ddb	Merge commit '1dc1b78e8c8e39e7b57e7299be0879ed027d19bd' into why3-before-cex-from-rac	2024-10-23 16:51:58 +02:00
MARCHE Claude	7e819237a6	unused dependencies on Euclidean div/mod	2024-10-23 15:10:58 +02:00
MARCHE Claude	24baef2ce5	fix closure computation in remove_unused	2024-10-22 21:25:49 +02:00
Gerald Point	370b73b83d	add mach.java modules	2024-10-02 11:28:58 +02:00
MARCHE Claude	6813754dce	clarify ghost and non-ghost for reals and ufloats	2024-10-01 15:38:42 +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
Jacques-Henri Jourdan	9137a0403e	Define converters from various BV sizes to 256 bits ... Update drivers accordingly	2024-09-17 13:14:05 +02:00
PATAULT Paul	9371ad18ab	Merge branch 'coma-only' into 'master' ... New front-end language: Coma See merge request why3/why3!1098	2024-09-04 10:19:12 +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
Paul Patault	000fd2d347	coma: update stdlib + examples	2024-08-08 11:09:46 +02:00
Paul Patault	ddb799e96d	coma: add attributes to pre/post if given in type decl	2024-08-08 09:06:08 +02:00
Andrei Paskevich	4ab78a9f61	coma: eliminate trivial equalities more aggressively	2024-08-08 09:06:08 +02:00
Paul Patault	ec40aa57b7	coma: WIP RE	2024-08-08 09:06:08 +02:00