Index: gnat1drv.adb =================================================================== --- gnat1drv.adb (revision 194190) +++ gnat1drv.adb (working copy) @@ -201,7 +201,9 @@ Dynamic_Elaboration_Checks := False; - -- Set STRICT mode for overflow checks if not set explicitly + -- Set STRICT mode for overflow checks if not set explicitly. This + -- prevents suppressing of overflow checks by default, in code down + -- below. if Suppress_Options.Overflow_Checks_General = Not_Set then Suppress_Options.Overflow_Checks_General := Strict; @@ -268,6 +270,129 @@ Try_Semantics := True; end if; + -- Set switches for formal verification mode + + if Debug_Flag_Dot_VV then + Formal_Extensions := True; + end if; + + if Debug_Flag_Dot_FF then + Alfa_Mode := True; + + -- Set strict standard interpretation of compiler permissions + + if Debug_Flag_Dot_DD then + Strict_Alfa_Mode := True; + end if; + + -- 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; + + -- Note: at this point we used to suppress various checks, but that + -- is not what we want. We need the semantic processing for these + -- checks (which will set flags like Do_Overflow_Check, showing the + -- points at which potential checks are required semantically). We + -- don't want the expansion associated with these checks, but that + -- happens anyway because this expansion is simply not done in the + -- Alfa version of the expander. + + -- Turn off dynamic elaboration checks: generates inconsistencies in + -- trees between specs compiled as part of a main unit or as part of + -- a with-clause. + + Dynamic_Elaboration_Checks := False; + + -- Set STRICT mode for overflow checks if not set explicitly. This + -- prevents suppressing of overflow checks by default, in code down + -- below. + + if Suppress_Options.Overflow_Checks_General = Not_Set then + Suppress_Options.Overflow_Checks_General := Strict; + Suppress_Options.Overflow_Checks_Assertions := Strict; + end if; + + -- 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) + -- as it is needed for computing effects of subprograms in the formal + -- verification backend. + + Xref_Active := True; + + -- Polling mode forced off, since it generates confusing junk + + Polling_Required := False; + + -- Set operating mode to Generate_Code, but full front-end expansion + -- is not desirable in Alfa mode, so a light expansion is performed + -- instead. + + Operating_Mode := Generate_Code; + + -- Skip call to gigi + + Debug_Flag_HH := True; + + -- Disable Expressions_With_Actions nodes + + -- The gnat2why backend does not deal with Expressions_With_Actions + -- in all places (in particular assertions). It is difficult to + -- determine in the frontend which cases are allowed, so we disable + -- Expressions_With_Actions entirely. Even in the cases where + -- gnat2why deals with Expressions_With_Actions, it is easier to + -- deal with the original constructs (quantified, conditional and + -- case expressions) instead of the rewritten ones. + + Use_Expression_With_Actions := False; + + -- 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; + + -- Suppress the generation of name tables for enumerations, which are + -- not needed for formal verification, and fall outside the Alfa + -- subset (use of pointers). + + Global_Discard_Names := True; + + -- Suppress the expansion of tagged types and dispatching calls, + -- which lead to the generation of non-Alfa code (use of pointers), + -- which is more complex to formally verify than the original source. + + Tagged_Type_Expansion := False; + end if; + -- Set Configurable_Run_Time mode if system.ads flag set if Targparm.Configurable_Run_Time_On_Target or Debug_Flag_YY then @@ -335,8 +460,8 @@ -- Set proper status for overflow check mechanism - -- If already set (by -gnato or above in CodePeer mode) then we have - -- nothing to do. + -- If already set (by -gnato or above in Alfa or CodePeer mode) then we + -- have nothing to do. if Opt.Suppress_Options.Overflow_Checks_General /= Not_Set then null; @@ -430,114 +555,6 @@ Back_End_Handles_Limited_Types := False; end if; - -- Set switches for formal verification mode - - if Debug_Flag_Dot_VV then - Formal_Extensions := True; - end if; - - if Debug_Flag_Dot_FF then - Alfa_Mode := True; - - -- Set strict standard interpretation of compiler permissions - - if Debug_Flag_Dot_DD then - Strict_Alfa_Mode := True; - end if; - - -- 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; - - -- Note: at this point we used to suppress various checks, but that - -- is not what we want. We need the semantic processing for these - -- checks (which will set flags like Do_Overflow_Check, showing the - -- points at which potential checks are required semantically). We - -- don't want the expansion associated with these checks, but that - -- happens anyway because this expansion is simply not done in the - -- Alfa version of the expander. - - -- 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) - -- as it is needed for computing effects of subprograms in the formal - -- verification backend. - - Xref_Active := True; - - -- Polling mode forced off, since it generates confusing junk - - Polling_Required := False; - - -- Set operating mode to Generate_Code, but full front-end expansion - -- is not desirable in Alfa mode, so a light expansion is performed - -- instead. - - Operating_Mode := Generate_Code; - - -- Skip call to gigi - - Debug_Flag_HH := True; - - -- Disable Expressions_With_Actions nodes - - -- The gnat2why backend does not deal with Expressions_With_Actions - -- in all places (in particular assertions). It is difficult to - -- determine in the frontend which cases are allowed, so we disable - -- Expressions_With_Actions entirely. Even in the cases where - -- gnat2why deals with Expressions_With_Actions, it is easier to - -- deal with the original constructs (quantified, conditional and - -- case expressions) instead of the rewritten ones. - - Use_Expression_With_Actions := False; - - -- 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; - - -- Suppress the generation of name tables for enumerations, which are - -- not needed for formal verification, and fall outside the Alfa - -- subset (use of pointers). - - Global_Discard_Names := True; - - -- Suppress the expansion of tagged types and dispatching calls, - -- which lead to the generation of non-Alfa code (use of pointers), - -- which is more complex to formally verify than the original source. - - Tagged_Type_Expansion := False; - end if; - -- If the inlining level has not been set by the user, compute it from -- the optimization level: 1 at -O1/-O2 (and -Os), 2 at -O3 and above.