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

• afa350ea73 Merge branch 'topic/kanig/728-branchbaseline' into '25.1' Johannes Kanig 2024-10-23 07:20:19 +00:00
• 68f698182f Various baseline and session updates Johannes Kanig 2024-10-08 10:22:29 +09:00
• 7472902938 Rename primitives to insert vectors in formal vectors Claire Dross 2024-10-21 11:36:23 +02:00
• 50582052ef Merge branch 'cherry-pick-8fa47fdc' into '25.1' Claire Dross 2024-10-21 07:45:40 +00:00
• cfa39084c1 Merge branch 'topic/dross-735-multisets' into 'master' Claire Dross 2024-10-17 07:36:13 +00:00
• 3dd6f7d190 Merge branch 'topic/dross-625-hashed-containers' into '25.1' Claire Dross 2024-10-21 07:42:52 +00:00
• d2d8c44281 Move formal hash_tables from gnat repo to sparklib Claire Dross 2024-10-10 16:30:00 +02:00
• 2d01f00de7 Merge branch 'topic/dross-625-hashed-containers' into 'master' Claire Dross 2024-10-11 13:39:45 +00:00
• ec8d16acc4 Also use hash_tables from SPARKlib in unbounded containers Claire Dross 2024-10-11 15:31:32 +02:00
• d8e98e6fda Merge branch 'topic/dross-625-hashed-containers' into 'master' Claire Dross 2024-10-11 09:49:08 +00:00
• 833e3c5b4a Move formal hash_tables from gnat repo to sparklib Claire Dross 2024-10-10 16:30:00 +02:00
• 8fa47fdca8 Merge branch 'topic/dross-735-multisets' into 'master' Claire Dross 2024-10-11 08:00:12 +00:00
• ec7a9e2ca2 Change the definition of Invariant on Multisets Claire Dross 2024-10-08 12:12:29 +02:00
• 106bdfeecd Merge branch 'topic/728-kanig-testsuite' into 'master' Johannes Kanig 2024-10-08 07:53:12 +00:00
• 6482e7578b Various baseline and session updates Johannes Kanig 2024-10-08 10:22:29 +09:00
• 562f599127 Merge branch 'topic/665-dross-formal-maps-test' into 'master' 25.0 Claire Dross 2024-09-16 09:31:37 +00:00
• 3c40d17212 File test for hashed maps Claire Dross 2024-09-13 12:56:09 +02:00
• 198d85960f Merge branch 'topic/665__resize' into 'master' Claire Dross 2024-09-13 10:40:49 +00:00
• abc67b3791 Enable test for Resize on unbounded containers Claire Dross 2024-09-13 11:59:32 +02:00
• 484a82b58c Merge branch 'topic/665-dross-formal-sets-test' into 'master' Claire Dross 2024-09-12 13:07:50 +00:00
• b3e0897271 Use Include in test for Include for hashed sets Claire Dross 2024-09-12 14:46:09 +02:00
• d66c83ec0d Merge branch 'topic/none-huguet-update-tests' into 'master' Joffrey Huguet 2024-09-11 15:17:26 +00:00
• 23dce0441c Use no_crash instead of prove_all in quality tests Joffrey Huguet 2024-09-11 15:42:33 +02:00
• 1d77d49777 Merge branch 'topic/665-dross-formal-set-test' into 'master' Claire Dross 2024-09-11 15:00:48 +00:00
• 6ffd242015 File tests for hashed sets Claire Dross 2024-09-09 11:21:36 +02:00
• c0bd6086c5 Merge branch 'topic/713-dross-logical-eq-in-hashed-sets' into 'master' Claire Dross 2024-09-10 08:39:10 +00:00
• c266f32a85 Use logical equal in posts of unbounded hashed sets Claire Dross 2024-09-09 15:51:07 +02:00
• 2ab21ead94 Merge branch 'topic/none-huguet-update-tests' into 'master' Joffrey Huguet 2024-09-06 16:07:56 +00:00
• f18f63b571 Update test output Joffrey Huguet 2024-09-06 15:44:21 +02:00
• edb75bad32 Merge branch 'topic/709-dross-replace_element' into 'master' Claire Dross 2024-09-05 08:31:11 +00:00
• da7a619336 Remove incorrect postcondition on Replace_Element Claire Dross 2024-09-04 14:13:17 +02:00
• b2665e93b8 Merge branch 'topic/665-dross-formal-vector-test' into 'master' Claire Dross 2024-09-04 09:53:47 +00:00
• 7ee2771c18 Add tests for formal vectors Claire Dross 2024-09-03 15:35:54 +02:00
• d2b1d8fd18 Merge branch 'topic/665-dross-formal-list-test' into 'master' Claire Dross 2024-09-02 09:55:03 +00:00
• c0dde73fb1 File test for formal doubly linked lists Claire Dross 2024-07-29 11:54:04 +02:00
• 0e8ad0053a Merge branch 'topic/665-add-test-for-functional-map' into 'master' Claire Dross 2024-09-02 08:52:31 +00:00
• 230f1c157a Add test for functional maps Claire Dross 2024-07-26 14:02:51 +02:00
• 2193d2a132 Merge branch 'topic/700-dross-splice' into 'master' Claire Dross 2024-08-01 08:44:25 +00:00
• a86fcb90f1 In Splice, insert elements in the order of Source Claire Dross 2024-07-31 18:11:04 +02:00
• ea67529abf Merge branch 'topic/698-dross-splice' into 'master' Claire Dross 2024-07-31 16:10:12 +00:00
• a35695ba10 Fix crash in Splice on empty source for doubly linked lists Claire Dross 2024-07-31 12:39:18 +02:00
• f840be3009 Merge branch 'topic/697-dross-delete_last' into 'master' Claire Dross 2024-07-31 11:08:35 +00:00
• f5ba524a55 Minor fixes in Doubly_Linked_Lists Claire Dross 2024-07-30 17:47:31 +02:00
• 7db8030f82 Merge branch 'topic/665-add-test-for-functional-set' into 'master' Claire Dross 2024-07-30 10:05:01 +00:00
• e659880f8c File tests for functional sets Claire Dross 2024-07-25 14:59:08 +02:00
• 8b2df9dfe2 Merge branch 'topic/694-dross-ghost-iteration-on-functional-sets-and-maps' into 'master' Claire Dross 2024-07-29 11:21:18 +00:00
• 259152f0bf Add ghost aspects to iteration primitives on functional sets and maps Claire Dross 2024-07-26 16:23:36 +02:00
• 79c64393c2 Merge branch 'topic/693-quantification-not-executable' into 'master' Claire Dross 2024-07-25 12:28:16 +00:00
• 9b892ad277 Do not use quantification in functional set body Claire Dross 2024-07-25 11:03:27 +02:00
• 600a6ebaa1 Merge branch 'topic/693-dross-is_singleton-post' into 'master' Claire Dross 2024-07-24 08:06:00 +00:00
• c5283e76d4 Extend postcondition of Is_Singleton on functional sets Claire Dross 2024-07-23 10:37:23 +02:00
• a77d77a79a Merge branch 'topic/665-add-test-for-functional-vector' into 'master' Claire Dross 2024-07-23 08:07:16 +00:00
• f38288025d File test for functional vectors Claire Dross 2024-07-22 16:35:22 +02:00
• 83a7ce4c99 Merge branch 'topic/693-short-circuit-in-is_singleton' into 'master' Claire Dross 2024-07-22 15:40:29 +00:00
• 6668e9a6f7 Use a short-circuit operator in Is_Singleton Claire Dross 2024-07-22 17:37:25 +02:00
• b68fac6be5 Merge branch 'topic/665-add-tests-for-c-strings' into 'master' Claire Dross 2024-07-18 07:34:51 +00:00
• e5b32eed7f Add unit tests for SPARK.C.Strings and SPARK.C.Constant_Strings Claire Dross 2024-07-17 16:29:07 +02:00
• 4021a21c93 Merge branch 'topic/688-c-strings-free' into 'master' Claire Dross 2024-07-18 07:34:35 +00:00
• 5e102d7b90 Add Depends contract to SPARK.C.Strings.Free Claire Dross 2024-07-17 15:20:03 +02:00
• 50a451b1f0 Merge branch 'topic/665-move-proof-tests' into 'master' Claire Dross 2024-07-16 13:54:04 +00:00
• 2f369bc52b Move tests for the proof of sparklib units to the sparkilb repo Claire Dross 2024-07-16 12:32:44 +02:00
• 325ae7aab3 Merge branch 'topic/669-dross-update-comments' into 'master' Claire Dross 2024-06-28 10:05:00 +00:00
• 8713b89241 Add preconditions to Generic_Keys.Key in formal sets Claire Dross 2024-06-27 15:28:04 +02:00
• 60cbe2ebec Remove obsolete comments at the top of formal sets and maps Claire Dross 2024-06-27 16:02:22 +02:00
• d3069f657f Merge branch 'topic/637-huguet-sparklib-alire' into 'fsf-14' fsf-14 Joffrey Huguet 2024-06-28 09:04:16 +00:00
• eff4cf2a48 Simplify sparklib.gpr for Alire Joffrey Huguet 2024-06-17 12:49:28 +02:00
• 38bae84075 Merge branch 'topic/637-huguet-change-filenames' into 'master' Joffrey Huguet 2024-06-26 09:08:27 +00:00
• 42578b97a6 Change project file names Joffrey Huguet 2024-06-20 18:01:48 +02:00
• c03d47d89b Merge branch 'topic/dross-remove-tagged-type-in-light' into 'master' Claire Dross 2024-06-20 15:18:57 +00:00
• 5d36765d89 Remove tagged types in sparklib light Claire Dross 2024-06-20 14:10:59 +02:00
• 74668d6223 Merge branch 'topic/dross-minor-add-ghost-on-vet' into 'master' Claire Dross 2024-06-17 14:03:02 +00:00
• 4368bf25bb Add Ghost aspect on the internal function Vet Claire Dross 2024-06-17 15:27:37 +02:00
• 5f5d5bb75a Merge branch 'topic/628-kanig-lemmas' into 'master' Johannes Kanig 2024-06-11 09:28:19 +00:00
• 3cb27a1b84 Update sparklib sessions after alt-ergo update Johannes Kanig 2024-06-11 18:17:34 +09:00
• 26696af0b0 Merge branch 'topic/603-clochard-underspec-in-sparklib' into 'master' Martin Clochard 2024-06-04 13:38:52 +00:00
• a2f615e967 Fix underspecification of Model functions in formal vectors Martin Clochard 2024-06-04 12:10:03 +02:00
• 0e0bd8ac96 Merge branch 'topic/615-string-hash' into 'master' Claire Dross 2024-05-30 16:29:27 +00:00
• 5383534bed Add a new package for lemmas on hash functions in Containers Claire Dross 2024-05-30 15:27:41 +02:00
• a5db3bd18c Merge branch 'topic/628-kanig-alt-ergo-sparklib' into '24.2' 24.2 24-sustained Johannes Kanig 2024-05-24 08:44:22 +00:00
• c168cf54a7 Fix SPARKlib sessions after alt-ergo change Johannes Kanig 2024-05-24 17:42:13 +09:00
• e0128b8349 Merge branch 'topic/634-kanig-checks' into 'master' Johannes Kanig 2024-05-22 11:11:56 +00:00
• 688e34e0ec Add more checks to sparklib pre-commit checks Johannes Kanig 2024-05-22 17:57:41 +09:00
• 0d6957e38e Merge branch 'topic/598-dross-functional-light' into 'master' Claire Dross 2024-04-18 09:37:25 +00:00
• 224092dc50 Factorize Default_Switches Claire Dross 2024-04-18 09:52:30 +02:00
• 924d2ce2bd Make big integers executable in light with SPARK_Body => On Claire Dross 2024-04-11 17:42:13 +02:00
• beccaffe0a Keep bodies of functional containers in light Claire Dross 2024-04-11 14:25:33 +02:00
• 0873c409de Merge branch 'topic/547-kanig-ref' into 'master' Johannes Kanig 2024-04-08 08:13:39 +00:00
• 9a75242bcf Add back with of unit for pragma Export Johannes Kanig 2024-04-08 17:02:50 +09:00
• fb92a2dc19 Merge branch 'topic/547-kanig-check' into 'master' Johannes Kanig 2024-04-05 07:06:21 +00:00
• 40d574f2b3 Improve style checking options for SPARKlib and clean up Johannes Kanig 2024-04-04 18:26:48 +09:00
• ded2176fac Merge branch 'topic/nodiff' into 'master' Johannes Kanig 2024-04-04 00:53:33 +00:00
• 9e4813f07a address style warnings Johannes Kanig 2024-04-03 18:52:35 +09:00
• 6c4b06d102 add gitlab CI Johannes Kanig 2024-04-03 17:36:21 +09:00
• c0ee2b12c2 Add pre-commit check for style checking Johannes Kanig 2024-04-03 17:28:28 +09:00
• b5aa3ec94b Merge branch 'topic/nodiff' into 'master' Johannes Kanig 2024-04-03 07:59:52 +00:00
• d56ed649e4 Merge branch 'topic/kanig-sessions' into 'master' Johannes Kanig 2024-04-03 07:59:06 +00:00
• 5e50336758 hide diffs on session files in diffs Johannes Kanig 2024-04-03 16:54:50 +09:00
• 9c2f4c308f update why3 sessions for SPARK lib Johannes Kanig 2024-04-03 16:50:49 +09:00
• f9196b4acc Merge branch 'topic/571-clochard-no-strict-aliasing' into 'master' Martin Clochard 2024-03-21 15:18:18 +00:00
• aa4b7aa8ed Remove warning in test output Martin Clochard 2024-03-21 15:49:11 +01:00