diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2011-09-27 12:03:09 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2011-09-27 12:03:09 +0200 |
| commit | da124b6afd64364d321813cee77442a1de624ec5 (patch) | |
| tree | 119eb2e20370d17d8cd10aad56e8c0dc1560c851 /gcc/ada/gnat1drv.adb | |
| parent | 706a4067b883765331b693caded5f08a43eb2645 (diff) | |
| download | gcc-da124b6afd64364d321813cee77442a1de624ec5.tar.gz | |
[multiple changes]
2011-09-27 Robert Dewar <dewar@adacore.com>
* a-comutr.ads: Minor reformatting.
2011-09-27 Ed Schonberg <schonberg@adacore.com>
* a-cimutr.adb, a-cimutr.ads, a-cbmutr.adb, a-cbmutr.ads: Add children
iterators to multiway trees.
2011-09-27 Yannick Moy <moy@adacore.com>
* debug.adb (d.D): New option for strict Alfa mode.
* opt.ads (Strict_Alfa_Mode): New flag to interpret compiler
permissions as strictly as possible.
* sem_ch3.adb (Signed_Integer_Type_Declaration): In non-strict
Alfa mode, now, interpret ranges of base types like GNAT does; in
strict mode, simply change the range of the implicit base Itype.
* gnat1drv.adb: Update comments. Set Strict_Alfa_Mode.
From-SVN: r179258
Diffstat (limited to 'gcc/ada/gnat1drv.adb')
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index bf811eb5fb5..57456cc67ff 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -392,6 +392,12 @@ procedure Gnat1drv is Alfa_Mode := True; + -- Set strict standard interpretation of compiler permissions + + if Debug_Flag_Dot_DD then + Strict_Alfa_Mode := True; + end if; + -- Turn off inlining, which would confuse formal verification output -- and gain nothing. @@ -428,6 +434,8 @@ procedure Gnat1drv is Debug_Generated_Code := False; -- Turn cross-referencing on in case it was disabled (e.g. by -gnatD) + -- as it is needed for computing effects of subprograms in the formal + -- verification backend. Xref_Active := True; @@ -473,13 +481,15 @@ procedure Gnat1drv is Warning_Mode := Suppress; - -- Suppress the generation of name tables for enumerations - -- why??? + -- Suppress the generation of name tables for enumerations, which are + -- not needed for formal verification, and fall outside the Alfa + -- subset (use of pointers). Global_Discard_Names := True; - -- Suppress the expansion of tagged types and dispatching calls - -- why??? + -- Suppress the expansion of tagged types and dispatching calls, + -- which lead to the generation of non-Alfa code (use of pointers), + -- which is more complex to formally verify than the original source. Tagged_Type_Expansion := False; end if; |