Johannes Kanig
a5db3bd18c
Merge branch 'topic/628-kanig-alt-ergo-sparklib' into '24.2'
...
Fix SPARKlib sessions after alt-ergo change
Issue: eng/spark/spark2014#628
See merge request eng/spark/sparklib!50
2024-05-24 08:44:22 +00:00
Johannes Kanig
c168cf54a7
Fix SPARKlib sessions after alt-ergo change
2024-05-24 17:42:39 +09:00
Yannick Moy
c2543114ce
Merge branch 'wip/sparklib-warning' into 'master'
...
Type variables from SPARKlib projects to avoid GPRbuild warnings
See merge request eng/spark/sparklib!20
2023-08-01 13:32:30 +00:00
Yannick Moy
647579cd3c
Type variables from SPARKlib projects to avoid GPRbuild warnings
...
When variables are untyped, GPRbuild may emit a warning on case constructs
without "others" as found in SPARKlib projects.
2023-08-01 15:20:12 +02:00
Yannick Moy
c68e7c4e30
Merge branch 'wip/moy-55-spark-internal' into 'master'
...
Use common project file for internal testing of SPARKlib
Issue: eng/spark/spark2014#55
See merge request eng/spark/sparklib!19
2023-07-27 14:30:08 +00:00
Yannick Moy
21ace05153
Use common project file for internal testing of SPARKlib
...
Avoid having a separate project file sparklib_internal.gpr for the
testing of SPARKlib. Instead use project variable SPARK_Body_Mode to
decide on values relevant for internal testing and analysis.
Issue: eng/spark/spark2014#55
2023-07-27 15:38:36 +02:00
Yannick Moy
5628249e30
Merge branch 'wip/moy-55-sparklib-dev' into 'master'
...
Adapt the project files for the dev setup
Issue: eng/spark/spark2014#55
See merge request eng/spark/sparklib!18
2023-07-26 13:38:26 +00:00
Yannick Moy
94a51bce74
Adapt the project files for the dev setup, and setup.sh script
...
Issue: eng/spark/spark2014#55
2023-07-26 12:32:48 +02:00
Yannick Moy
5a6df4112a
Merge branch 'wip/moy-55-sparklib' into 'master'
...
Update tests to work with new SPARKlib projects
Issue: eng/spark/spark2014#55
See merge request eng/spark/sparklib!17
2023-07-26 08:40:13 +00:00
Yannick Moy
d7b4f6f901
Update SPARKlib project files to remove use of SPARKLIB_OBJECT_DIR
...
SPARKlib was forcing the definition of a global variable to define
a suitable object file for compiling its sources when used in a client
project. This was not ideal, as use of a local path meant that the object
directory was created directly inside SPARK installation, instead of being
local to the client directories.
Now SPARKlib projects are divided into "external" ones which cannot be used
directly, as they specify Externally_Built to be True, and "model" projects that
a user should copy and adapt to their usage, in terms of Object_Dir and
Excluded_Source_Files. The model ones extends the external ones.
Issue: eng/spark/spark2014#55
2023-07-26 00:50:16 +02:00
Yannick Moy
e00fc27765
Update tests to work with new SPARKlib projects
...
Issue: eng/spark/spark2014#55
2023-07-25 14:54:39 +02:00
Johannes Kanig
0c72ea85c7
Merge branch 'topic/246-kanig-sparklib' into 'master'
...
Fix proof of SPARK library
Issue: eng/spark/spark2014#246
See merge request eng/spark/sparklib!16
2023-07-06 07:56:32 +00:00
Johannes Kanig
a5f8179ccb
Fix proof of SPARK library
...
* generate_session.py
- show proved VC when running Coq; this helps detect when the
--limit-line argument is incorrect
- delete more files
- remove useless level argument to call of run_automatic
* manual_proof.in: fixed locations of checks
* lemma_raising_order_*.prf: fixed proof of lemma, the proof is now much
simpler
2023-07-06 11:03:57 +09:00
Joffrey Huguet
5a49901322
Merge branch 'topic/255-kanig-exclude' into 'master'
...
More files to be excluded from sparklib_light project
Issue: eng/spark/spark2014#255
See merge request eng/spark/sparklib!15
2023-07-05 11:40:32 +00:00
Johannes Kanig
89cb85e60c
More files to be excluded from sparklib_light project
2023-07-05 18:21:25 +09:00
Johannes Kanig
35200d29ba
Merge branch 'topic/255-kanig-exclude' into 'master'
...
Exclude invalid file names from projects
Issue: eng/spark/spark2014#255
See merge request eng/spark/sparklib!14
2023-06-21 08:43:21 +00:00
Johannes Kanig
83c57fb5fe
Exclude invalid file names from projects
2023-06-21 16:10:56 +09:00
Yannick Moy
02769a20c4
Merge branch 'wip/moy-237-dependency' into 'master'
...
Add missing private dependency
Issue: eng/spark/spark2014#237
See merge request eng/spark/sparklib!13
2023-06-08 13:59:49 +00:00
Yannick Moy
dd731ff9dd
Add missing private dependency
...
This missing dependency leads to nameres failures when analyzing
code with LAL.
Issue: eng/spark/spark2014#237
2023-06-05 16:23:52 +02:00
Martin Clochard
ac469598b3
Merge branch 'topic/209-clochard-space-style' into 'master'
...
Adds missing spaces for style
Issue: eng/spark/spark2014#209
See merge request eng/spark/sparklib!12
2023-06-01 13:09:08 +00:00
Martin Clochard
4c7eeb4f0d
Adds missing spaces for style
2023-06-01 15:01:55 +02:00
Martin Clochard
aa5933c728
Merge branch 'topic/209-clochard-add-iterable-exemption' into 'master'
...
Add gnatcheck exemption for Iterable occurrences.
Issue: eng/spark/spark2014#209
See merge request eng/spark/sparklib!11
2023-06-01 08:43:59 +00:00
Martin Clochard
fb8f1a8f02
Add gnatcheck exemption for Iterable occurrences.
2023-05-30 14:43:16 +02:00
Claire Dross
d32720d58d
Merge branch 'topic/26-dross-add-terminates-on-generics' into 'master'
...
Add Always_Terminates annotation on nested generics inside containers
Issue: eng/spark/spark2014#26
See merge request eng/spark/sparklib!10
2023-05-25 14:51:13 +00:00
Claire Dross
f9c2536473
Add Always_Terminates annotation on nested generics inside containers
...
The aspect Always_Terminates is not inherited from parents of generic
units. State it explicitly.
2023-05-25 16:01:22 +02:00
