Add test-case for packages

Also includes cprover_start even when there is no function to call in a CU.

Author: Petr Bauch

gnat2goto/driver/driver.adb

@@ -226,6 +226,17 @@ package body Driver is
       end;
 
       if not Add_Start then
+         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

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

testsuite/gnat2goto/tests/packages/packages.adb

@@ -0,0 +1,7 @@
+with Test;
+
+procedure Packages
+is
+begin
+   Test.Foo (1);
+end Packages;

testsuite/gnat2goto/tests/packages/test.adb

@@ -0,0 +1,12 @@
+package body Test
+is
+   procedure Foo(Input : Positive)
+   is
+   begin
+      if (Input > 5) then
+         null;
+      else
+         null;
+      end if;
+   end Foo;
+end Test;

testsuite/gnat2goto/tests/packages/test.ads

@@ -0,0 +1,4 @@
+package Test
+is
+   procedure Foo(Input : Positive);
+end Test;

testsuite/gnat2goto/tests/packages/test.out

@@ -0,0 +1 @@
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/packages/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()