Commit Graph

  • d4b2a1e6f1 Do not introduce overflow checks for 'Length on universal integers Claire Dross 2026-01-23 12:35:53 +01:00
  • d151d09c3f Do not introduce overflow checks for 'Length on universal integers Claire Dross 2026-01-23 12:35:53 +01:00
  • bbce283c00 Merge branch 'topic/kanig-1155-error2' into 'master' Johannes Kanig 2026-01-28 10:46:58 +00:00
  • c6d4ae1e75 Extra msg argument for Error_Msg_N Johannes Kanig 2026-01-28 18:34:10 +09:00
  • 024ded3e5b Merge branch 'topic/kanig-1155-error' into 'master' Johannes Kanig 2026-01-28 09:29:45 +00:00
  • b449d11035 Support for error message kinds Johannes Kanig 2026-01-28 09:17:35 +09:00
  • 09ee3d327c Merge branch 'topic/blake3-squeeze' into 'master' Piotr Trojanek 2026-01-28 10:00:48 +01:00
  • ec8584fba4 Update session files for large tests with names squeezed by Blake3 Piotr Trojanek 2026-01-27 14:40:57 +01:00
  • 71e5881833 Switch from SHA1 to Blake3 to squeeze long Why3 filenames Piotr Trojanek 2026-01-27 01:06:42 +01:00
  • 23ad454399 Merge branch 'topic/25.2-invalid_data_representation' into '25.2' 25.2 Piotr Trojanek 2026-01-27 15:13:49 +01:00
  • b7680e3888 Merge branch 'topic/create_record_tree' into 'master' Piotr Trojanek 2026-01-27 12:30:13 +01:00
  • 50827c6fa5 Add test for coverage with empty global whose extensions are visible Piotr Trojanek 2026-01-21 15:58:16 +01:00
  • deee30efd2 Create record tree together with initial and final vertices Piotr Trojanek 2026-01-20 16:40:15 +01:00
  • 3bfc995dee Include bounds vertices in record grouping Piotr Trojanek 2026-01-21 10:01:49 +01:00
  • f171265b17 Adapt test for broken GCC to work on Windows Piotr Trojanek 2026-01-27 00:31:36 +01:00
  • 5ef595517d Merge branch 'topic/blake3' into 'master' Piotr Trojanek 2026-01-27 12:01:19 +01:00
  • d877e3a881 Switch from SHA1 to Blake3 for mamcache Piotr Trojanek 2026-01-22 16:11:14 +01:00
  • 694c9a141c Switch from SHA1 to Blake3 when writing gnat2why options file Piotr Trojanek 2026-01-22 16:07:53 +01:00
  • 95e0a8ab00 Merge branch 'topic/1742-dross-file-test' into 'master' Claire Dross 2026-01-27 10:12:34 +00:00
  • 9b7a4429f9 File test for frontend issue Claire Dross 2026-01-26 10:46:18 +01:00
  • ecc26f7130 Merge branch 'topic/1179-dross-length' into 'master' Claire Dross 2026-01-27 10:11:45 +00:00
  • 8af36ae2a3 Do not introduce overflow checks for 'Length on universal integers Claire Dross 2026-01-23 12:35:53 +01:00
  • 9ce7b9fe93 Merge branch 'topic/1178-dross-refined-expr-fun' into 'master' Claire Dross 2026-01-23 16:51:18 +00:00
  • 7c59f69f79 Fix routine to detect if the completion of an expr fun is deferred Claire Dross 2026-01-23 13:01:45 +01:00
  • 814a7a10f1 Merge branch 'topic/1171-dross-ghost-program-exit' into 'master' Claire Dross 2026-01-23 16:50:31 +00:00
  • 703660266d Reject program exit in inlined ghost calls Claire Dross 2026-01-21 17:32:27 +01:00
  • 7c05a84fc0 Merge branch 'topic/1026-dross-nested-uu' into 'master' Claire Dross 2026-01-23 13:36:27 +00:00
  • 84009699da File test with nested contrained uu type without inferable discriminant Claire Dross 2026-01-22 10:55:24 +01:00
  • 35d2532b9d Merge branch 'topic/kanig-1176-disable' into 'master' Johannes Kanig 2026-01-23 09:27:08 +00:00
  • 34ef5d8451 Disable coverage to avoid build crash Johannes Kanig 2026-01-23 11:13:41 +09:00
  • 6b77ed0e84 Merge branch 'topic/1733-dross-assertion-levels' into 'master' Claire Dross 2026-01-22 14:32:06 +00:00
  • 05b3f7469c Allow ghost entity in aspects that apply to dependent ghost entities Claire Dross 2026-01-22 13:28:00 +01:00
  • 7fa212208c Merge branch 'topic/1026-dross-conv-UU' into 'master' Claire Dross 2026-01-22 10:01:16 +00:00
  • 720bf80174 Add a check on conversion from UU derived type Claire Dross 2026-01-21 16:41:44 +01:00
  • 5a0e1dd011 Merge branch 'topic/1168-dross-no-raise' into 'master' Claire Dross 2026-01-22 10:00:29 +00:00
  • 4d2d152e41 Detect inlined procedures with No_Raise Claire Dross 2026-01-21 18:03:39 +01:00
  • f92d99fbef Merge branch 'topic/toom/1172-xfail-test' into 'master' Andres Toom 2026-01-22 02:37:34 +02:00
  • 5ef962ecc3 Xfail test Andres Toom 2026-01-21 21:03:18 +02:00
  • 7113768195 Merge branch 'topic/toom/923-xfail-non-deterministic-test' into 'master' Andres Toom 2026-01-21 17:54:27 +02:00
  • 9a66b3f9cd xfail test with non-deterministic counterexample Andres Toom 2026-01-21 14:31:01 +02:00
  • f3c9f1c7da Merge branch 'topic/1171-dross-ghost-program-exit' into 'master' Claire Dross 2026-01-21 15:53:23 +00:00
  • fc1d1b5514 Do not reject Program_Exit on ghost subprograms Claire Dross 2026-01-20 16:02:17 +01:00
  • 0715c70528 Merge branch 'topic/1044-clochard-document-no-raise-in-finally' into 'master' Martin Clochard 2026-01-21 15:30:26 +00:00
  • 4641f50fbc Document that exceptions shall not escape finally section in SPARK Martin Clochard 2026-01-20 17:22:55 +01:00
  • 8c61ffb47c Merge branch 'topic/toom/P201-069-update-baseline' into 'master' Andres Toom 2026-01-21 16:34:02 +02:00
  • 8df10e1634 Revert "Update baseline: update proof failure reason" Andres Toom 2026-01-21 11:52:58 +02:00
  • 336450e5e9 Merge branch 'topic/1044-clochard-unexpected-raise-in-finally' into 'master' Martin Clochard 2026-01-21 09:42:06 +00:00
  • 50b802bf86 New test Martin Clochard 2025-09-19 17:34:56 +02:00
  • fb2cc3d469 Add reason for check for unexpected exceptions in finally sections Martin Clochard 2025-09-19 17:31:34 +02:00
  • c6b9ac0478 Merge branch 'topic/1161-clochard-spark-book-crash' into 'master' Martin Clochard 2026-01-21 09:38:41 +00:00
  • 15edbd30c9 Fix spark_book example Martin Clochard 2026-01-20 12:13:20 +01:00
  • d34b94a599 Merge branch 'topic/kanig-1170-xfail' into 'master' Johannes Kanig 2026-01-21 00:17:19 +00:00
  • d31ac92cbb Move tests to XFAIL Johannes Kanig 2026-01-20 18:24:30 +09:00
  • 13ed9b7872 Merge branch 'topic/aspect_pragma_priority' into 'master' Piotr Trojanek 2026-01-20 17:13:05 +01:00
  • 0fc96201a0 Pick main subprogram priority from aspect specification Piotr Trojanek 2026-01-19 23:21:54 +01:00
  • 4c598bbeff Merge branch 'topic/708-dross-external-initializer' into 'master' Claire Dross 2026-01-20 15:11:18 +00:00
  • 4cafb80b9b Imprecise support for External_Initialization Claire Dross 2026-01-16 14:51:46 +01:00
  • 5b1ef3a9d2 Merge branch 'topic/gnatformat-20260118' into 'master' Piotr Trojanek 2026-01-20 14:42:39 +01:00
  • 2da1700eff Ignore reformatting with gnatformat-20260118 while blaming Piotr Trojanek 2026-01-20 09:56:05 +01:00
  • fb11753841 Merge branch 'topic/1168-dross-no-raise' into 'master' Claire Dross 2026-01-20 11:22:21 +00:00
  • 6bbfd92e74 Accept No_Raise Claire Dross 2026-01-16 17:31:22 +01:00
  • 3503fed14c Merge branch 'topic/1164-dross-fix-tests' into 'master' Claire Dross 2026-01-20 11:16:39 +00:00
  • efd6c8ecf6 Regain proof lost after prover update Claire Dross 2026-01-19 14:39:30 +01:00
  • d12b384317 Merge branch 'topic/kanig-replay-cache' into 'master' Johannes Kanig 2026-01-20 09:38:04 +00:00
  • 34ccaae833 Disable cache on replay test Johannes Kanig 2026-01-20 18:00:04 +09:00
  • cc339473cf Merge branch 'topic/gnatformat-20260118' into 'master' Piotr Trojanek 2026-01-20 09:52:21 +01:00
  • f2cdae4627 Format code with gnatformat-20260118 Piotr Trojanek 2026-01-19 19:35:35 +01:00
  • 7734881d98 Merge branch 'topic/toom/1052-reduce-python-update-baseline' into 'master' Andres Toom 2026-01-19 19:30:16 +02:00
  • 36b7bc5024 Update baseline: update proof failure reason Andres Toom 2026-01-19 18:09:55 +02:00
  • 218c96492f Update baseline: remove extraneous backslash conversion Andres Toom 2026-01-19 12:43:34 +02:00
  • 6260613a81 Merge branch 'topic/toom/1052-reduce-python-calls-timeout' into 'master' Andres Toom 2026-01-19 16:09:03 +02:00
  • aec8dadaa7 Restore the default timeout 780 in tests Andres Toom 2026-01-19 12:02:18 +02:00
  • 66c5678431 Merge branch 'topic/kanig-515-pass' into 'master' Joffrey Huguet 2026-01-19 13:32:13 +00:00
  • 7c3bee4351 Re-enable CE after fix on cvc5 Johannes Kanig 2026-01-19 18:46:10 +09:00
  • d528d09b1d Merge branch 'topic/kanig-1152-baselines' into 'master' Joffrey Huguet 2026-01-19 11:27:56 +00:00
  • 1835a5cdba Baselines and sessions after prover updates Johannes Kanig 2026-01-19 18:22:51 +09:00
  • 37b4f9d3e1 Merge branch 'topic/kanig-baselines' into 'master' Johannes Kanig 2026-01-19 09:51:09 +00:00
  • d67c82221c Baselines in coq testsuite Johannes Kanig 2026-01-19 17:37:13 +09:00
  • 28b4881ed6 Merge branch 'topic/clochard-remove-unused-case' into 'master' Martin Clochard 2026-01-19 09:17:49 +00:00
  • 1b508f6bac Remove unused parameter Martin Clochard 2026-01-16 16:14:06 +01:00
  • aa4b4061da Merge branch 'topic/1165-dross-file-test' into 'master' Claire Dross 2026-01-16 14:35:28 +00:00
  • 0eab6c439a File test for pragma Short_Circuit_And_Or Claire Dross 2026-01-16 11:10:35 +01:00
  • 575d86e70c Merge branch 'topic/935-dross-extended-access' into 'master' Claire Dross 2026-01-16 14:33:45 +00:00
  • 9e308a0614 Support pragma Extended_Access Claire Dross 2026-01-16 11:48:08 +01:00
  • 39e9bfebb2 Merge branch 'topic/1167-dross-destructors' into 'master' Claire Dross 2026-01-16 14:32:57 +00:00
  • fa496cb474 Reject destructors as unsupported Claire Dross 2026-01-16 12:39:21 +01:00
  • 02738c21b7 Merge branch 'topic/kanig-1123-df' into 'master' Johannes Kanig 2026-01-16 10:41:21 +00:00
  • 5215a72e35 Monitor disk usage on most CI jobs Johannes Kanig 2026-01-16 11:04:49 +09:00
  • 7e7ebbf097 Merge branch 'topic/kanig-1152-baselines' into 'master' Johannes Kanig 2026-01-16 09:24:16 +00:00
  • 3d286f184d Further baseline updates Johannes Kanig 2026-01-15 10:52:21 +09:00
  • 110a965304 xfail spark_book test Johannes Kanig 2026-01-15 10:29:06 +09:00
  • 12de965222 further testsuite updates Johannes Kanig 2026-01-14 19:18:06 +09:00
  • 36f71dab20 Remove failed markers from tests for pre-commit checks Johannes Kanig 2026-01-13 19:41:01 +09:00
  • 0dc9182ab1 Testsuite updates for provers Johannes Kanig 2026-01-13 09:49:47 +00:00
  • aad888856b Merge branch 'topic/toom/1052-reduce-python-calls' into 'master' Andres Toom 2026-01-15 13:45:54 +02:00
  • 6445222d14 Merge branch 'cherry-pick-57e6fd5b' into '26.2' Claire Dross 2026-01-15 11:24:01 +00:00
  • 8057a7b3d7 Merge branch 'topic/1151-dross-array-attr' into 'master' Claire Dross 2026-01-14 16:11:45 +00:00
  • 7731875ae9 Run basic tests in the same Python process by default Andres Toom 2026-01-12 21:15:24 +02:00
  • 90f8c2c6eb Remove obsolete check for test.cmd Andres Toom 2026-01-12 00:55:26 +02:00
  • 2916747fa9 Remove obsolete __init.py__ from testsuite/lib Andres Toom 2026-01-12 00:16:08 +02:00