Add a new swicth --gnattest_values to indicate the json in
which values should be read.
Add the logic to parse these values and use them as counter examples.
Issue: #908
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
