-- PSL - Simple subset -- Copyright (C) 2002-2016 Tristan Gingold -- -- This program is free software: you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation, either version 2 of the License, or -- (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program. If not, see . with Types; use Types; with PSL.Types; use PSL.Types; with PSL.Errors; use PSL.Errors; package body PSL.Subsets is procedure Check_Simple (N : Node) is begin case Get_Kind (N) is when N_Not_Bool => if Get_Psl_Type (Get_Boolean (N)) /= Type_Boolean then Error_Msg_Sem ("operand of a negation operator must be a boolean", N); end if; when N_Never => case Get_Psl_Type (Get_Property (N)) is when Type_Sequence | Type_Boolean => null; when others => Error_Msg_Sem ("operand of a 'never' operator must be " & "a boolean or a sequence", N); end case; when N_Eventually => case Get_Psl_Type (Get_Property (N)) is when Type_Sequence | Type_Boolean => null; when others => Error_Msg_Sem ("operand of an 'eventually!' operator must be" & " a boolean or a sequence", N); end case; when N_And_Bool => if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then Error_Msg_Sem ("left-hand side operand of logical 'and' must be" & " a boolean", N); end if; when N_Or_Bool => if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then Error_Msg_Sem ("left-hand side operand of logical 'or' must be" & " a boolean", N); end if; when N_Log_Imp_Prop => if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then Error_Msg_Sem ("left-hand side operand of logical '->' must be" & " a boolean", N); end if; -- FIXME: <-> when N_Until => if not Get_Inclusive_Flag (N) then if Get_Psl_Type (Get_Right (N)) /= Type_Boolean then Error_Msg_Sem ("right-hand side of a non-overlapping " & "'until*' operator must be a boolean", N); end if; else if Get_Psl_Type (Get_Right (N)) /= Type_Boolean or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean then Error_Msg_Sem ("both operands of an overlapping 'until*'" & " operator are boolean", N); end if; end if; when N_Before => if Get_Psl_Type (Get_Right (N)) /= Type_Boolean or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean then Error_Msg_Sem ("both operands of a 'before*'" & " operator are boolean", N); end if; when others => null; end case; -- Recursion. case Get_Kind (N) is when N_Error => null; when N_Hdl_Mod_Name => null; when N_Vunit | N_Vmode | N_Vprop => declare Item : Node; begin Item := Get_Item_Chain (N); while Item

--  Although being part of GRT, the readline binding should be independent of
--  it (for easier reuse).

with System; use System;

package Grt.Readline is
   subtype Fat_String is String (Positive);
   type Char_Ptr is access Fat_String;
   pragma Convention (C, Char_Ptr);
   --  A C string (which is NUL terminated) is represented as a (thin) access
   --  to a fat string (a string whose range is 1 .. integer'Last).
   --  The use of an access to a constrained array allows a representation
   --  compatible with C.  Indexing of object of that type is safe only for
   --  indexes until the NUL character.

   function Readline (Prompt : Char_Ptr) return Char_Ptr;
   function Readline (Prompt : Address) return Char_Ptr;
   pragma Import (C, Readline);

   procedure Free (Buf : Char_Ptr);
   pragma Import (C, Free);

   procedure Add_History (Line : Char_Ptr);
   pragma Import (C, Add_History);

   function Strlen (Str : Char_Ptr) return Natural;
   pragma Import (C, Strlen);

   pragma Linker_Options ("-lreadline");
end Grt.Readline;