From fd22e260b5d48a245411c09858fa42b1614a89c7 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 18 Apr 2016 12:02:58 +0200 Subject: [multiple changes] 2016-04-18 Yannick Moy * sem_res.adb (Resolve_Call): Prevent inlining of calls inside expression functions. Factor previous code issuing errors to call Cannot_Inline instead, which does appropriate processing of message for GNATprove. 2016-04-18 Arnaud Charlet * einfo.ads, sem_ch3.adb, sem_ch8.adb, osint-l.adb, rtsfind.adb, osint-b.adb: Cleanups. 2016-04-18 Yannick Moy * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Only create body to inline in GNATprove mode when SPARK_Mode On applies to subprogram body. * sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_Type): Make function public. 2016-04-18 Eric Botcazou * layout.adb: Fix minor typo in comment. * inline.adb: Fix minor pasto. * sem_ch12.ads: Fix minor typos in comments. From-SVN: r235111 --- gcc/ada/sem_prag.ads | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'gcc/ada/sem_prag.ads') diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index ce05bfd..3bc2f65 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -383,6 +383,11 @@ package Sem_Prag is function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type; -- Given a pragma SPARK_Mode node, return corresponding mode id + function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type; + -- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram + -- Get_SPARK_Mode_From_Pragma. Convert a name into a corresponding value + -- of type SPARK_Mode_Type. + procedure Initialize; -- Initializes data structures used for pragma processing. Must be called -- before analyzing each new main source program. -- cgit v1.1