ada/SPARKlib
0
0
Fork 0
mirror of https://github.com/AdaCore/SPARKlib.git synced 2026-02-12 13:11:36 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 13b2546cd9 Merge branch 'topic/kanig-1103-format' into 'master' Johannes Kanig 2025-11-12 08:20:16 +00:00
  • ed6c50dd57 Line number changes after formatting Johannes Kanig 2025-11-11 11:14:54 +09:00
  • 30935e756e Formatting of sparklib Johannes Kanig 2025-11-10 11:00:17 +09:00
  • 4937310342 Merge branch 'topic/kanig-1103-testsuite' into 'master' Johannes Kanig 2025-11-07 10:56:23 +00:00
  • 7444724153 Update test output after line number changes Johannes Kanig 2025-11-07 18:39:27 +09:00
  • 48f07aa057 Merge branch 'topic/kanig-773-doc' into 'master' Johannes Kanig 2025-11-07 08:37:16 +00:00
  • 6709166f47 Documentation for new body mode Johannes Kanig 2025-11-07 11:27:52 +09:00
  • 6897243583 Merge branch 'topic/kanig-sparklib-coveraage' into 'master' Johannes Kanig 2025-11-07 08:20:35 +00:00
  • e601032a12 Commit new location of sparklib coverage manifest Johannes Kanig 2025-11-07 10:40:59 +09:00
  • e7fc1d3775 Merge branch 'topic/1070-dross-session-updates' into 'master' Claire Dross 2025-11-07 07:48:19 +00:00
  • cdce2c2177 Update proof for higher order properties of functional containers Claire Dross 2025-11-06 13:20:31 +01:00
  • f375c3ca08 Merge branch 'topic/kanig-773-format2' into 'master' Johannes Kanig 2025-11-07 01:44:36 +00:00
  • aa8fd0ddf0 Manual style checks Johannes Kanig 2025-11-06 10:40:52 +09:00
  • 4e68a6f67c automatic formatting Johannes Kanig 2025-11-06 10:43:10 +09:00
  • dda95017e5 Merge branch 'topic/merge_pr' into 'master' Joffrey Huguet 2025-11-06 09:43:20 +00:00
  • 3d59531543 Fix documentation link in the README Fernando Oleo Blanco 2025-09-03 16:00:31 +02:00
  • cc03b5d682 Merge branch 'topic/1070-dross-holders' into 'master' Claire Dross 2025-11-06 09:38:50 +00:00
  • 29ea903420 Factorize refcounted elements in a separate package Claire Dross 2025-11-03 11:35:11 +01:00
  • c7b4c9eb9b Merge branch 'topic/kanig-773-preproc' into 'master' Johannes Kanig 2025-11-06 00:33:10 +00:00
  • c3b6fee4dd test fixes and session updates Johannes Kanig 2025-11-04 18:37:29 +09:00
  • 2427855e09 Merge branch 'topic/fsf_merge_269/20251022' into 'fsf' Marc Poulhiès 2025-11-04 08:54:59 +01:00
  • 01816b8a72 Remove body mode from tests and use new test driver capabilities Johannes Kanig 2025-11-04 11:13:01 +09:00
  • 142211f785 Remove explicit bodymode setting Johannes Kanig 2025-11-03 11:41:13 +09:00
  • 3576f06136 Merge commit '2f5010e7213f592361b3bef6a87c302fe383f4d8' into topic/fsf_merge_269/20251022 Marc Poulhiès 2025-11-03 15:25:45 +01:00
  • 45a09e9d13 Replace preprocessor directives by custom markers Johannes Kanig 2025-06-13 10:18:32 +09:00
  • f698acefa4 Merge branch 'topic/kanig-773-contains' into 'master' Johannes Kanig 2025-11-03 09:52:42 +00:00
  • 989ed003a8 Remove useless 'contains_manual_proof' variable Johannes Kanig 2025-11-03 11:46:03 +09:00
  • 4a4242260a Merge branch 'topic/fsf_merge_269/20250925' into 'fsf' Marc Poulhiès 2025-10-30 10:32:02 +01:00
  • 295595fd86 Minor session updates Johannes Kanig 2025-09-18 17:54:21 +09:00
  • 721cdbd9d0 Move tests for the full runtime to large and update outputs Claire Dross 2025-09-16 20:00:15 +02:00
  • 958c4d8f15 Ensure that SPARKlib works with assertions enabled Claire Dross 2025-09-12 12:05:51 +02:00
  • 39f2c60c7e Update session test Claire Dross 2025-09-04 14:16:17 +02:00
  • adb5892924 Introduce assertion levels in the SPARKlib Claire Dross 2025-06-23 14:30:48 +02:00
  • 14be3d2a89 Update baselines for SPARKlib Johannes Kanig 2025-08-21 10:00:37 +09:00
  • b8a87ea4ac Update session tests and outputs Joffrey Huguet 2025-08-13 18:41:58 +02:00
  • ed45ca66af Repair session after support for continue Martin Clochard 2025-07-28 16:14:30 +02:00
  • 04acae6993 Update session files Claire Dross 2025-07-08 16:56:17 +02:00
  • cd11cbd81f Minor update to test outputs Claire Dross 2025-07-07 17:43:16 +02:00
  • 96e7f29dd0 Add comment to pragma Warnings Johannes Kanig 2025-06-26 10:20:24 +09:00
  • 0d13c5645a Update slocs after removing workaround for an elaboration issue Piotr Trojanek 2025-07-01 17:31:33 +02:00
  • 491c2856ce Deconstruct workaround for ghost elaboration entities in generic instances Piotr Trojanek 2025-06-30 11:27:32 +02:00
  • b641260df8 Remove workaround for ghost elaboration entities in generic instances Piotr Trojanek 2025-06-26 15:01:53 +02:00
  • 940af74c06 Fix sparklib tests after reorg Johannes Kanig 2025-06-25 10:30:02 +09:00
  • 7ecbe7633a Suppress spurious warning about underflow Johannes Kanig 2025-06-25 16:19:30 +09:00
  • 63d97a4d16 Move comment to more appropriate place Johannes Kanig 2025-06-20 09:30:33 +09:00
  • ec21ec761d Enable style checking for SPARKlib light Johannes Kanig 2025-06-20 08:47:39 +09:00
  • c67dba099c Restructure sparklib to use subfolders instead of file naming schemes Johannes Kanig 2025-06-16 10:39:48 +09:00
  • 1f34101015 update line numbers after source change Johannes Kanig 2025-06-18 18:20:16 +09:00
  • 643d6657f8 Session updates Johannes Kanig 2025-06-16 17:44:03 +09:00
  • ec38cd0505 Restore provability of floating-point arithmetic lemmas Claire Dross 2025-06-16 10:23:42 +02:00
  • eed4ff017f Minor diffs in warnings in test output Claire Dross 2025-05-16 09:56:09 +02:00
  • 0218520ab0 Baseline and session updates Johannes Kanig 2025-04-30 18:54:42 +09:00
  • e765676863 Session updates on multiset tests Claire Dross 2025-04-23 16:03:36 +02:00
  • 460c78ffb9 Use explicit component associations in Empty_Multiset Claire Dross 2025-04-23 14:48:33 +02:00
  • 53193ec540 Fix crash on contract of unbounded doubly linked lists Claire Dross 2025-04-23 14:34:35 +02:00
  • d56ac1b863 Fix incorrect contract on Splice in formal lists Claire Dross 2025-04-14 10:58:56 +02:00
  • 63e90bf3a1 Session files update Joffrey Huguet 2025-04-10 16:41:30 +02:00
  • e463c9ca12 Minor session updates Johannes Kanig 2025-04-03 18:58:11 +09:00
  • d573da9953 Update SPARKlib baselines Johannes Kanig 2025-03-31 18:31:09 +09:00
  • 591a0e2d83 Minor baseline update Johannes Kanig 2025-03-27 18:01:49 +09:00
  • bf293873ee update baseline for warning tag Johannes Kanig 2025-03-27 18:02:14 +09:00
  • 67ad67ccf7 Update sessions for alt-ergo SMT input Johannes Kanig 2025-03-25 18:05:48 +09:00
  • d373bd77b1 Remove slow part of the test Johannes Kanig 2025-03-12 09:47:36 +09:00
  • 21fd98b086 Session updates Johannes Kanig 2025-03-10 19:13:07 +09:00
  • 204a890f9b Update session tests Claire Dross 2025-03-05 09:01:42 +01:00
  • b4a03b1a2e Minor diffs in test outputs Claire Dross 2025-02-28 11:00:05 +01:00
  • 9fc1c4d4be Pass normal equality to model containers instead of logical equality Claire Dross 2025-02-26 16:32:11 +01:00
  • d71888309a Do not use operators on map models in formal containers Claire Dross 2025-02-26 15:55:25 +01:00
  • 82b5cd49d2 Do not use operators on sequence models in formal containers Claire Dross 2025-02-26 14:35:51 +01:00
  • 7c2099603b Simplify Reference functions in containers and pointers libraries Claire Dross 2025-02-13 12:12:04 +01:00
  • b90b651a92 Update tests outputs Joffrey Huguet 2025-02-19 17:03:53 +01:00
  • 007cf36188 Update test output and config Joffrey Huguet 2025-02-12 22:29:15 +01:00
  • f368ed23d5 Update sparklib baselines Johannes Kanig 2025-02-12 17:42:14 +09:00
  • 086a211277 bump pre-commit hooks version Johannes Kanig 2025-02-06 18:58:01 +09:00
  • 96cb73da8a Fix incorrect flake8 version Johannes Kanig 2025-02-04 19:01:35 +09:00
  • 13688f73e4 Bump flake8 and black versions Johannes Kanig 2025-02-04 09:53:34 +09:00
  • 04b9ec931d Update session files in proof tests Claire Dross 2025-02-03 16:12:52 +01:00
  • be3f631d6f Minor update line number in large container tests Claire Dross 2025-01-22 14:11:59 +01:00
  • 77e2e09e96 Add Ada_2022 pragma to hash table packages Claire Dross 2025-01-17 11:59:02 +01:00
  • bb36068a9d Baselines for cvc5 update Johannes Kanig 2025-01-20 19:41:35 +09:00
  • 5d077e7d47 sparklib baseline update after quantifier grouping Johannes Kanig 2025-01-17 09:34:57 +00:00
  • 4d53ecb180 Remove redundant parentheses inside unary operators Piotr Trojanek 2025-01-10 12:06:04 +01:00
  • c8def2b7cc Z3 baseline updates - mixed or negative Johannes Kanig 2025-01-07 19:24:40 +09:00
  • eecd026bf7 Z3 baseline updates - positive Johannes Kanig 2025-01-07 19:24:26 +09:00
  • c13ab596ce Enable assertions on tests Joffrey Huguet 2025-01-08 17:55:03 +01:00
  • 116d622c64 Update baseline for exit cases Johannes Kanig 2025-01-08 08:57:58 +00:00
  • f3704463c3 Copyright update Johannes Kanig 2025-01-06 09:49:38 +09:00
  • 44435f86ba Remove useless project indirection Johannes Kanig 2024-12-04 18:27:26 +09:00
  • f6342fcaec Hide internal URL Boris Yakobowski 2024-11-27 19:39:00 +01:00
  • 2b8888545d Remove private url for public packages Johannes Kanig 2024-11-26 17:22:47 +09:00
  • c227ba2778 Revert "SKIP tests on Windows" Johannes Kanig 2024-11-22 11:11:03 +09:00
  • 60ee6dfb35 Update test outputs Johannes Kanig 2024-11-22 11:08:13 +09:00
  • 0eab601113 SPARKlib tests: Use helper function from python library for compilation Johannes Kanig 2024-10-01 10:07:17 +09:00
  • 1cef0a3980 SKIP tests on Windows Joffrey Huguet 2024-11-21 14:58:39 +01:00
  • 090de66c8e Extend timeout for tests Joffrey Huguet 2024-11-21 14:46:41 +01:00
  • c76345f8d2 Add checking of opt files Johannes Kanig 2024-11-13 10:21:16 +09:00
  • 15258c9ccd Update session tests and outputs Joffrey Huguet 2024-11-04 18:09:55 +01:00
  • 8be9b951a6 Add SPARK_Mode Off to big integer conversions Claire Dross 2024-10-31 15:59:33 +01:00
  • 1002aad671 Fix project files of tests using SPARKlib Claire Dross 2024-10-28 14:53:19 +01:00
  • cf127f8b6f Stop using Big_Integers_Ghost in the SPARKlib Claire Dross 2024-10-25 09:32:21 +02:00