C++ destructor in Ada

build.gpr

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

capdpa-foo.adb

package body Capdpa.Foo
is
   procedure Finalize (This : in out Controlled_Class)
   is
   begin
      Destructor (This.Data);
   end Finalize;

end Capdpa.Foo;

capdpa-foo.ads

with Ada.Finalization;

package Capdpa.Foo
   with SPARK_Mode => Off
is
   type Class is
   limited record
      null;
   end record
   with Import, Convention => CPP;

   type Class_Address is private;

   function Constructor return Class
   with Global => null;
   pragma Cpp_Constructor (Constructor, "_ZN3FooC1Ev");

   procedure Destructor (This : in out Class)
   with Global => null;
   pragma Import (Cpp, Destructor, "_ZN3FooD1Ev");

   type Controlled_Class is tagged limited private;

private
   pragma SPARK_Mode (Off);

   type Controlled_Class is new Ada.Finalization.Limited_Controlled with
   record
      Data : Class := Constructor;
   end record;

   overriding procedure Finalize (This : in out Controlled_Class);

   type Class_Address is access Class;

end Capdpa.Foo;

capdpa.ads

with Interfaces.C;
with Interfaces.C.Extensions;
package Capdpa
   with SPARK_Mode => Off
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 Capdpa;

foo.cpp

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

Foo::Foo() {
   std::cout << "Constructor called" << std::endl;
}

Foo::~Foo() {
   std::cout << "Destructor called" << std::endl;
}

foo.h

class Foo {
   public:
      Foo();
      ~Foo();
      int method();
};

main.adb

with Capdpa.Foo;

procedure Main
is
   use Capdpa;
   F : Foo.Controlled_Class;
begin
   null;
end Main;