Johannes Kanig
a2807b3ddb
Merge 1.8.2 into AdaCore master
2025-10-14 10:32:03 +09:00
Claude Marche
e991d73789
update headers
2025-06-04 10:51:30 +02:00
Matteo Manighetti
c04b008016
Merge remote-tracking branch 'why3-inria/master' into why3-devel
2024-12-13 17:34:11 +01:00
Guillaume Melquiond
8a86d9ac62
Update copyright years.
2024-12-07 09:01:55 +01: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
Matteo Manighetti
436c5e6414
Add all warning IDs and make them mandatory
2023-09-11 17:12:34 +00:00
Jacques-Henri Jourdan
8e64474551
Fix a bug in cfg_path, where unnamed invariants triggered an infinite loop.
...
Each time we saw an unnamed invariant, we would assign it a new
generated name, so that going twice through the same invariant would
not trigger the "already seen" mechanism.
2023-05-23 17:01:54 +02:00
Johannes Kanig
8772b328ac
Fixes of merge commit
...
* cfg_stackify.ml: added implementation of Either.t and
List.partition_map, as those don't exist in older versions of ocaml
* remove our code related to epsilon, replaced by upstream code
* incomplete change during merge: closed paren vs end
* some functions need to be exported
2023-05-18 08:58:22 +09:00
Xavier Denis
773169689a
Make named invariants in mlcfg optional and deprecated
2023-04-27 11:20:10 +02:00
Xavier Denis
cb9c7730f2
Add support for loop variants to mlcfg
2023-04-27 01:18:08 +02:00
Guillaume Melquiond
79738ae6a4
Update headers.
2023-03-07 09:58:45 +01:00
Xavier Denis
673edaccef
Format
2023-02-06 16:02:21 +01:00
Xavier Denis
7bee7d25a1
Set up skeleton for subregion mutation analysis
2023-02-06 16:02:20 +01:00
MARCHE Claude
7cc7156c0e
Revamp the API for loading drivers. Documentation clarified too.
2022-07-21 15:08:01 +00:00
Jacques-Henri Jourdan
5633c0e12c
MLCFG: allow attributes to the body of a function.
2022-07-06 13:18:28 +02:00
Guillaume Melquiond
53926bbbf5
Update headers.
2022-04-26 16:33:42 +02:00
Claude Marche
27b9fd8a97
CFG/stackify: keep the name of invariants in generated WhyML
2022-04-19 13:00:38 +02:00
Claude Marche
10c3ba9a84
fix generation of infinite loops, adding an absurd afterwards
...
Additional various fixes, including removing annoying warnings from
recent versions of OCaml
2022-03-29 19:03:27 +02:00
Xavier Denis
1985144eab
Stackify
2022-01-14 10:35:59 +01:00
