File size: 650 Bytes
d8df231
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
-- Copyright (c) 2026 Ahmad Ali Parr. All rights reserved.
-- SPDX-License-Identifier: LicenseRef-Proprietary
-- Public source visibility does not grant an open-source license. See LICENSE.

package body Heap_Model with SPARK_Mode is

   function Used (H : Heap) return Count is (H.Allocated);

   procedure Reset (H : out Heap) is
   begin
      H := (Allocated => 0);
   end Reset;

   procedure Allocate (H : in out Heap; Success : out Boolean) is
   begin
      if H.Allocated < Capacity then
         H.Allocated := H.Allocated + 1;
         Success := True;
      else
         Success := False;
      end if;
   end Allocate;

end Heap_Model;