The SPARK plugin for GS offered two options to perform proof
at the VC level: one going through Coq, and one going through Why3
tactics. Only the first one remains. The second one is removed
because it is too complex to use.
Remove generated menu file for the GS plugin, as well as code to
generate this file.
Update the UG and develguide docs to reflect that change.
Update the why3 commit after removal of code for manual proof.
* configuration.adb
(Set_Provers): remove check for cvc4 (obsolence message)
* gnatprove.conf: remove cvc4 configuration
* P804-001__driver: the test configuration now uses a modified version
of cvc5 instead of a modified version of cvc4
* remove cvc4 from various plans
* update why3menus.py for manual proof menus
GNATprove now generates data representation in JSON format by calling
the appropriate compiler for the target on sources of the project,
passing switches -gnatc to only perform semantic analysis and -gnatR2js
to generate a JSON file for every source input file, containing entries
for all source types and objects.
This generation takes place in a preliminary step of GNATprove, prior
to generating ALI files with global variable information. In the
translation phase to Why3, the JSON files for all sources in the closure
of the current main are read to populate a global table with data
representation information on types and objects, represented by their
location string.
Whenever translation hits a size or alignment attribute, it checks if
the corresponding value is not present in the global data representation
information, and retrieves it if present.
A new unit GNAT2Why.Data_Decomposition is defined to group the new variable
and subprogram for data decomposition.
Issue: eng/spark/spark2014#158
Issue: eng/spark/spark2014#168
Add a precommit check to avoid committing testsuite markers such as
"SOUNDNESS BUG" in test output.
* check-empty-file.py: add comment
* check-testsuite-markers.py: new script to check for the testsuite
markers
* .pre-commit-config.yaml: add a hook for the new script for .out files.
Add a new switch to Gnatprove to enable more logging by why3.
* configuration.adb
(Parse_Switches): add switch --why3-logging
(Compute_Why3_Args): pass switch to Why3 if enabled
- Config mostly taken from anod repository
- Make all python files compliant
- Remove some obviously unused python files (still in python2
syntax)
Change-Id: Ie90715f9e6e0a4831613faf0e9472706e210a7af
Fix newlines to "\n" so that on windows, the script does not write
"\r\n", which would lead to style errors.
Change-Id: I0e61ae24dd9f898594859a76769b30ccb9366f36
Tiny performance improvement for a regexp pattern that was computed for each
line of the input file.
* scripts/why3keywords.py
(regexp): Now a precomputed pattern.
no-tn-check
Change-Id: Icf91e1142680166954bec3a9b0e8a8b80f7696cc
Address a complaint from pre-commit-check style checker:
E741 ambiguous variable name 'l'
whose full description and advise are respectively:
"Variables named I, O, and l can be very hard to read. This is because the
letter I and the letter l are easily confused, and the letter O and the
number 0 can be easily confused.
Change the names of these variables to something more descriptive."
* scripts/why3keywords.py
(find_keywords): Rename "l" to "line".
no-tn-check
Change-Id: Iabcc003677fdc1e52292814e81e56efd102a656a
