function Sqrt (X : Float_Type'Base) return Float_Type'Base with
Post => Sqrt'Result >= 0.0
-
and then (if X = 0.0 then Sqrt'Result = 0.0)
-
and then (if X = 1.0 then Sqrt'Result = 1.0)
- -- If X is positive, the result of Sqrt is positive. This property is
- -- useful in particular for static analysis. The property that X is
- -- positive is not expressed as (X > 0), as the value X may be held in
- -- registers that have larger range and precision on some architecture
+ -- Finally if X is positive, the result of Sqrt is positive (because
+ -- the sqrt of numbers greater than 1 is greater than or equal to 1,
+ -- and the sqrt of numbers less than 1 is greater than the argument).
+
+ -- This property is useful in particular for static analysis. The
+ -- property that X is positive is not expressed as (X > 0), as
+ -- the value X may be held in registers that have larger range and
+ -- precision on some architecture (for example, on x86 using x387
+ -- FPU, as opposed to SSE2). So, it might be possible for X to be
+ -- 2.0**(-5000) or so, which could cause the number to compare as
+ -- greater than 0, but Sqrt would still return a zero result.
- -- (for example, on x86 using x387 FPU, as opposed to SSE2). So, it
- -- might be possible for X to be 2.0**(-5000) or so, which could cause
- -- the number to compare as greater than 0, but Sqrt would still return
- -- a zero result.
+ -- Note: we use the comparison with Succ (0.0) here because this is
+ -- more amenable to CodePeer analysis than the use of 'Machine.
and then (if X >= Float_Type'Succ (0.0) then Sqrt'Result > 0.0);
function "**" (Left, Right : Float_Type'Base) return Float_Type'Base with
Post => "**"'Result >= 0.0
- and then (if Right = 0.0 then "**"'Result = 1.0)
- and then (if Right = 1.0 then "**"'Result = Left)
- and then (if Left = 1.0 then "**"'Result = 1.0)
- and then (if Left = 0.0 then "**"'Result = 0.0);
+ and then (if Right = 0.0 then "**"'Result = 1.0)
+ and then (if Right = 1.0 then "**"'Result = Left)
+ and then (if Left = 1.0 then "**"'Result = 1.0)
+ and then (if Left = 0.0 then "**"'Result = 0.0);
function Sin (X : Float_Type'Base) return Float_Type'Base with
Post => Sin'Result in -1.0 .. 1.0
- and then (if X = 0.0 then Sin'Result = 0.0);
+ and then (if X = 0.0 then Sin'Result = 0.0);
function Sin (X, Cycle : Float_Type'Base) return Float_Type'Base with
Post => Sin'Result in -1.0 .. 1.0
- and then (if X = 0.0 then Sin'Result = 0.0);
+ and then (if X = 0.0 then Sin'Result = 0.0);
function Cos (X : Float_Type'Base) return Float_Type'Base with
Post => Cos'Result in -1.0 .. 1.0
- and then (if X = 0.0 then Cos'Result = 1.0);
+ and then (if X = 0.0 then Cos'Result = 1.0);
function Cos (X, Cycle : Float_Type'Base) return Float_Type'Base with
Post => Cos'Result in -1.0 .. 1.0
- and then (if X = 0.0 then Cos'Result = 1.0);
+ and then (if X = 0.0 then Cos'Result = 1.0);
function Tan (X : Float_Type'Base) return Float_Type'Base with
Post => (if X = 0.0 then Tan'Result = 0.0);
function Cosh (X : Float_Type'Base) return Float_Type'Base with
Post => Cosh'Result >= 1.0
- and then (if X = 0.0 then Cosh'Result = 1.0);
+ and then (if X = 0.0 then Cosh'Result = 1.0);
function Tanh (X : Float_Type'Base) return Float_Type'Base with
Post => Tanh'Result in -1.0 .. 1.0
- and then (if X = 0.0 then Tanh'Result = 0.0);
+ and then (if X = 0.0 then Tanh'Result = 0.0);
function Coth (X : Float_Type'Base) return Float_Type'Base with
Post => abs Coth'Result >= 1.0;
function Arccosh (X : Float_Type'Base) return Float_Type'Base with
Post => Arccosh'Result >= 0.0
- and then (if X = 1.0 then Arccosh'Result = 0.0);
+ and then (if X = 1.0 then Arccosh'Result = 0.0);
function Arctanh (X : Float_Type'Base) return Float_Type'Base with
Post => (if X = 0.0 then Arctanh'Result = 0.0);
-- Check if an imported or extended project if also a library project
procedure Check_Aggregate_Library_Dirs;
+ -- Check that the library directory and the library ALI directory of
+ -- an aggregate library project are not the same as the object directory
+ -- or the library directory of any of its aggregated projects.
----------------------------------
-- Check_Aggregate_Library_Dirs --
----------------------------------
procedure Check_Aggregate_Library_Dirs is
-
procedure Process_Aggregate (Proj : Project_Id);
+ -- Recursive procedure to check the aggregated projects, as they may
+ -- also be aggregated library projects.
-----------------------
-- Process_Aggregate --
-----------------------
procedure Process_Aggregate (Proj : Project_Id) is
-
- Agg : Aggregated_Project_List := Proj.Aggregated_Projects;
+ Agg : Aggregated_Project_List;
begin
+ Agg := Proj.Aggregated_Projects;
while Agg /= null loop
Error_Msg_Name_1 := Agg.Project.Name;
- if Agg.Project.Qualifier /= Aggregate_Library and then
- Project.Library_ALI_Dir.Name
- = Agg.Project.Object_Directory.Name
+ if Agg.Project.Qualifier /= Aggregate_Library
+ and then Project.Library_ALI_Dir.Name =
+ Agg.Project.Object_Directory.Name
then
Error_Msg
(Data.Flags,
& " object directory of aggregated project %%",
The_Lib_Kind.Location, Project);
- elsif Project.Library_ALI_Dir.Name
- = Agg.Project.Library_Dir.Name
+ elsif Project.Library_ALI_Dir.Name =
+ Agg.Project.Library_Dir.Name
then
Error_Msg
(Data.Flags,
& " library directory of aggregated project %%",
The_Lib_Kind.Location, Project);
- elsif Agg.Project.Qualifier /= Aggregate_Library and then
- Project.Library_Dir.Name
- = Agg.Project.Object_Directory.Name
+ elsif Agg.Project.Qualifier /= Aggregate_Library
+ and then Project.Library_Dir.Name =
+ Agg.Project.Object_Directory.Name
then
Error_Msg
(Data.Flags,
& " object directory of aggregated project %%",
The_Lib_Kind.Location, Project);
- elsif Project.Library_Dir.Name
- = Agg.Project.Library_Dir.Name
+ elsif Project.Library_Dir.Name =
+ Agg.Project.Library_Dir.Name
then
Error_Msg
(Data.Flags,
end loop;
end Process_Aggregate;
+ -- Start of processing for Check_Aggregate_Library_Dirs
+
begin
if Project.Qualifier = Aggregate_Library then
Process_Aggregate (Project);
projects / gcc.git / commitdiff