From 67c861780f945ca79a8d6d5bf7cb8d3c22fc7f74 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 2 Sep 2011 11:22:16 +0200 Subject: [multiple changes] 2011-09-02 Robert Dewar * prj-dect.adb, prj-env.adb, prj-nmsc.adb, prj-proc.adb, prj-tree.adb, prj.adb, prj.ads, sem_ch5.adb: Minor reformatting. 2011-09-02 Thomas Quinot * sem_attr.adb (Analyze_Attribute, case Unrestriced_Access): Guard against a prefix that is an N_Has_Entity but has no associated entity. 2011-09-02 Yannick Moy * lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa references. 2011-09-02 Yannick Moy * opt.ads (Warn_On_Suspicious_Contract): New warning flag. * sem_ch3.adb (Analyze_Declarations): Call checker for suspicious contracts. * sem_ch6.adb, sem_ch6.ads (Check_Subprogram_Contract): New procedure looking for suspicious postconditions. * usage.adb (Usage): New options -gnatw.t and -gnatw.T. * warnsw.adb (Set_Dot_Warning_Switch): Take into account new options -gnatw.t and -gnatw.T. From-SVN: r178448 --- gcc/ada/lib-xref-alfa.adb | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) (limited to 'gcc/ada/lib-xref-alfa.adb') diff --git a/gcc/ada/lib-xref-alfa.adb b/gcc/ada/lib-xref-alfa.adb index 74d1421..ce95463 100644 --- a/gcc/ada/lib-xref-alfa.adb +++ b/gcc/ada/lib-xref-alfa.adb @@ -608,11 +608,20 @@ package body Alfa is -- On non-callable entities, the only references of interest are -- reads and writes. - if Ekind (E) in Overloadable_Kind then - return Typ = 's'; - else - return Typ = 'r' or else Typ = 'm'; - end if; + case Ekind (E) is + when Overloadable_Kind => + return Typ = 's'; + + -- References to IN parameters are not considered in Alfa + -- section, as these will be translated as constants in the + -- intermediate language for formal verification. + + when E_In_Parameter => + return False; + + when others => + return Typ = 'r' or else Typ = 'm'; + end case; end Is_Alfa_Reference; ------------------- -- cgit v1.1