diff --git a/gnat2goto/driver/driver.adb b/gnat2goto/driver/driver.adb index 8b790ea1a..61cffb5eb 100644 --- a/gnat2goto/driver/driver.adb +++ b/gnat2goto/driver/driver.adb @@ -257,6 +257,20 @@ package body Driver is end; if not Add_Start then + -- If the compilation unit is not a subprogram body then there is + -- no function/procedure to call + -- CBMC does not like that so we add cprover_start with empty body + Start_Symbol.Name := Start_Name; + Start_Symbol.PrettyName := Start_Name; + Start_Symbol.BaseName := Start_Name; + + Set_Return_Type (Start_Type, Void_Type); + + Start_Symbol.SymType := Start_Type; + Start_Symbol.Value := Start_Body; + Start_Symbol.Mode := Intern ("C"); + + Global_Symbol_Table.Insert (Start_Name, Start_Symbol); Put_Line (Sym_Tab_File, Create (SymbolTable2Json (Global_Symbol_Table)).Write); else diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index d94082397..ff02499e5 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/gnat2goto/driver/tree_walk.adb @@ -1,6 +1,9 @@ +with Uname; use Uname; + with Einfo; use Einfo; with Namet; use Namet; with Nlists; use Nlists; +with Sem; with Sem_Util; use Sem_Util; with Sem_Aux; use Sem_Aux; with Snames; use Snames; @@ -207,6 +210,12 @@ package body Tree_Walk is function Do_Op_Not (N : Node_Id) return Irep with Pre => Nkind (N) in N_Op; + procedure Do_Package_Declaration (N : Node_Id) + with Pre => Nkind (N) = N_Package_Declaration; + + procedure Do_Package_Specification (N : Node_Id) + with Pre => Nkind (N) = N_Package_Specification; + function Do_Procedure_Call_Statement (N : Node_Id) return Irep with Pre => Nkind (N) = N_Procedure_Call_Statement, Post => Kind (Do_Procedure_Call_Statement'Result) = @@ -279,6 +288,16 @@ package body Tree_Walk is Post => Kind (Do_Unconstrained_Array_Definition'Result) = I_Struct_Type; + procedure Do_Withed_Unit_Spec (N : Node_Id); + -- Enters the specification of the withed unit, N, into the symbol table + + procedure Do_Withed_Units_Specs is new Sem.Walk_Library_Items + (Action => Do_Withed_Unit_Spec); + -- Traverses tree applying the procedure Do_With_Unit_Spec to all nodes + -- which are specifications of library units withed by the GNAT_Root unit + -- (that is, the body being compiled). + -- It starts with the unit Standard and finishes with GNAT_Root + function Find_Record_Variant (Variant_Part : Node_Id; Actual_Disc : Node_Id) return Node_Id with Pre => Nkind (Variant_Part) = N_Variant_Part, @@ -355,13 +374,41 @@ package body Tree_Walk is Old_Type : Entity_Id; New_Type : Entity_Id) return Irep; + type Construct is (Declaration, Statement); + + procedure Warn_Unhandled_Construct (C : Construct; Mess : String); + + procedure Process_Declaration (N : Node_Id; Block : Irep); +-- with Pre => Nkind (N) in N_Declaration or else +-- Nkind (N) in N_Number_Declaration or else +-- Nkind (N) in N_Later_Decl_Item or else +-- Nkind (N) in N_Pragma or else +-- Nkind (N) in N_Exception_Declaration or else +-- Nkind (N) in N_Freeze_Entity; +-- Precondition commented out because full extend of declrations not yet known + -- Handles both a basic declaration and a declarative item. + + procedure Process_Declarations (L : List_Id; Block : Irep); + -- Processes the declarations and is used for both a package specification + -- where only basic declarations are allowed (no subprogram bodies etc.) + -- and declarative parts where subprogram bodies etc. may be declared. + -- The Gnat front end will check that only allowed declarations are used + -- where only basic declarations permitted. + -- Process_Declarations is a procedure rather than a function like its + -- sister Process_Statements because the Irep (an I_Code_Block) has to be + -- extended in package_specifications when it has private declarations. + procedure Process_Statement (N : Node_Id; Block : Irep) with Pre => Kind (Block) = I_Code_Block; - -- Process statement or declaration + -- Process statement function Process_Statements (L : List_Id) return Irep with Post => Kind (Process_Statements'Result) = I_Code_Block; - -- Process list of statements or declarations + -- Process list of statements + + procedure Register_Subprogram_Specification (N : Node_Id) + with Pre => Nkind (N) in N_Subprogram_Specification; + -- Insert the subprogram specification into the symbol table procedure Remove_Entity_Substitution (E : Entity_Id); @@ -1243,24 +1290,26 @@ package body Tree_Walk is U : constant Node_Id := Unit (N); Unit_Symbol : Symbol; begin + -- Insert all all specifications of all withed units including the + -- specification of the given compilation unit into the symbol table. + Do_Withed_Units_Specs; + case Nkind (U) is when N_Subprogram_Body => declare - Unit_Type : constant Irep := - Do_Subprogram_Specification (Specification (U)); Unit_Name : constant Symbol_Id := Intern (Unique_Name (Unique_Defining_Entity (U))); begin - -- Register the symbol *before* we compile the body, for - -- recursive calls. - Unit_Symbol.Name := Unit_Name; - Unit_Symbol.PrettyName := Unit_Name; - Unit_Symbol.BaseName := Unit_Name; - Unit_Symbol.Mode := Intern ("C"); - Unit_Symbol.SymType := Unit_Type; - Global_Symbol_Table.Insert (Unit_Name, Unit_Symbol); - - Unit_Symbol.Value := Do_Subprogram_Or_Block (U); + -- The specification of the subprogram body has already + -- been inserted into the symbol table by the call to + -- Do_Withed_Unit_Specs. + pragma Assert (Global_Symbol_Table.Contains (Unit_Name)); + Unit_Symbol := Global_Symbol_Table (Unit_Name); + + -- Now compile the body of the subprogram + Unit_Symbol.Value := Do_Subprogram_Or_Block (U); + + -- and update the symbol table entry for this subprogram. Global_Symbol_Table.Replace (Unit_Name, Unit_Symbol); Add_Start := True; end; @@ -1547,11 +1596,6 @@ package body Tree_Walk is end Create_Dummy_Irep; function Do_Expression (N : Node_Id) return Irep is - procedure Warn_Unhandled_Expression (M : String); - procedure Warn_Unhandled_Expression (M : String) is - begin - Put_Line (Standard_Error, "Warning: " & M & "expressions unhandled"); - end Warn_Unhandled_Expression; begin Declare_Itype (Etype (N)); case Nkind (N) is @@ -1567,14 +1611,14 @@ package body Tree_Walk is when Attribute_Access => return Do_Address_Of (N); when Attribute_Length => return Do_Array_Length (N); when Attribute_Range => - Warn_Unhandled_Expression ("Range attribute"); - return Create_Dummy_Irep; + return Report_Unhandled_Node_Irep (N, "Do_Expression", + "Range attribute"); when Attribute_First => - Warn_Unhandled_Expression ("First attribute"); - return Create_Dummy_Irep; + return Report_Unhandled_Node_Irep (N, "Do_Expression", + "First attribute"); when Attribute_Last => - Warn_Unhandled_Expression ("Last attribute"); - return Create_Dummy_Irep; + return Report_Unhandled_Node_Irep (N, "Do_Expression", + "Last attribute"); when others => return Report_Unhandled_Node_Irep (N, "Do_Expression", "Unknown attribute"); @@ -1585,20 +1629,20 @@ package body Tree_Walk is when N_Indexed_Component => return Do_Indexed_Component (N); when N_Slice => return Do_Slice (N); when N_In => - Warn_Unhandled_Expression ("In"); - return Create_Dummy_Irep; + return Report_Unhandled_Node_Irep (N, "Do_Expression", + "In"); when N_Real_Literal => return Do_Real_Constant (N); when N_If_Expression => return Do_If_Expression (N); when N_And_Then => return Do_And_Then (N); when N_Or_Else => - Warn_Unhandled_Expression ("Or else"); - return Create_Dummy_Irep; + return Report_Unhandled_Node_Irep (N, "Do_Expression", + "Or else"); when N_Qualified_Expression => - Warn_Unhandled_Expression ("Qualified"); - return Create_Dummy_Irep; + return Report_Unhandled_Node_Irep (N, "Do_Expression", + "Qualified"); when N_Quantified_Expression => - Warn_Unhandled_Expression ("Quantified"); - return Create_Dummy_Irep; + return Report_Unhandled_Node_Irep (N, "Do_Expression", + "Quantified"); when others => return Report_Unhandled_Node_Irep (N, "Do_Expression", "Unknown expression kind"); @@ -3500,6 +3544,31 @@ package body Tree_Walk is return Ret; end Do_Operator_Simple; + ---------------------------- + -- Do_Package_Declaration -- + ---------------------------- + + procedure Do_Package_Declaration (N : Node_Id) is + begin + Do_Package_Specification (Specification (N)); + end Do_Package_Declaration; + + ---------------------------- + -- Do_Package_Specification -- + ---------------------------- + + procedure Do_Package_Specification (N : Node_Id) is + Package_Decs : constant Irep := New_Irep (I_Code_Block); + begin + Set_Source_Location (Package_Decs, Sloc (N)); + if Present (Visible_Declarations (N)) then + Process_Declarations (Visible_Declarations (N), Package_Decs); + end if; + if Present (Private_Declarations (N)) then + Process_Declarations (Private_Declarations (N), Package_Decs); + end if; + end Do_Package_Specification; + --------------------------------- -- Do_Procedure_Call_Statement -- --------------------------------- @@ -3946,27 +4015,22 @@ package body Tree_Walk is Proc_Symbol : Symbol; begin if not Global_Symbol_Table.Contains (Proc_Name) then - Put_Line (Standard_Error, "Warning: Subprogram " & - Unintern (Proc_Name) & " not in symbol table"); - declare - Proc_Type : constant Irep := - Do_Subprogram_Specification (Specification (N)); - New_Proc_Symbol : Symbol; - begin - New_Proc_Symbol.Name := Proc_Name; - New_Proc_Symbol.BaseName := Proc_Name; - New_Proc_Symbol.PrettyName := Proc_Name; - New_Proc_Symbol.SymType := Proc_Type; - New_Proc_Symbol.Mode := Intern ("C"); - - Global_Symbol_Table.Insert (Proc_Name, New_Proc_Symbol); - end; + -- A subprogram body does not have to have a separate declaration + -- so it may not be in the symbol table. + -- The subprogram specification of the subprogram body is used to + -- populate the symbol table instead. + Register_Subprogram_Specification (Specification (N)); end if; + -- Todo aspect_specification, i.e. pre/post-conditions + -- Now the subprogram should registered in the symbol table + -- whether a separate declaration was provided or not. if not Global_Symbol_Table.Contains (Proc_Name) then Report_Unhandled_Node_Empty (N, "Do_Subprogram_Body", "Proc name not in symbol table"); end if; Proc_Symbol := Global_Symbol_Table (Proc_Name); + + -- Compile the subprogram body and update its entry in the symbol table. Proc_Symbol.Value := Proc_Body; Global_Symbol_Table.Replace (Proc_Name, Proc_Symbol); end Do_Subprogram_Body; @@ -3976,23 +4040,9 @@ package body Tree_Walk is ------------------------------- procedure Do_Subprogram_Declaration (N : Node_Id) is - Proc_Type : constant Irep := - Do_Subprogram_Specification (Specification (N)); - - Proc_Name : constant Symbol_Id := Intern - (Unique_Name (Defining_Unit_Name (Specification (N)))); - -- take from spec, because body could be absent (null procedure) - - Proc_Symbol : Symbol; - begin - Proc_Symbol.Name := Proc_Name; - Proc_Symbol.BaseName := Proc_Name; - Proc_Symbol.PrettyName := Proc_Name; - Proc_Symbol.SymType := Proc_Type; - Proc_Symbol.Mode := Intern ("C"); - - Global_Symbol_Table.Insert (Proc_Name, Proc_Symbol); + Register_Subprogram_Specification (Specification (N)); + -- Todo Aspect specifications end Do_Subprogram_Declaration; ---------------------------- @@ -4002,18 +4052,18 @@ package body Tree_Walk is function Do_Subprogram_Or_Block (N : Node_Id) return Irep is Decls : constant List_Id := Declarations (N); HSS : constant Node_Id := Handled_Statement_Sequence (N); - Decls_Rep : Irep; + Reps : constant Irep := New_Irep (I_Code_Block); begin - Decls_Rep := (if Present (Decls) - then Process_Statements (Decls) - else New_Irep (I_Code_Block)); + if Present (Decls) then + Process_Declarations (Decls, Reps); + end if; - Set_Source_Location (Decls_Rep, Sloc (N)); + Set_Source_Location (Reps, Sloc (N)); if Present (HSS) then - Process_Statement (HSS, Decls_Rep); + Process_Statement (HSS, Reps); end if; - return Decls_Rep; + return Reps; end Do_Subprogram_Or_Block; -------------------------------- @@ -4273,6 +4323,54 @@ package body Tree_Walk is end Do_Unconstrained_Array_Definition; + ------------------------- + -- Do_Withed_Unit_Spec -- + ------------------------- + + procedure Do_Withed_Unit_Spec (N : Node_Id) is + Unit_Name : constant String := Get_Name_String (Get_Unit_Name (N)); + begin + if Defining_Entity (N) = Stand.Standard_Standard or else + Unit_Name = "system%s" + then + -- At the moment Standard or System are not processed: TODO + null; + else + -- Handle all other withed library unit declarations + case Nkind (N) is + when N_Subprogram_Body => + if Acts_As_Spec (N) then + -- The unit is a withed library unit which subprogram body + -- that has no separate declaration, or, + -- it is the subprogram body of the compilation unit being + -- compiled and it has no separate declaration. + -- Obtain the subprogram specification from the body + -- and insert it into the symbol table. + Register_Subprogram_Specification (Specification (N)); + else + null; + end if; + when N_Subprogram_Declaration => + -- The unit is withed library unit that is a subprogram + -- declaration, or, + -- it is the declaration of the compilation unit body being + -- compiled. + -- Do_Subprogram_Declaration enters the specification of the + -- subprogram into the symbol table. + Do_Subprogram_Declaration (N); + when N_Package_Declaration => + Do_Package_Declaration (N); + when N_Package_Body => + null; + when others => + Put_Line (Standard_Error, + "This type of library_unit is not yet handled"); + end case; + + end if; + + end Do_Withed_Unit_Spec; + ------------------------- -- Find_Record_Variant -- ------------------------- @@ -4926,81 +5024,247 @@ package body Tree_Walk is end; end Maybe_Make_Typecast; + -------------------------------- + -- Warn_Unhandled_Construct -- + -------------------------------- + + procedure Warn_Unhandled_Construct (C : Construct; Mess : String) is + S : constant String := + (case C is + when Declaration => " declarations ", + when Statement => " statements ") & "unhandled"; + begin + Put_Line (Standard_Error, "Warning: " & Mess & S); + end Warn_Unhandled_Construct; + + -------------------------- + -- Process_Declaration -- + -------------------------- + + procedure Process_Declaration (N : Node_Id; Block : Irep) is + begin + -- Deal with the declaration + + case Nkind (N) is + + -- basic_declarations -- + + when N_Full_Type_Declaration => + Do_Full_Type_Declaration (N); + + when N_Subtype_Declaration => + Do_Subtype_Declaration (N); + + when N_Object_Declaration => + Do_Object_Declaration (N, Block); + + when N_Number_Declaration => + Warn_Unhandled_Construct (Declaration, "Number"); + + when N_Subprogram_Declaration => + Do_Subprogram_Declaration (N); + + when N_Abstract_Subprogram_Declaration => + Warn_Unhandled_Construct + (Declaration, "Abstract subprogram"); + + when N_Package_Declaration => + Warn_Unhandled_Construct (Declaration, "Package"); + + when N_Renaming_Declaration => + Warn_Unhandled_Construct (Declaration, "Renaming"); + + when N_Exception_Declaration => + Warn_Unhandled_Construct (Declaration, "Exception"); + + when N_Generic_Declaration => + Warn_Unhandled_Construct (Declaration, "Generic"); + + when N_Generic_Instantiation => + Warn_Unhandled_Construct (Declaration, "Generic instantiation"); + + -- basic_declarative_items -- + + when N_Representation_Clause => + Warn_Unhandled_Construct (Declaration, "Representation clause"); + + when N_Use_Package_Clause => + Warn_Unhandled_Construct (Declaration, "Use package clause"); + + when N_Use_Type_Clause => + Warn_Unhandled_Construct (Declaration, "Use type clause"); + + -- remaining declarative items -- + + -- proper_body -- + + when N_Subprogram_Body => + Do_Subprogram_Body (N); + + when N_Package_Body => + Warn_Unhandled_Construct (Declaration, "Package body"); + + when N_Task_Body => + Warn_Unhandled_Construct (Declaration, "Task body"); + + when N_Protected_Body => + Warn_Unhandled_Construct (Declaration, "Protected body"); + + -- body_stub -- + + when N_Subprogram_Body_Stub => + Warn_Unhandled_Construct (Declaration, "Subprogram body stub"); + + when N_Package_Body_Stub => + Warn_Unhandled_Construct (Declaration, "Package body stub"); + + when N_Task_Body_Stub => + Warn_Unhandled_Construct (Declaration, "Task body stub"); + + when N_Protected_Body_Stub => + Warn_Unhandled_Construct (Declaration, "Protected body stub"); + + -- Pragmas may appear in declarations -- + + when N_Pragma => + Warn_Unhandled_Construct (Declaration, "Pragmas in"); + + -- Every code lable is implicitly declared in -- + -- the closest surrounding block -- + + when N_Implicit_Label_Declaration => + -- Ignore for now, as I guess an implicit label can't be + -- referenced. + -- Yes it can: this is the declaration of the name it appears + -- the declaritve section but is used on a statement. + null; + + -- Not sure the nex two should be here -- + when N_Itype_Reference => + Do_Itype_Reference (N); + + when N_Freeze_Entity => + -- Ignore, nothing to generate + null; + + when others => + Report_Unhandled_Node_Empty (N, "Process_Declaration", + "Unknown declaration kind"); + + end case; + + end Process_Declaration; + + -------------------------- + -- Process_Declarations -- + -------------------------- + + procedure Process_Declarations (L : List_Id; Block : Irep) is + Decl : Node_Id := First (L); + begin + while Present (Decl) loop + Process_Declaration (Decl, Block); + Next (Decl); + end loop; + + end Process_Declarations; + ------------------------- -- Process_Statement -- ------------------------- procedure Process_Statement (N : Node_Id; Block : Irep) is - procedure Warn_Unhandled_Statement (M : String); - procedure Warn_Unhandled_Statement (M : String) is - begin - Put_Line (Standard_Error, "Warning: " & M & "statements unhandled"); - end Warn_Unhandled_Statement; begin -- Deal with the statement case Nkind (N) is + -- Simple statements -- + when N_Null_Statement => + null; + when N_Assignment_Statement => Append_Op (Block, Do_Assignment_Statement (N)); + when N_Exit_Statement => + Append_Op (Block, Do_Exit_Statement (N)); + + when N_Goto_Statement => + Warn_Unhandled_Construct (Statement, "goto"); + when N_Procedure_Call_Statement => Append_Op (Block, Do_Procedure_Call_Statement (N)); when N_Simple_Return_Statement => Append_Op (Block, Do_Simple_Return_Statement (N)); - when N_Object_Declaration => - Do_Object_Declaration (N, Block); + when N_Entry_Call_Statement => + Warn_Unhandled_Construct (Statement, "entry_call"); - when N_Handled_Sequence_Of_Statements => - Append_Op (Block, Do_Handled_Sequence_Of_Statements (N)); + when N_Requeue_Statement => + Warn_Unhandled_Construct (Statement, "requeue"); + + when N_Delay_Statement => + Warn_Unhandled_Construct (Statement, "delay"); + + when N_Abort_Statement => + Warn_Unhandled_Construct (Statement, "abort"); + + when N_Raise_Statement => + Warn_Unhandled_Construct (Statement, "raise"); + + when N_Code_Statement => + Warn_Unhandled_Construct (Statement, "code"); + + -- Compound statements when N_If_Statement => Append_Op (Block, Do_If_Statement (N)); - when N_Implicit_Label_Declaration => - -- Ignore for now, as I guess an implicit label can't be - -- referenced. - null; + when N_Case_Statement => + Warn_Unhandled_Construct (Statement, "case"); when N_Loop_Statement => Append_Op (Block, Do_Loop_Statement (N)); - when N_Full_Type_Declaration => - Do_Full_Type_Declaration (N); + when N_Block_Statement => + Warn_Unhandled_Construct (Statement, "block"); - when N_Subtype_Declaration => - Do_Subtype_Declaration (N); + when N_Handled_Sequence_Of_Statements => -- this seems incorrct + -- It should be block_statement + Append_Op (Block, Do_Handled_Sequence_Of_Statements (N)); - when N_Freeze_Entity => - -- Ignore, nothing to generate - null; + when N_Extended_Return_Statement => + Warn_Unhandled_Construct (Statement, "extended_return"); - when N_Itype_Reference => - Do_Itype_Reference (N); + when N_Accept_Statement => + Warn_Unhandled_Construct (Statement, "accept"); - when N_Subprogram_Declaration => - Do_Subprogram_Declaration (N); + -- Select statements -- - when N_Subprogram_Body => - Do_Subprogram_Body (N); + when N_Selective_Accept => + Warn_Unhandled_Construct (Statement, "selective_accept"); - when N_Null_Statement => - null; + when N_Timed_Entry_Call => + Warn_Unhandled_Construct (Statement, "timed_entry_call"); - when N_Exit_Statement => - Append_Op (Block, Do_Exit_Statement (N)); + when N_Conditional_Entry_Call => + Warn_Unhandled_Construct (Statement, "conditional_entry_call"); + + when N_Asynchronous_Select => + Warn_Unhandled_Construct (Statement, "asychronous select"); + + -- Pragmas may placed in sequences of statements -- when N_Pragma => Do_Pragma (N, Block); - when N_Raise_Statement => - Warn_Unhandled_Statement ("Raise"); - - when N_Number_Declaration => - Warn_Unhandled_Statement ("Number declaration"); + -- Not sure the nex two should be here - + -- should they be in declarations? -- +-- when N_Itype_Reference => +-- Do_Itype_Reference (N); - when N_Case_Statement => - Warn_Unhandled_Statement ("Case"); +-- when N_Freeze_Entity => +-- -- Ignore, nothing to generate +-- null; when others => Report_Unhandled_Node_Empty (N, "Process_Statement", @@ -5038,6 +5302,29 @@ package body Tree_Walk is return Reps; end Process_Statements; + --------------------------------------- + -- Register_Subprogram_Specification -- + --------------------------------------- + + procedure Register_Subprogram_Specification (N : Node_Id) is + Subprog_Type : constant Irep := + Do_Subprogram_Specification (N); + Subprog_Name : constant Symbol_Id := + Intern (Unique_Name (Defining_Unit_Name (N))); + + Subprog_Symbol : Symbol; + + begin + Subprog_Symbol.Name := Subprog_Name; + Subprog_Symbol.BaseName := Subprog_Name; + Subprog_Symbol.PrettyName := Subprog_Name; + Subprog_Symbol.SymType := Subprog_Type; + Subprog_Symbol.Mode := Intern ("C"); + Subprog_Symbol.Value := Make_Nil (Sloc (N)); + + Global_Symbol_Table.Insert (Subprog_Name, Subprog_Symbol); + end Register_Subprogram_Specification; + procedure Remove_Entity_Substitution (E : Entity_Id) is begin Identifier_Substitution_Map.Delete (E); diff --git a/testsuite/gnat2goto/tests/long_integer/test_long_integer.adb b/testsuite/gnat2goto/tests/long_integer/test_long_integer.adb index 795bb6ca0..c145999d6 100644 --- a/testsuite/gnat2goto/tests/long_integer/test_long_integer.adb +++ b/testsuite/gnat2goto/tests/long_integer/test_long_integer.adb @@ -1,4 +1,3 @@ -with Ada.Text_IO; procedure Test_Long_Integer is x: Long_Long_Integer := 1152921504606846976; begin diff --git a/testsuite/gnat2goto/tests/package_type/package_type.adb b/testsuite/gnat2goto/tests/package_type/package_type.adb new file mode 100644 index 000000000..ddde5cac0 --- /dev/null +++ b/testsuite/gnat2goto/tests/package_type/package_type.adb @@ -0,0 +1,9 @@ +with Test; use Test; +-- without "use" just "with" does not introduce the operators associated with +-- the type from with-ed package +procedure Package_Type +is + Small_Number : Range_10 := 4; +begin + pragma Assert (Small_Number * 2 = 8); +end Package_Type; diff --git a/testsuite/gnat2goto/tests/package_type/test.ads b/testsuite/gnat2goto/tests/package_type/test.ads new file mode 100644 index 000000000..05b22d4e8 --- /dev/null +++ b/testsuite/gnat2goto/tests/package_type/test.ads @@ -0,0 +1,4 @@ +package Test +is + type Range_10 is range 1..10; +end Test; diff --git a/testsuite/gnat2goto/tests/package_type/test.out b/testsuite/gnat2goto/tests/package_type/test.out new file mode 100644 index 000000000..c0794a357 --- /dev/null +++ b/testsuite/gnat2goto/tests/package_type/test.out @@ -0,0 +1 @@ +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/package_type/test.py b/testsuite/gnat2goto/tests/package_type/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/package_type/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() diff --git a/testsuite/gnat2goto/tests/packages/packages.adb b/testsuite/gnat2goto/tests/packages/packages.adb new file mode 100644 index 000000000..4ddf8c2da --- /dev/null +++ b/testsuite/gnat2goto/tests/packages/packages.adb @@ -0,0 +1,7 @@ +with Test; + +procedure Packages +is +begin + pragma Assert (Test.Double (1) = 2); +end Packages; diff --git a/testsuite/gnat2goto/tests/packages/test.adb b/testsuite/gnat2goto/tests/packages/test.adb new file mode 100644 index 000000000..44479a29f --- /dev/null +++ b/testsuite/gnat2goto/tests/packages/test.adb @@ -0,0 +1,8 @@ +package body Test +is + function Double(Input : Positive) return Positive + is + begin + return Input + Input; + end Double; +end Test; diff --git a/testsuite/gnat2goto/tests/packages/test.ads b/testsuite/gnat2goto/tests/packages/test.ads new file mode 100644 index 000000000..05dc3c4b1 --- /dev/null +++ b/testsuite/gnat2goto/tests/packages/test.ads @@ -0,0 +1,4 @@ +package Test +is + function Double(Input : Positive) return Positive; +end Test; diff --git a/testsuite/gnat2goto/tests/packages/test.opt b/testsuite/gnat2goto/tests/packages/test.opt new file mode 100644 index 000000000..b585e32d0 --- /dev/null +++ b/testsuite/gnat2goto/tests/packages/test.opt @@ -0,0 +1 @@ +ALL XFAIL cbmc returns failed verification (calling function without body) diff --git a/testsuite/gnat2goto/tests/packages/test.py b/testsuite/gnat2goto/tests/packages/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/packages/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove()