diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2014-01-20 13:44:07 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2014-01-20 13:44:07 +0000 |
| commit | c39cce408b9bbfdd8c3bf5851b6c8a6abd1e00a1 (patch) | |
| tree | 28136a11943ad5ecf1f77f1683891380d08d62e8 /gcc/ada/lib-writ.adb | |
| parent | b18c9f75f715306f7544e0141a74cf3cae21cc3c (diff) | |
| download | gcc-c39cce408b9bbfdd8c3bf5851b6c8a6abd1e00a1.tar.gz | |
2014-01-20 Yannick Moy <moy@adacore.com>
* adabkend.adb, ali-util.adb, errout.adb, exp_ch7.adb,
* exp_dbug.adb, freeze.adb, lib-xref.adb, restrict.adb,
* sem_attr.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb,
* sem_prag.adb, sem_res.adb, sem_util.adb Rename SPARK_Mode into
GNATprove_Mode.
* sem_ch13.adb: Remove blank.
* exp_spark.adb, exp_spark.ads (Expand_SPARK_Call): Only replace
subprograms by alias for renamings, not for inherited primitive
operations.
* exp_util.adb (Expand_Subtype_From_Expr): Apply the expansion
in GNATprove mode.
(Remove_Side_Effects): Apply the removal in
GNATprove mode, for the full analysis of expressions.
* expander.adb (Expand): Call the light SPARK expansion in GNATprove
mode.
(Expander_Mode_Restore, Expander_Mode_Save_And_Set): Ignore
save/restore actions for Expander_Active flag in GNATprove mode,
similar to what is done in ASIS mode.
* frontend.adb (Frontend): Generic bodies are instantiated in
GNATprove mode.
* gnat1drv.adb (Adjust_Global_Switches): Set operating
mode to Check_Semantics in GNATprove mode, although a light
expansion is still performed.
(Gnat1drv): Set Back_End_Mode to
Declarations_Only in GNATprove mode, and later on special case
the GNATprove mode to continue analysis anyway.
* lib-writ.adb (Write_ALI): Always generate ALI files in
GNATprove mode.
* opt.adb, opt.ads (Full_Expander_Active): Make it equivalent to
Expander_Active.
(SPARK_Mode): Renamed as GNATprove_Mode.
* sem_aggr.adb (Aggregate_Constraint_Checks): Add checks in the
tree in GNATprove_Mode.
* sem_ch12.adb (Analyze_Package_Instantiation): Always instantiate
body in GNATprove mode.
(Need_Subprogram_Instance_Body): Always instantiate body in GNATprove
mode.
* sem_ch3.adb (Constrain_Index, Process_Range_Expr_In_Decl):
Make sure side effects are removed in GNATprove mode.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206805 138bc75d-0d04-0410-961f-82ee72b054a4
Diffstat (limited to 'gcc/ada/lib-writ.adb')
| -rw-r--r-- | gcc/ada/lib-writ.adb | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index f794162e20b..015c628b87b 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -841,7 +841,7 @@ package body Lib.Writ is -- files, which are required to compute frame conditions -- of subprograms. - or else SPARK_Mode + or else GNATprove_Mode then Write_Info_Tab (25); @@ -973,9 +973,10 @@ package body Lib.Writ is -- If we are not generating code, and there is an up to date ALI file -- file accessible, read it, and acquire the compilation arguments from - -- this file. + -- this file. In GNATprove mode, always generate the ALI file, which + -- contains a special section for formal verification. - if Operating_Mode /= Generate_Code then + if Operating_Mode /= Generate_Code and then not GNATprove_Mode then if Up_To_Date_ALI_File_Exists then Update_Tables_From_ALI_File; return; @@ -1488,7 +1489,7 @@ package body Lib.Writ is -- Output SPARK cross-reference information if needed - if Opt.Xref_Active and then SPARK_Mode then + if Opt.Xref_Active and then GNATprove_Mode then SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table, Num_Sdep => Num_Sdep); SPARK_Specific.Output_SPARK_Xrefs; |