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
18,511 Commits 65 Branches 1 Tag
master
Commit Graph

492 Commits

Author SHA1 Message Date
Johannes Kanig
3262153853 Various postmerge adaptations 2025-12-15 17:51:17 +09:00
Johannes Kanig
25b13e2cab merge commit 2025-12-15 10:45:08 +09:00
Benjamin Jorge
350cc165aa Support module with interface in parsing API 2025-11-20 14:24:32 +01:00
Benjamin Jorge
a07a1b6a88 Improve Pmodule API, update documentation 2025-11-20 14:14:24 +01:00
Benjamin Jorge
667ab3ae79 Sandwich implementation 2025-11-20 14:14:24 +01:00
Johannes Kanig
e6c44bb771 Follow AST change in gnat2why 2025-11-12 10:48:43 +00:00
XIA Li-Yao
51e0579b35 Merge branch 'multi-spans' into 'master' 
coma: Highlight function call sites

Closes #928

See merge request why3/why3!1261
 2025-10-29 17:31:55 +01:00
XIA Li-Yao
061ff8cc12 Merge branch 'coma-errors-2' into 'master' 
coma: locate some error messages

Closes #907

See merge request why3/why3!1260
 2025-10-29 11:30:30 +01:00
Li-yao Xia
ea57d79058 coma: Allow annotating function calls with source locations 2025-10-17 20:23:04 +02:00
Li-yao Xia
f0d09ca4fd coma: Track callers in VC generation 2025-10-17 20:23:04 +02:00
Li-yao Xia
5ef8115d8d Update term to carry multiple locations 2025-10-17 20:23:02 +02:00
Li-yao Xia
b9a59a9ebb coma: Add field for function call locations 2025-10-17 17:27:55 +02:00
Li-yao Xia
64b6266f58 coma: locate some error messages 2025-10-17 12:43:30 +02:00
Li-yao Xia
340fc7b46e coma: better better type error messages 2025-10-17 11:13:17 +02:00
Paul Patault
7064223432 coma: typing better error messages 2025-10-17 10:37:47 +02:00
Johannes Kanig
a2807b3ddb Merge 1.8.2 into AdaCore master 2025-10-14 10:32:03 +09:00
Andrei Paskevich
a5898d4657 coma_logic: ignore fake dependencies in mutually recursive handlers 2025-07-24 20:00:25 +02:00
Claude Marche
50f084bf55 Merge branch 'bugfix/v1.8' 2025-06-04 11:10:16 +02:00
Claude Marche
e991d73789 update headers 2025-06-04 10:51:30 +02:00
Martin Clochard
d29be55424 Clean up compiler warnings 
Change-Id: Ibf6a012ed61635ea324cbabee05cadb72e143baf
 2025-04-07 11:25:36 +02:00
Matteo Manighetti
399658bd65 Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel 2025-03-25 17:55:52 +01:00
Matteo Manighetti
f39e24ed74 Merge branch 'master' into why3-devel 2025-03-25 17:47:35 +01:00
Claude Marche
a912f9d0f7 fix conversion of term to concrete terms for records 2025-02-28 13:38:49 +01:00
Johannes Kanig
7a46b14d36 Adapt Why3 tree to gnat2why changes 2025-01-15 17:36:46 +09:00
Matteo Manighetti
c04b008016 Merge remote-tracking branch 'why3-inria/master' into why3-devel 2024-12-13 17:34:11 +01:00