blob: afbcc2fbf18025b4ef7c7b32b75686c86eb0778e [file] [log] [blame]
package Ghost1 is
type Ghost_Typ is record
Data : Integer;
end record
with Ghost;
procedure Spec_And_Body (Obj : Ghost_Typ)
with Ghost;
end Ghost1;