Commit 5a59d818 authored by jhugues's avatar jhugues
Browse files

* Added support for the floor and ceil operator in REAL



git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@5937 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent d62799a8
...@@ -2921,7 +2921,7 @@ package body Ocarina.Backends.REAL is ...@@ -2921,7 +2921,7 @@ package body Ocarina.Backends.REAL is
end; end;
when FC_Cos | FC_Sin | FC_Tan | FC_Cosh | FC_Sinh | FC_Tanh when FC_Cos | FC_Sin | FC_Tan | FC_Cosh | FC_Sinh | FC_Tanh
| FC_Ln | FC_Exp | FC_Sqrt => | FC_Ln | FC_Exp | FC_Sqrt | FC_Ceil | FC_Floor =>
declare declare
VT : Value_Type; VT : Value_Type;
R : Value_Id; R : Value_Id;
...@@ -2954,6 +2954,12 @@ package body Ocarina.Backends.REAL is ...@@ -2954,6 +2954,12 @@ package body Ocarina.Backends.REAL is
Result := New_Real_Value (Exp (VT.RVal)); Result := New_Real_Value (Exp (VT.RVal));
when FC_Sqrt => when FC_Sqrt =>
Result := New_Real_Value (Sqrt (VT.RVal)); Result := New_Real_Value (Sqrt (VT.RVal));
when FC_Floor =>
Result := New_Real_Value
(Long_Long_Float'Floor (VT.RVal));
when FC_Ceil =>
Result := New_Real_Value
(Long_Long_Float'Ceiling (VT.RVal));
when others => when others =>
raise Program_Error; raise Program_Error;
end case; end case;
......
...@@ -173,6 +173,9 @@ package body Ocarina.Analyzer.REAL is ...@@ -173,6 +173,9 @@ package body Ocarina.Analyzer.REAL is
T : Node_Id; T : Node_Id;
It : Natural := RNU.Node_List.First; It : Natural := RNU.Node_List.First;
begin begin
-- XXX The list of theorem to be checked should be computed
-- from the instance tree instead
if Main_Theorem = No_Name then if Main_Theorem = No_Name then
-- We walk through all annex clauses to build the list of -- We walk through all annex clauses to build the list of
-- theorems to be checked. -- theorems to be checked.
...@@ -1337,7 +1340,6 @@ package body Ocarina.Analyzer.REAL is ...@@ -1337,7 +1340,6 @@ package body Ocarina.Analyzer.REAL is
-- The first parameter must be a set -- The first parameter must be a set
case Kind (N) is case Kind (N) is
when K_Set_Reference => when K_Set_Reference =>
-- We register the predefined set -- We register the predefined set
...@@ -2497,7 +2499,7 @@ package body Ocarina.Analyzer.REAL is ...@@ -2497,7 +2499,7 @@ package body Ocarina.Analyzer.REAL is
end if; end if;
when FC_Cos | FC_Sin | FC_Tan | FC_Cosh | FC_Sinh | FC_Tanh when FC_Cos | FC_Sin | FC_Tan | FC_Cosh | FC_Sinh | FC_Tanh
| FC_Ln | FC_Exp | FC_Sqrt => | FC_Ln | FC_Exp | FC_Sqrt | FC_Floor | FC_Ceil =>
Set_Returned_Type (S, RT_Float); Set_Returned_Type (S, RT_Float);
declare declare
...@@ -2590,7 +2592,6 @@ package body Ocarina.Analyzer.REAL is ...@@ -2590,7 +2592,6 @@ package body Ocarina.Analyzer.REAL is
while Present (N) loop while Present (N) loop
case Kind (N) is case Kind (N) is
when K_Set_Reference => when K_Set_Reference =>
-- We register the predefined set -- We register the predefined set
......
...@@ -302,6 +302,10 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is ...@@ -302,6 +302,10 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
return FC_List; return FC_List;
when T_Integer => when T_Integer =>
return FC_Int; return FC_Int;
when T_Ceil =>
return FC_Ceil;
when T_Floor =>
return FC_Floor;
when T_Float => when T_Float =>
return FC_Float; return FC_Float;
when T_Sum => when T_Sum =>
...@@ -420,7 +424,7 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is ...@@ -420,7 +424,7 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
return RT_Unknown; return RT_Unknown;
when FC_Queue => when FC_Queue =>
return RT_Unknown; return RT_Unknown;
when FC_Cos | FC_Sin | FC_Tan => when FC_Cos | FC_Sin | FC_Tan | FC_Ceil | FC_Floor =>
return RT_Float; return RT_Float;
when others => when others =>
DE ("Unable to determine REAL function returning type"); DE ("Unable to determine REAL function returning type");
......
...@@ -132,6 +132,8 @@ package Ocarina.ME_REAL.REAL_Tree.Utils is ...@@ -132,6 +132,8 @@ package Ocarina.ME_REAL.REAL_Tree.Utils is
FC_Ln : constant := 48; FC_Ln : constant := 48;
FC_Exp : constant := 49; FC_Exp : constant := 49;
FC_Sqrt : constant := 50; FC_Sqrt : constant := 50;
FC_Ceil : constant := 51;
FC_Floor : constant := 52;
FC_MMax : constant := 60; FC_MMax : constant := 60;
FC_MMin : constant := 61; FC_MMin : constant := 61;
......
...@@ -165,6 +165,8 @@ package body Ocarina.ME_REAL.Tokens is ...@@ -165,6 +165,8 @@ package body Ocarina.ME_REAL.Tokens is
New_Token (T_List, "List"); New_Token (T_List, "List");
New_Token (T_Float, "Float"); New_Token (T_Float, "Float");
New_Token (T_Max, "Max"); New_Token (T_Max, "Max");
New_Token (T_Ceil, "ceil");
New_Token (T_Floor, "floor");
New_Token (T_Cos, "cos"); New_Token (T_Cos, "cos");
New_Token (T_Sin, "sin"); New_Token (T_Sin, "sin");
New_Token (T_Tan, "tan"); New_Token (T_Tan, "tan");
......
...@@ -136,6 +136,8 @@ package Ocarina.ME_REAL.Tokens is ...@@ -136,6 +136,8 @@ package Ocarina.ME_REAL.Tokens is
T_Head, -- Return the first node of a list T_Head, -- Return the first node of a list
T_Queue, -- Return the list minus the first node T_Queue, -- Return the list minus the first node
T_Integer, T_Integer,
T_Ceil,
T_Floor,
T_Max, T_Max,
T_Min, T_Min,
T_Cos, T_Cos,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment