From 8fdafe44be001fa59172d7a28626d4babdc24b7b Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 27 Jan 2014 17:39:57 +0100 Subject: [multiple changes] 2014-01-27 Thomas Quinot * exp_ch7.adb: Minor reformatting. 2014-01-27 Robert Dewar * opt.adb (SPARK_Mode): Default for library units is None rather than Off. * opt.ads: Remove AUTO from SPARK_Mode_Type SPARK_Mode_Type is no longer ordered. * sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Remove AUTO possibility. * snames.ads-tmpl (Name_Auto): Removed, no longer used. 2014-01-27 Robert Dewar * par-ch5.adb (P_Sequence_Of_Statements): Make entry in Suspicious_Labels table if we have identifier; followed by loop or block. * par-endh.adb (Evaluate_End_Entry): Search Suspicious_Labels table. * par.adb (Suspicious_Labels): New table. 2014-01-27 Robert Dewar * exp_aggr.adb (Check_Bounds): Reason is range check, not length check. 2014-01-27 Yannick Moy * get_spark_xrefs.adb (Get_SPARK_Xrefs): Accept new type 'c' for reference. * lib-xref-spark_specific.adb (Is_Global_Constant): Remove useless function now. (Add_SPARK_Xrefs): Include references to constants. * spark_xrefs.ads Document new character 'c' for references to constants. 2014-01-27 Thomas Quinot * exp_smem.adb (Add_Write_After): For a function call, insert write as an after action in a transient scope. From-SVN: r207140 --- gcc/ada/spark_xrefs.ads | 2 ++ 1 file changed, 2 insertions(+) (limited to 'gcc/ada/spark_xrefs.ads') diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index e7df033..b17d799 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -177,6 +177,7 @@ package SPARK_Xrefs is -- m = modification -- r = reference + -- c = reference to constant object -- s = subprogram reference in a static call -- Special entries for reads and writes to memory reference a special @@ -229,6 +230,7 @@ package SPARK_Xrefs is Rtype : Character; -- Indicates type of reference, using code used in ALI file: -- r = reference + -- c = reference to constant object -- m = modification -- s = call -- cgit v1.1