415 Commits

Author SHA1 Message Date
Joffrey Huguet
44c9f597a6 Merge branch 'topic/1187-minor-test-update' into 'master'
Minor update of test output

Issue: eng/spark/spark2014#1187

See merge request eng/spark/sparklib!235
2026-02-11 15:06:36 +00:00
Claire Dross
6b203cac3d Minor update of test output 2026-02-11 09:28:32 +01:00
Claire Dross
7e9d23fdd4 Merge branch 'topic/1187-dross-proof-cyclic' into 'master'
Update warnings about recursive subprograms

Issue: eng/spark/spark2014#1187

See merge request eng/spark/sparklib!234
2026-02-10 09:28:51 +00:00
Claire Dross
fccd05adf7 Update warnings about recursive subprograms 2026-02-09 10:34:26 +01:00
Claire Dross
ca214c2cc4 Merge branch 'topic/1188-dross-replace-element' into 'master'
Fix precondition of Replace_Element on formal sets

Issue: eng/spark/spark2014#1188

See merge request eng/spark/sparklib!233
2026-02-04 07:45:58 +00:00
Claire Dross
5b1cdd6403 Fix precondition of Replace_Element on formal sets 2026-02-02 17:20:23 +01:00
Piotr Trojanek
9c35056cf7 Merge branch 'topic/blake3' into 'master'
Switch from SHA1 to Blake3 to squeeze long Why3 filenames

Issue: eng/spark/spark2014#1175

See merge request eng/spark/sparklib!231
2026-01-28 09:59:55 +01:00
Piotr Trojanek
e91968c3c7 Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 3) 2026-01-27 10:11:10 +01:00
Piotr Trojanek
8fc84e846f Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 2) 2026-01-27 01:32:37 +01:00
Piotr Trojanek
6645568407 Switch from SHA1 to Blake3 to squeeze long Why3 filenames (part 1) 2026-01-27 01:32:34 +01:00
Johannes Kanig
a3e69f200a Merge branch 'topic/kanig-sparklib' into 'master'
Fixes to sparklib proofs

Issue: eng/spark/spark2014#1152

See merge request eng/spark/sparklib!230
2026-01-20 09:40:26 +00:00
Johannes Kanig
f5e451566d Fixes to sparklib proofs
- fixes to session generation script
- fixed line/col numbers for VCs
2026-01-20 10:53:48 +09:00
Johannes Kanig
6a2ac48b4d New sessions after prover updates 2026-01-20 10:30:08 +09:00
Johannes Kanig
b9b3c7272d Merge branch 'topic/kanig-1152-baselines' into 'master'
Baselines for prover updates

Issue: eng/spark/spark2014#1152, eng/spark/spark2014#1153, eng/spark/spark2014#1154

See merge request eng/spark/sparklib!229
2026-01-16 09:23:38 +00:00
Johannes Kanig
5205d4b4fa Baselines for prover updates 2026-01-13 09:56:25 +00:00
Johannes Kanig
28eeabc4ca Merge branch 'topic/kanig-773-preproc' into 'master'
Fix generate_session.py

Issue: eng/spark/spark2014#773

See merge request eng/spark/sparklib!227
2026-01-09 08:05:21 +00:00
Johannes Kanig
373215ff07 Fix generate_session.py 2026-01-07 08:19:57 +00:00
Johannes Kanig
83611539c5 Merge branch 'topic/kanig-copyright' into 'master'
Update copyright info

no-issue-check

See merge request eng/spark/sparklib!226
2026-01-07 08:16:41 +00:00
Johannes Kanig
e14fdaf74e Update copyright info 2026-01-05 10:01:42 +00:00
Johannes Kanig
0f9ea09e3c Merge branch 'topic/kanig-merge' into 'master'
Update sessions for why3 update

Issue: eng/spark/spark2014#1146

See merge request eng/spark/sparklib!219
2026-01-05 09:50:29 +00:00
Johannes Kanig
613b2bf465 Update sparklib sessions after why3 update 2026-01-05 00:16:55 +00:00
Johannes Kanig
4daa25c47e Merge branch 'topic/kanig-1148-extract' into 'master'
Remove explicit gnatformat date from sparklib

Issue: eng/spark/spark2014#1148

See merge request eng/spark/sparklib!224
2026-01-04 23:26:40 +00:00
Johannes Kanig
45fefdf609 Remove explicit gnatformat date from sparklib 2025-12-19 10:25:33 +00:00
Claire Dross
d787e29610 Merge branch 'topic/1139-test-update' into 'master'
Remaining large test updates

Issue: eng/spark/spark2014#1139

See merge request eng/spark/sparklib!223
2025-12-19 10:24:16 +00:00
Claire Dross
50bfe58c69 Remaining large test updates 2025-12-19 09:36:02 +01:00