Piotr Trojanek
add6393de0
Merge branch 'topic/rac_concat_check' into 'master'
...
Add missing range check to concatenation operator in RAC
Issue: eng/spark/spark2014#1199
See merge request eng/spark/spark2014!2576
2026-02-12 14:47:18 +01:00
Piotr Trojanek
b6ea3bd887
Add range check to concatenation operator in RAC
...
[changelog]
* src/counterexamples/ce_rac.adb
(RAC_Binary_Op): Add missing check on concatenation operator.
* testsuite/gnatprove/tests/1119__concat_ce/
Now we have a good counterexample.
* testsuite/gnatprove/tests/O709-030__concat_string/test.out
The CEs are good, just that the first one is badly displayed.
2026-02-12 14:46:55 +01:00
Piotr Trojanek
48d8862baa
Use existing renaming in RAC code for concatenation
2026-02-12 14:46:55 +01:00
Piotr Trojanek
13434116d4
Add test with missing counterexample on string concatenation
2026-02-12 14:46:55 +01:00
Johannes Kanig
8a4b0aff07
Merge branch 'topic/kanig-1099-large' into 'master'
...
Improve job status based on timing violation
Issue: eng/spark/spark2014#1099
See merge request eng/spark/spark2014!2586
2026-02-12 09:16:57 +00:00
Johannes Kanig
1b8773df0c
Apply 1 suggestion(s) to 1 file(s)
...
Co-authored-by: Piotr Trojanek <trojanek@adacore.com >
2026-02-11 23:35:54 +00:00
Johannes Kanig
ea51a9627b
Improve job status based on large test violation
2026-02-11 23:35:54 +00:00
Claire Dross
346742a22a
Merge branch 'topic/1184-test-update' into 'master'
...
Missing large test updates
Issue: eng/spark/spark2014#1184
See merge request eng/spark/spark2014!2587
2026-02-11 11:14:40 +00:00
Claire Dross
e0c189acf6
Missing large test updates
2026-02-11 11:14:18 +00:00
Piotr Trojanek
83ccfd6454
Merge branch 'topic/kill_wait' into 'master'
...
Reclaim why3server resources after killing it
Issue: eng/spark/spark2014#1211
See merge request eng/spark/spark2014!2585
2026-02-11 11:10:21 +01:00
Piotr Trojanek
c0d87d81f8
Reclaim why3server resources after killing it
...
Child processes that have been killed are still managed by the GNAT runtime,
at least on Windows. To really forget about them we need to call Wait_Process.
[changelog]
* src/gnatprove/gnatprove.adb
(Flow_Analysis_And_Proof): Add cleanup.
2026-02-11 11:09:57 +01:00
Claire Dross
31aee052ca
Merge branch 'topic/1184-dross-annotate' into 'master'
...
Use kinds for incorrect uses of annotations
Issue: eng/spark/spark2014#1184
See merge request eng/spark/spark2014!2581
2026-02-11 07:28:46 +00:00
Claire Dross
217c994941
Use kinds for incorrect uses of annotations
2026-02-10 17:34:43 +01:00
Claire Dross
ff1dbbba77
Merge branch 'topic/1184-dross-lrm-references' into 'master'
...
Add more LRM references for violations
Issue: eng/spark/spark2014#1184
Depends-On: eng/toolchain/acats!755
See merge request eng/spark/spark2014!2573
2026-02-10 10:18:49 +00:00
Claire Dross
ee3a77155e
Add more LRM references for violations
2026-02-10 10:18:26 +00:00
Johannes Kanig
9141eac132
Merge branch 'automated-submodule-update-723d72a7' into 'master'
...
Automatic submodule commit
no-issue-check
See merge request eng/spark/spark2014!2584
2026-02-10 09:44:55 +00:00
eng-bot
0829d5083d
Automatic submodule commit
2026-02-10 09:44:39 +00:00
Claire Dross
b7210ab527
Merge branch 'topic/1187-dross-proof-cyclic' into 'master'
...
Improve warnings for proof dependencies
Issue: eng/spark/spark2014#1187
Depends-On: eng/spark/sparklib!234
Depends-On: eng/spark/spark-internal-testsuite!422
See merge request eng/spark/spark2014!2574
2026-02-10 09:29:09 +00:00
Claire Dross
2a2ddad4d3
Improve warnings for proof dependencies
...
Now emit a warning for each subprogram that is proof cyclic, listing
the information that might be missing. The warning is emitted during
proof, so it is only present when proof is attempted on the subprogram.
2026-02-10 09:28:43 +00:00
Johannes Kanig
a8a8ab567a
Merge branch 'topic/kanig-1454-kill' into 'master'
...
Avoid calling GNAT.OS_Lib.Kill_Process_Tree
Issue: eng/spark/spark2014#1454
See merge request eng/spark/spark2014!2583
2026-02-10 01:15:31 +00:00
Johannes Kanig
abf11f2f76
Avoid calling GNAT.OS_Lib.Kill_Process_Tree
...
Instead we make sure the why3server kills its own children and only kill
the server.
2026-02-10 09:21:24 +09:00
Claire Dross
71caed2b84
Merge branch 'topic/1184-dross-refactor-limitations' into 'master'
...
Refactor handling of root cause for limitations
Issue: eng/spark/spark2014#1184
See merge request eng/spark/spark2014!2564
2026-02-09 10:10:05 +00:00
Claire Dross
5a7e90a2a2
Refactor handling of root cause for limitations
2026-02-09 10:07:02 +00:00
Johannes Kanig
45a5a5c978
Merge branch 'revert-338cf5b3' into 'master'
...
Revert "Adaptations to merge of spark2014 specs in anod"
Issue: eng/spark/spark2014#1062
Depends-On: eng/shared/anod!7937
See merge request eng/spark/spark2014!2577
2026-02-09 10:02:51 +00:00
Johannes Kanig
08da2c7776
Revert "Merge branch 'topic/kanig-1062-core' into 'master'"
...
This reverts merge request !2496
2026-02-09 09:06:28 +00:00
