C++ method in Ada

.gitignore

obj

build.gpr

project Build
is
   for Create_Missing_Dirs use "True";
   for Languages use ("C++", "Ada");
   for Object_Dir use "obj";
   for Main use ("main.cpp");
end Build;

example-foo.adb

pragma Ada_2012;
package body Example.Foo is

   ------------
   -- Offset --
   ------------

   function Offset
     (This : Class;
      Val : Example.Int)
      return Example.Int
   is
      use Interfaces.C;
   begin
      return Int (This.Private_X_Value) + Val;
   end Offset;

end Example.Foo;

example-foo.ads

package Example.Foo
   with SPARK_Mode
is
   type Private_Int is limited private;

   type Class is
   limited record
      Private_X_Value : Private_Int;
   end record
   with Import, Convention => CPP;

   type Class_Address is private;

   function Constructor (Arg1 : Example.Int) return Class
   with Global => null;
   pragma Cpp_Constructor (Constructor, "_ZN3FooC1Ei");

   function Offset (This : Class; Val : Example.Int) return Example.Int
   with Global => null, Export, Convention => CPP, External_Name => "_ZN3Foo6offsetEi";

private
   pragma SPARK_Mode (Off);

   type Class_Address is access Class;
   type Private_Int is new Example.Int;
end Example.Foo;

example.ads

with Interfaces.C;
with Interfaces.C.Extensions;
package Example
   with SPARK_Mode
is
   subtype Bool is Interfaces.C.Extensions.bool;
   subtype Unsigned_Char is Interfaces.C.unsigned_char;
   subtype Unsigned_Short is Interfaces.C.unsigned_short;
   subtype Unsigned_Int is Interfaces.C.unsigned;
   subtype Unsigned_Long is Interfaces.C.unsigned_long;
   subtype Unsigned_Long_Long is Interfaces.C.Extensions.unsigned_long_long;
   subtype Char is Interfaces.C.char;
   subtype Signed_Char is Interfaces.C.signed_char;
   subtype Wchar_t is Interfaces.C.wchar_t;
   subtype Short is Interfaces.C.short;
   subtype Int is Interfaces.C.int;
   subtype C_X_Int128 is Interfaces.C.Extensions.Signed_128;
   --  unsigned __int128 is not defined in Interfaces.C.Extensions
   subtype Long is Interfaces.C.long;
   subtype Long_Long is Interfaces.C.Extensions.long_long;
   subtype C_float is Interfaces.C.C_float;
   subtype Double is Interfaces.C.double;
   type Long_Double is private;
   subtype Void is Interfaces.C.Extensions.void;
   subtype Void_Address is Interfaces.C.Extensions.void_ptr;

   type Bool_Address is private;
   type Unsigned_Char_Address is private;
   type Unsigned_Short_Address is private;
   type Unsigned_Int_Address is private;
   type Unsigned_Long_Address is private;
   type Unsigned_Long_Long_Address is private;
   type Char_Address is private;
   type Signed_Char_Address is private;
   type Wchar_t_Address is private;
   type Short_Address is private;
   type Int_Address is private;
   type C_X_Int128_Address is private;
   type Long_Address is private;
   type Long_Long_Address is private;
   type C_float_Address is private;
   type Double_Address is private;
   type Long_Double_Address is private;

private

   pragma SPARK_Mode(Off);

   type Long_Double is new Interfaces.C.long_double;

   type Bool_Address is access all Bool;
   type Unsigned_Char_Address is access all Unsigned_Char;
   type Unsigned_Short_Address is access all Unsigned_Short;
   type Unsigned_Int_Address is access all Unsigned_Int;
   type Unsigned_Long_Address is access all Unsigned_Long;
   type Unsigned_Long_Long_Address is access all Unsigned_Long_Long;
   type Char_Address is access all Char;
   type Signed_Char_Address is access all Signed_Char;
   type Wchar_t_Address is access all Wchar_t;
   type Short_Address is access all Short;
   type Int_Address is access all Int;
   type C_X_Int128_Address is access all C_X_Int128;
   type Long_Address is access all Long;
   type Long_Long_Address is access all Long_Long;
   type C_float_Address is access all C_float;
   type Double_Address is access all Double;
   type Long_Double_Address is access all Long_Double;

end Example;

foo.cpp

#include "foo.h"

Foo::Foo (int val) : _value(val) { }
//int Foo::offset (int val) { return _value + val; };

foo.h

class Foo {
      int _value;
   public:
      Foo(int);
      int offset (int val);
};

main.cpp

#include "foo.h"
#include <iostream>

int
main()
{
   std::cout << "Started" << std::endl;
   Foo foo (17);
   int result = foo.offset(5);
   std::cout << "Result: " << result << std::endl;
}