Commit Graph

Select branches

Hide Pull Requests

24-sustained

24.0

24.1

24.2

25-sustained

25.0

25.1

25.2

26.0

26.1

26.2

fsf

fsf-14

fsf-15

master

#1

Mono Color

• aacf7f0bef Rename primitives to insert vectors in formal vectors Claire Dross 2024-10-21 11:36:23 +02:00
• da28d165c5 Also use hash_tables from SPARKlib in unbounded containers Claire Dross 2024-10-11 15:31:32 +02:00
• 1cc6b99b7c Move formal hash_tables from gnat repo to sparklib Claire Dross 2024-10-10 16:30:00 +02:00
• 028b927637 Change the definition of Invariant on Multisets Claire Dross 2024-10-08 12:12:29 +02:00
• 19562f3ec7 Various baseline and session updates Johannes Kanig 2024-10-08 10:22:29 +09:00
• c07d12189d File test for hashed maps Claire Dross 2024-09-13 12:56:09 +02:00
• 2f49200a15 Enable test for Resize on unbounded containers Claire Dross 2024-09-13 11:59:32 +02:00
• ca3b23039f Use Include in test for Include for hashed sets Claire Dross 2024-09-12 14:46:09 +02:00
• b98171c57a Use no_crash instead of prove_all in quality tests Joffrey Huguet 2024-09-11 15:42:33 +02:00
• c60bab7425 File tests for hashed sets Claire Dross 2024-09-09 11:21:36 +02:00
• 5ad395942c Use logical equal in posts of unbounded hashed sets Claire Dross 2024-09-09 15:51:07 +02:00
• fc1ea879da Update test output Joffrey Huguet 2024-09-06 15:44:21 +02:00
• a102839de1 Remove incorrect postcondition on Replace_Element Claire Dross 2024-09-04 14:13:17 +02:00
• 8ccefc6552 Add tests for formal vectors Claire Dross 2024-09-03 15:35:54 +02:00
• 1d42a71e34 File test for formal doubly linked lists Claire Dross 2024-07-29 11:54:04 +02:00
• db31ff3fb8 Add test for functional maps Claire Dross 2024-07-26 14:02:51 +02:00
• e72826725a In Splice, insert elements in the order of Source Claire Dross 2024-07-31 18:11:04 +02:00
• 79ae321e43 Fix crash in Splice on empty source for doubly linked lists Claire Dross 2024-07-31 12:39:18 +02:00
• a127223b77 Minor fixes in Doubly_Linked_Lists Claire Dross 2024-07-30 17:47:31 +02:00
• cfc90cad20 File tests for functional sets Claire Dross 2024-07-25 14:59:08 +02:00
• 0411d87315 Add ghost aspects to iteration primitives on functional sets and maps Claire Dross 2024-07-26 16:23:36 +02:00
• e76807af57 Do not use quantification in functional set body Claire Dross 2024-07-25 11:03:27 +02:00
• 04ddf0ebfc Extend postcondition of Is_Singleton on functional sets Claire Dross 2024-07-23 10:37:23 +02:00
• 539060ecdd File test for functional vectors Claire Dross 2024-07-22 16:35:22 +02:00
• db22e63e32 Use a short-circuit operator in Is_Singleton Claire Dross 2024-07-22 17:37:25 +02:00
• dd01a37d71 Add unit tests for SPARK.C.Strings and SPARK.C.Constant_Strings Claire Dross 2024-07-17 16:29:07 +02:00
• 495012ef6f Add Depends contract to SPARK.C.Strings.Free Claire Dross 2024-07-17 15:20:03 +02:00
• ed2b0d8ee0 Move tests for the proof of sparklib units to the sparkilb repo Claire Dross 2024-07-16 12:32:44 +02:00
• 5bffdd56d9 Add preconditions to Generic_Keys.Key in formal sets Claire Dross 2024-06-27 15:28:04 +02:00
• b9c226e3fd Remove obsolete comments at the top of formal sets and maps Claire Dross 2024-06-27 16:02:22 +02:00
• deea24861e Change project file names Joffrey Huguet 2024-06-20 18:01:48 +02:00
• fd1ef520cd Remove tagged types in sparklib light Claire Dross 2024-06-20 14:10:59 +02:00
• d6f454a674 Add Ghost aspect on the internal function Vet Claire Dross 2024-06-17 15:27:37 +02:00
• 28447adb16 Merge branch 'mr/marc/disable_ci_fsf' into 'fsf' Marc Poulhiès 2025-10-28 14:38:01 +01:00
• 92058f2d40 Remove CI for the fsf branch Marc Poulhiès 2025-10-28 12:18:33 +01:00
• 29ef87347c Merge branch 'topic/1069-dross-logical-eq-in-sequences' into 'master' Claire Dross 2025-10-28 11:03:29 +00:00
• cf1fbb8df4 Add boolean parameter to handle logical equality in sequences Claire Dross 2025-10-01 13:42:31 +02:00
• 2f5010e721 Merge branch 'topic/kanig-black' into 'master' Johannes Kanig 2025-10-22 09:52:12 +00:00
• fdead6fcf3 Coverage report for sparklib Johannes Kanig 2025-10-22 17:13:04 +09:00
• d0e412657f Merge branch 'topic/kanig-black' into 'master' Johannes Kanig 2025-10-13 07:12:20 +00:00
• e17b3e6920 Bump black to 25.1.0 Johannes Kanig 2025-10-13 12:02:20 +09:00
• 0f564ef7c2 Merge branch 'topic/26.0-test-update' into '26.0' 26.0 Joffrey Huguet 2025-10-08 22:16:16 +00:00
• 78d5ce785d Update session tests Joffrey Huguet 2025-10-08 18:06:22 +02:00
• f2509db2d6 Merge branch 'topic/kanig-sessions' into 'master' Johannes Kanig 2025-09-18 09:12:46 +00:00
• 07d9b81bf7 Minor session updates Johannes Kanig 2025-09-18 17:54:21 +09:00
• 6275b6f48a Merge branch 'topic/752-dross-test-outputs' into 'master' Joffrey Huguet 2025-09-16 20:21:28 +00:00
• ba89e7045e Move tests for the full runtime to large and update outputs Claire Dross 2025-09-16 20:00:15 +02:00
• 2ec8b5e22d Merge branch 'topic/752-dross-add-tests-with-gnata' into 'master' Claire Dross 2025-09-16 08:04:36 +00:00
• 82a8328d17 Ensure that SPARKlib works with assertions enabled Claire Dross 2025-09-12 12:05:51 +02:00
• e99e239412 Merge branch 'topic/752-dross-ghost-level-in-sparklib' into 'master' Claire Dross 2025-09-10 19:14:24 +00:00
• 406899cfb0 Update session test Claire Dross 2025-09-04 14:16:17 +02:00
• d0933b76f7 Introduce assertion levels in the SPARKlib Claire Dross 2025-06-23 14:30:48 +02:00
• 3adc140410 Merge branch 'topic/kanig-sparklib' into 'master' Johannes Kanig 2025-08-21 09:16:48 +00:00
• 47f55feda6 Update baselines for SPARKlib Johannes Kanig 2025-08-21 10:00:37 +09:00
• f7c2f68c9c Merge branch 'topic/none-huguet-update-tests' into 'master' Piotr Trojanek 2025-08-14 00:02:22 +02:00
• f3068912d5 Update session tests and outputs Joffrey Huguet 2025-08-13 18:41:58 +02:00
• 766812551b Merge branch 'topic/936-clochard-repair-session-after-continue-exit-name-change' into 'master' Martin Clochard 2025-07-30 10:01:11 +00:00
• 6a5e83e847 Repair session after support for continue Martin Clochard 2025-07-28 16:14:30 +02:00
• 81af72afb3 Merge branch 'topic/980-dross-update-session' into 'master' Claire Dross 2025-07-09 07:45:01 +00:00
• 8d7451a9c8 Update session files Claire Dross 2025-07-08 16:56:17 +02:00
• 3863ecc48e Merge branch 'topic/976-dross-test-outputs' into 'master' Claire Dross 2025-07-08 11:29:47 +00:00
• b1e3bf2ead Minor update to test outputs Claire Dross 2025-07-07 17:43:16 +02:00
• 429f5fdfc2 Merge branch 'topic/kanig-966-comment' into 'master' Johannes Kanig 2025-07-06 23:53:17 +00:00
• 7c3e55d857 Add comment to pragma Warnings Johannes Kanig 2025-06-26 10:20:24 +09:00
• 90eee876db Merge branch 'topic/ghost_generic_elab' into 'master' Piotr Trojanek 2025-07-02 10:46:31 +02:00
• a9accb9efe Update slocs after removing workaround for an elaboration issue Piotr Trojanek 2025-07-01 17:31:33 +02:00
• 99b8a800b1 Merge branch 'topic/ghost_generic_elab' into 'master' Piotr Trojanek 2025-07-01 16:11:42 +02:00
• 76f29308f8 Deconstruct workaround for ghost elaboration entities in generic instances Piotr Trojanek 2025-06-30 11:27:32 +02:00
• a7c2bc5383 Merge branch 'topic/ghost_generic_elab' into 'master' Piotr Trojanek 2025-06-27 01:31:10 +02:00
• a871a2c1f8 Remove workaround for ghost elaboration entities in generic instances Piotr Trojanek 2025-06-26 15:01:53 +02:00
• 6873c984d1 Merge branch 'topic/kanig-773-reorg' into 'master' Johannes Kanig 2025-06-26 08:37:18 +00:00
• 45ed5a9b9a Fix sparklib tests after reorg Johannes Kanig 2025-06-25 10:30:02 +09:00
• 299277ae16 Merge branch 'topic/kanig-966-underflow' into 'master' Johannes Kanig 2025-06-25 07:41:14 +00:00
• c8a083d780 Suppress spurious warning about underflow Johannes Kanig 2025-06-25 16:19:30 +09:00
• 67fa99831a Merge branch 'topic/kanig-773-reorg' into 'master' Johannes Kanig 2025-06-25 01:26:28 +00:00
• 0f96585ead Move comment to more appropriate place Johannes Kanig 2025-06-20 09:30:33 +09:00
• 42ea23f198 Enable style checking for SPARKlib light Johannes Kanig 2025-06-20 08:47:39 +09:00
• 8c3cdcc322 Restructure sparklib to use subfolders instead of file naming schemes Johannes Kanig 2025-06-16 10:39:48 +09:00
• 6642934c56 Merge branch 'topic/kanig-959-lines' into 'master' Johannes Kanig 2025-06-18 23:34:14 +00:00
• e5543eba5d update line numbers after source change Johannes Kanig 2025-06-18 18:20:16 +09:00
• 8e3d5225b1 Merge branch 'topic/959-dross-big-number-literals' into 'master' Claire Dross 2025-06-16 08:49:40 +00:00
• b7bf4714e7 Session updates Johannes Kanig 2025-06-16 17:44:03 +09:00
• 485a33f57f Restore provability of floating-point arithmetic lemmas Claire Dross 2025-06-16 10:23:42 +02:00
• dc7cd02b08 Merge branch 'topic/fsf-15-cp' into 'fsf-15' fsf-15 Joffrey Huguet 2025-06-11 08:39:51 +00:00
• 71afecf069 Change project file names Joffrey Huguet 2024-06-20 18:01:48 +02:00
• 7d9bebb6f6 Merge branch 'topic/fsf-15-cp' into 'fsf-15' Joffrey Huguet 2025-06-09 09:40:34 +00:00
• c1305f2e82 Simplify sparklib.gpr for Alire Joffrey Huguet 2024-06-17 12:49:28 +02:00
• 05154be87d Merge branch 'topic/minor-test-update' into 'master' Claire Dross 2025-05-16 09:25:13 +00:00
• 997ec34bc5 Minor diffs in warnings in test output Claire Dross 2025-05-16 09:56:09 +02:00
• 17c6c618cc Merge branch 'topic/kanig-1602-baseline' into '25.2' 25.2 Johannes Kanig 2025-05-14 07:14:59 +00:00
• 8a032e736e Update session for 25.2 Johannes Kanig 2025-05-13 10:01:48 +09:00
• 618a911f79 Merge branch 'topic/kanig-864-baselines' into 'master' Joffrey Huguet 2025-04-30 11:57:43 +00:00
• 6e0ea769fc Baseline and session updates Johannes Kanig 2025-04-30 18:54:42 +09:00
• c297933c86 Merge branch 'topic/910-dross-double-free-on-aggregates' into 'master' Claire Dross 2025-04-23 14:30:09 +00:00
• 65cdac2005 Session updates on multiset tests Claire Dross 2025-04-23 16:03:36 +02:00
• 672c2ebcdb Merge branch 'topic/910-dross-double-free-on-aggregates' into 'master' Claire Dross 2025-04-23 13:17:27 +00:00
• 640af19d5b Use explicit component associations in Empty_Multiset Claire Dross 2025-04-23 14:48:33 +02:00
• 81d2c2de26 Merge branch 'topic/910-dross-crash-on-contract-of-UDLL' into 'master' Claire Dross 2025-04-23 13:14:50 +00:00
• 5dd2fd5369 Fix crash on contract of unbounded doubly linked lists Claire Dross 2025-04-23 14:34:35 +02:00
• e2263bd4a1 Merge branch 'topic/898-dross-splice' into 'master' Claire Dross 2025-04-16 07:11:10 +00:00