Do cu specs

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

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/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;

testsuite/gnat2goto/tests/package_type/test.ads

@@ -0,0 +1,4 @@
+package Test
+is
+   type Range_10 is range 1..10;
+end Test;

testsuite/gnat2goto/tests/package_type/test.out

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

testsuite/gnat2goto/tests/package_type/test.py

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

testsuite/gnat2goto/tests/packages/packages.adb

@@ -0,0 +1,7 @@
+with Test;
+
+procedure Packages
+is
+begin
+   pragma Assert (Test.Double (1) = 2);
+end Packages;

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;

testsuite/gnat2goto/tests/packages/test.ads

@@ -0,0 +1,4 @@
+package Test
+is
+   function Double(Input : Positive) return Positive;
+end Test;

testsuite/gnat2goto/tests/packages/test.opt

@@ -0,0 +1 @@
+ALL XFAIL cbmc returns failed verification (calling function without body)

testsuite/gnat2goto/tests/packages/test.py

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