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
Files
master
why3/examples/multiprecision
History
Matteo Manighetti 445595866e Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
..
add
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
add_1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
base_info
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
compare
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
div
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
get_str
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
lemmas
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
lineardecision
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
logical
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mini-gmp
Clean up archive
2018-06-22 14:26:57 +02:00
mpz
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_abs
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_add
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_cmp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_cmpabs
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_div
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_div2exp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_get_str
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_getset
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_mul
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_mul2exp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_neg
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_realloc2
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_set_str
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mpz_sub
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mul
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
overlays
Update overlay for pure 64-bit mode.
2020-06-26 18:16:28 +02:00
plots
Add gnuplot scripts for benchmarking
2020-02-06 17:44:38 +01:00
powm
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
random
Clean up archive
2018-06-22 14:26:57 +02:00
set_str
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
sqrt
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
sqrtrem
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
stringlemmas
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
sub
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
sub_1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
toom
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
types
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
util
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
valuation
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
wmpn
Add a initial comment in shapes files
2021-08-25 10:49:04 +00:00
.gitattributes
multiprecision gitattributes
2018-06-22 14:55:19 +02:00
.gitignore
Extract multi-file multiprecision library using headers
2018-06-22 14:26:57 +02:00
add_1.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
add.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
base_info.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
binverttab.ml
powm: extraction
2019-07-31 17:02:27 +02:00
compare.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
div.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
get_str.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
lemmas.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
lineardecision.mlw
Remove some trailing whitespaces.
2023-11-23 18:46:29 +01:00
logical.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
Makefile
add a forgotten GMPFLAGS for targets that use GMP
2024-10-02 10:07:13 +02:00
mpz_abs.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_add.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_cmp.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
mpz_cmpabs.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
mpz_div2exp.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_div.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_get_str.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_getset.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_mul2exp.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_mul.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_neg.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_realloc2.mlw
whymp: add some mpz functions
2021-04-27 13:23:43 +02:00
mpz_set_str.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz_sub.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mpz.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
mul.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
powm.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
ptralias.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
set_str.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
sqrt.mlw
Fix sessions
2019-11-04 10:00:56 +01:00
sqrtinit.ml
Generate sqrtinit.h.
2019-05-21 09:01:21 +02:00
sqrtrem.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
stringlemmas.mlw
Prove some strlen lemmas
2020-03-18 14:27:11 +01:00
sub_1.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
sub.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
tests.c
Improve benchmarks.
2021-04-27 12:21:33 +02:00
toom.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
types.mlw
Mark assignment functions as inlinable in examples/multiprecision.
2023-06-20 14:41:46 +02:00
util.mlw
stdlib: proper postcondition for (=) on bounded integers
2023-06-17 00:16:27 +00:00
valuation.mlw
Use the global ident table when extracting a function call
2019-11-25 16:59:43 +01:00
wmp.h
whymp: add some mpz functions
2021-04-27 13:23:43 +02:00
wmpn.drv
Mark assignment functions as inlinable in examples/multiprecision.
2023-06-20 14:41:46 +02:00
wmpn.mlw
whymp: add some mpz functions
2021-04-27 13:23:43 +02:00