In ALFA mode, compiler is working in a special way in which it should believe it generates actual object code, while it is not; warnings should not be issued; checks should not be inserted in the code; various pragmas should be ignored. Changing the startup of frontend to do that.
Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-05 Yannick Moy <m...@adacore.com> * debug.adb: Remove use of -gnatd.D. * gnat1drv.adb (Adjust_Global_Switches): adjust switches for ALFA mode * opt.ads: Simplify variables for ALFA mode, to keep one only * restrict.adb, sem_prag.adb: Adapt treatment done for CodePeer mode to ALFA mode.
Index: debug.adb =================================================================== --- debug.adb (revision 177351) +++ debug.adb (working copy) @@ -122,8 +122,8 @@ -- d.B -- d.C Generate concatenation call, do not generate inline code -- d.D - -- d.E SPARK generation mode - -- d.F Why generation mode + -- d.E + -- d.F ALFA mode -- d.G -- d.H -- d.I SCIL generation mode @@ -580,12 +580,10 @@ -- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases -- where we would normally generate inline concatenation code. - -- d.E SPARK generation mode. Generate intermediate code for the sake of - -- formal verification through SPARK and the SPARK toolset. + -- d.F ALFA mode. Generate AST in a form suitable for formal verification, + -- as well as additional cross reference information in ALI files to + -- compute effects of subprograms. - -- d.F Why generation mode. Generate intermediate code for the sake of - -- formal verification through Why and the Why VC generator. - -- d.I Generate SCIL mode. Generate intermediate code for the sake of -- of static analysis tools, and ensure additional tree consistency -- between different compilations of specs. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 177395) +++ sem_prag.adb (working copy) @@ -5059,9 +5059,9 @@ -- Start of processing for Process_Restrictions_Or_Restriction_Warnings begin - -- Ignore all Restrictions pragma in CodePeer mode + -- Ignore all Restrictions pragma in CodePeer and ALFA modes - if CodePeer_Mode then + if CodePeer_Mode or else ALFA_Mode then return; end if; @@ -5283,10 +5283,13 @@ -- Start of processing for Process_Suppress_Unsuppress begin - -- Ignore pragma Suppress/Unsuppress in codepeer mode on user code: - -- we want to generate checks for analysis purposes, as set by -gnatC + -- Ignore pragma Suppress/Unsuppress in CodePeer and ALFA modes on + -- user code: we want to generate checks for analysis purposes, as + -- set respectively by -gnatC and -gnatd.F - if CodePeer_Mode and then Comes_From_Source (N) then + if (CodePeer_Mode or else ALFA_Mode) + and then Comes_From_Source (N) + then return; end if; @@ -9444,11 +9447,12 @@ Check_Valid_Configuration_Pragma; Check_Restriction (No_Initialize_Scalars, N); - -- Initialize_Scalars creates false positives in CodePeer, - -- so ignore this pragma in this mode. + -- Initialize_Scalars creates false positives in CodePeer, and + -- incorrect negative results in ALFA mode, so ignore this pragma + -- in these modes. if not Restriction_Active (No_Initialize_Scalars) - and then not CodePeer_Mode + and then not (CodePeer_Mode or else ALFA_Mode) then Init_Or_Norm_Scalars := True; Initialize_Scalars := True; @@ -9475,10 +9479,10 @@ when Pragma_Inline_Always => GNAT_Pragma; - -- Pragma always active unless in CodePeer mode, since this causes - -- walk order issues. + -- Pragma always active unless in CodePeer or ALFA mode, since + -- this causes walk order issues. - if not CodePeer_Mode then + if not (CodePeer_Mode or else ALFA_Mode) then Process_Inline (True); end if; @@ -10917,10 +10921,11 @@ Check_Arg_Count (0); Check_Valid_Configuration_Pragma; - -- Normalize_Scalars creates false positives in CodePeer, so - -- ignore this pragma in this mode. + -- Normalize_Scalars creates false positives in CodePeer, and + -- incorrect negative results in ALFA mode, so ignore this pragma + -- in these modes. - if not CodePeer_Mode then + if not (CodePeer_Mode or else ALFA_Mode) then Normalize_Scalars := True; Init_Or_Norm_Scalars := True; end if; @@ -11287,9 +11292,9 @@ -- In the context of static code analysis, we do not need -- complex front-end expansions related to pragma Pack, - -- so disable handling of pragma Pack in this case. + -- so disable handling of pragma Pack in these cases. - if CodePeer_Mode then + if CodePeer_Mode or else ALFA_Mode then null; -- Don't attempt any packing for VM targets. We possibly Index: gnat1drv.adb =================================================================== --- gnat1drv.adb (revision 177334) +++ gnat1drv.adb (working copy) @@ -390,17 +390,86 @@ Back_End_Handles_Limited_Types := False; end if; - -- Set switches for formal verification modes + -- Set switches for formal verification mode - if Debug_Flag_Dot_EE then - ALFA_Through_SPARK_Mode := True; - end if; + if Debug_Flag_Dot_FF then - if Debug_Flag_Dot_FF then - ALFA_Through_Why_Mode := True; + ALFA_Mode := True; + + -- Turn off inlining, which would confuse formal verification output + -- and gain nothing. + + Front_End_Inlining := False; + Inline_Active := False; + + -- Disable front-end optimizations, to keep the tree as close to the + -- source code as possible, and also to avoid inconsistencies between + -- trees when using different optimization switches. + + Optimization_Level := 0; + + -- Enable some restrictions systematically to simplify the generated + -- code (and ease analysis). Note that restriction checks are also + -- disabled in ALFA mode, see Restrict.Check_Restriction, and user + -- specified Restrictions pragmas are ignored, see + -- Sem_Prag.Process_Restrictions_Or_Restriction_Warnings. + + Restrict.Restrictions.Set (No_Initialize_Scalars) := True; + + -- Suppress all language checks since they are handled implicitly by + -- the formal verification backend. + -- Turn off dynamic elaboration checks. + -- Turn off alignment checks. + -- Turn off validity checking. + + Suppress_Options := (others => True); + Enable_Overflow_Checks := False; + Dynamic_Elaboration_Checks := False; + Reset_Validity_Check_Options; + + -- Kill debug of generated code, since it messes up sloc values + + Debug_Generated_Code := False; + + -- Turn cross-referencing on in case it was disabled (e.g. by -gnatD) + + Xref_Active := True; + + -- Polling mode forced off, since it generates confusing junk + + Polling_Required := False; + + -- Set operating mode to Generate_Code to benefit from full front-end + -- expansion (e.g. default arguments). + + Operating_Mode := Generate_Code; + + -- Skip call to gigi + + Debug_Flag_HH := True; + + -- Enable assertions and debug pragmas, since they give valuable + -- extra information for formal verification. + + Assertions_Enabled := True; + Debug_Pragmas_Enabled := True; + + -- Turn off style check options since we are not interested in any + -- front-end warnings when we are getting ALFA output. + + Reset_Style_Check_Options; + + -- Suppress compiler warnings, since what we are + -- interested in here is what formal verification can find out. + + Warning_Mode := Suppress; + + -- Always perform semantics and generate ALI files in ALFA mode, + -- so that a gnatmake -c -k will proceed further when possible. + + Force_ALI_Tree_File := True; + Try_Semantics := True; end if; - - ALFA_Mode := ALFA_Through_SPARK_Mode or ALFA_Through_Why_Mode; end Adjust_Global_Switches; -------------------- Index: restrict.adb =================================================================== --- restrict.adb (revision 177274) +++ restrict.adb (working copy) @@ -375,11 +375,12 @@ begin Msg_Issued := False; - -- In CodePeer mode, we do not want to check for any restriction, or set - -- additional restrictions other than those already set in gnat1drv.adb - -- so that we have consistency between each compilation. + -- In CodePeer and ALFA mode, we do not want to check for any + -- restriction, or set additional restrictions other than those already + -- set in gnat1drv.adb so that we have consistency between each + -- compilation. - if CodePeer_Mode then + if CodePeer_Mode or else ALFA_Mode then return; end if; Index: opt.ads =================================================================== --- opt.ads (revision 177395) +++ opt.ads (working copy) @@ -1855,25 +1855,17 @@ -- Used to store the ASIS version number read from a tree file to check if -- it is the same as stored in the ASIS version number in Tree_IO. - ----------------------------------- - -- Modes for Formal Verification -- - ----------------------------------- + ---------------------------------- + -- Mode for Formal Verification -- + ---------------------------------- - -- These modes are currently defined through debug flags + -- This mode is currently defined through a debug flag ALFA_Mode : Boolean := False; - -- Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode + -- Specific compiling mode targeting formal verification through the + -- generation of Why code for those parts of the input code that belong to + -- the ALFA subset of Ada. Set by debuf flag -gnatd.F. - ALFA_Through_SPARK_Mode : Boolean := False; - -- Specific compiling mode targeting formal verification through - -- the generation of SPARK code for those parts of the input code that - -- belong to the ALFA subset of Ada. Set by debug flag -gnatd.E. - - ALFA_Through_Why_Mode : Boolean := False; - -- Specific compiling mode targeting formal verification through - -- the generation of Why code for those parts of the input code that - -- belong to the ALFA subset of Ada. Set by debuf flag -gnatd.F. - private -- The following type is used to save and restore settings of switches in