Skip to content

Commit 702ca83

Browse files
committed
doc pntrTempAlloc
1 parent 61a4c78 commit 702ca83

File tree

3 files changed

+55
-17
lines changed

3 files changed

+55
-17
lines changed

src/metamath.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -731,8 +731,8 @@ void command(int argc, char *argv[]);
731731
* will start main with \p argc set to 2, argv[0] to "read set.mm", argv[1]
732732
* to "verify proof *" (both without quotes) and argv[2] to NULL.
733733
* Returning 0 indicates successful completion, anything else some kind of
734-
failure.
735-
* For details see \ref https://en.cppreference.com/w/cpp/language/main_function.
734+
* failure.
735+
* For details see https://en.cppreference.com/w/cpp/language/main_function.
736736
*/
737737
int main(int argc, char *argv[]) {
738738

src/mmdata.c

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2449,7 +2449,7 @@ long g_pntrStartTempAllocStack = 0; /* Where to start freeing temporary alloca
24492449
when pntrLet() is called (normally 0, except in
24502450
special nested vstring functions) */
24512451
/*!
2452-
* \var pntrTempAllocStack
2452+
* \var pntrString *pntrTempAllocStack[]
24532453
* \brief a \ref stack "stack" of \ref temp_pntrString.
24542454
*
24552455
* Holds pointers to temporarily allocated data of type \ref pntrString. Such
@@ -2458,7 +2458,24 @@ long g_pntrStartTempAllocStack = 0; /* Where to start freeing temporary alloca
24582458
*/
24592459
pntrString *pntrTempAllocStack[M_MAX_ALLOC_STACK];
24602460

2461-
2461+
/*!
2462+
* \fn temp_pntrString *pntrTempAlloc(long size)
2463+
* \par size > 0
2464+
* allocates a \ref block capable of holding \p size \ref pntrString entries
2465+
* and pushes it onto the \ref pntrTempAllocStack.
2466+
* \par size == 0
2467+
* pops off all entries from the \ref pntrTempAllocStack and adds them to the
2468+
* \ref memFreePool.
2469+
* \param[in] size count of \ref pntrString entries. This value must include
2470+
* a terminal NULL pointer if needed.
2471+
* \return a pointer to the allocated \ref block, or NULL if deallocation only
2472+
* \pre
2473+
* \p size ==0: all entries in from \ref pntrTempAllocStack from
2474+
* \ref g_pntrTempAllocStackStart do not contain relevant data any more.
2475+
* \post
2476+
* - Exits on out-of-memory
2477+
* - updates \ref db2
2478+
*/
24622479
temp_pntrString *pntrTempAlloc(long size) {
24632480
/* pntrString memory allocation/deallocation */
24642481
/* When "size" is >0, "size" instances of pntrString are allocated. */

src/mmdata.h

Lines changed: 34 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515

1616
/* debugging flags & variables */
1717
/*!
18-
* \var db
18+
* \var long db
1919
* \brief bytes held by vstring instances outside of the stack of temporaries
2020
*
2121
* monitors the number of bytes (including the terminal NUL) currently used in
@@ -31,7 +31,7 @@
3131
/*E*/extern long db;
3232
/*E*/extern long db0;
3333
/*!
34-
* \var db1
34+
* \var long db1
3535
* \brief bytes held by vstring instances inside of the stack of temporaries
3636
*
3737
* monitors the number of bytes currently pointed to by \ref vstring pointers
@@ -43,6 +43,11 @@
4343
* \bug Seems never be displayed.
4444
*/
4545
/*E*/extern long db1;
46+
/*!
47+
* \var long db2
48+
* Bytes held in \ref blocks managed in \ref tempAllocStack
49+
* "temporary pointer stacks".
50+
*/
4651
/*E*/extern long db2;
4752
/*!
4853
* \var db3
@@ -315,27 +320,27 @@ void *poolFixedMalloc(long size /* bytes */);
315320
* \ref memFreePool. If this block exists, but has not sufficient size, it is
316321
* reallocated from the system. If the pool is empty, a new \ref block of
317322
* the given size is allocated from the system. In any case, the header of the
318-
* \ref block is properly initialized.
323+
* \ref block is properly initialized. Exits program on out of memory
324+
* condition.
319325
* \param[in] size (in bytes) of the block, not including the block header.
320326
* \return a free and initialized block of memory with at least the requested
321-
* user space.
322-
* \bug uses outOfMemory that can stack up endlessly
327+
* user space. Exit on out-of-memory
323328
*/
324329
void *poolMalloc(long size /* bytes */);
325330
/*!
326331
* \fn poolFree(void *ptr)
327332
*
328333
* Removes \p ptr from the \ref memUsedPool, if it is listed there. Then tries
329334
* adding it to the \ref memFreePool. If this pool is full, it is increased by
330-
* \ref MEM_POOL_GROW. If this fails, an error is created, else \p ptr is
335+
* \ref MEM_POOL_GROW. If this fails, the program is exited, else \p ptr is
331336
* added.
332337
* \param[in] ptr pointer to a \ref block.
333338
* \pre
334339
* all memory pointed to by \p ptr is considered free. This holds even if it
335340
* it is kept in \ref memUsedPool.
336341
* \post
337-
* \ref poolTotalFree is updated
338-
* \bug calls outOfMemory, that can stack up endlessly
342+
* - \ref poolTotalFree is updated
343+
* - Exit on out-of-memory (the \ref memFreePool overflows)
339344
*/
340345
void poolFree(void *ptr);
341346
/*!
@@ -363,7 +368,7 @@ void poolFree(void *ptr);
363368
* \post
364369
* - \ref poolTotalFree is the current free space in bytes in both pools.
365370
* - A full \ref block is not added to \ref memUsedPool by this function.
366-
* \bug calls outOfMemory, that can stack up endlessly
371+
* - Exit on out-of-memory (\ref memUsedPool overflows)
367372
*/
368373
void addToUsedPool(void *ptr);
369374
/* Purges reset memory pool usage */
@@ -375,7 +380,7 @@ void memFreePoolPurge(flag untilOK);
375380
*
376381
* Return the overall statistics about the pools \ref memFreePool
377382
* "free block array" and the \ref memUsedPool "used block array". In MEMORY
378-
* STATUS mode ON, a diagnostic message compares the the contents of
383+
* STATUS mode ON, a diagnostic message compares the contents of
379384
* \ref poolTotalFree to the values found in this statistics. They should not
380385
* differ!
381386
*
@@ -406,7 +411,7 @@ long getFreeSpace(long max);
406411
/* Fatal memory allocation error */
407412
/*!
408413
* \fn outOfMemory(const char *msg)
409-
* \brief fatal memory allocation error.
414+
* \brief exit after fatal memory allocation error.
410415
*
411416
* called when memory cannot be allocated, either because memory/address space
412417
* is physically exhausted, or because administrative structures would overflow.
@@ -664,12 +669,27 @@ long compressedProofSize(const nmbrString *proof, long statemNum);
664669
/*!
665670
* \var long g_pntrTempAllocStackTop
666671
*
667-
* Index of the current top af the \ref stack "stack" \ref pntrTempAlloc.
672+
* Index of the current top of the \ref stack "stack" \ref pntrTempAlloc.
668673
* New data is pushed from this location on if space available.
669674
*
670675
* \invariant always refers the null pointer element behind the valid data.
671676
*/
672677
extern long g_pntrTempAllocStackTop; /* Top of stack for pntrTempAlloc function */
678+
/*!
679+
* \var long g_pntrTempAllocStackStart
680+
*
681+
* Index of the first entry of the \ref stack "stack" \ref pntrTempAllocStack
682+
* eligible for deallocation on the next call to \ref pntrTempAlloc. Entries
683+
* below this value are considered not dependent on the value at this index,
684+
* but entries above are. So when this entry gets deallocated, dependent ones
685+
* should follow suit. A function like \ref pntrTempAlloc or \ref pntrLet
686+
* manage this automatic deallocation.
687+
* \n
688+
* Nested functions using the \ref pntrTempAllocStack usually save the current
689+
* value and set it to \ref g_pntrTempAllocStackTop, so they can create their
690+
* local dependency chain. On return the saved value is restored.
691+
* \invariant always less or equal to \ref g_pntrTempAllocStackTop.
692+
*/
673693
extern long g_pntrStartTempAllocStack; /* Where to start freeing temporary
674694
allocation when pntrLet() is called (normally 0, except for nested
675695
pntrString functions) */
@@ -698,7 +718,8 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s);
698718
* \post
699719
* - the \ref block \p target points to is filled with a copy of
700720
* \ref pntrString elements \p source points to, padded with a terminal
701-
* NULL, or an outOfMemory error is raised.
721+
* NULL.
722+
* - Exit on out-of-memory
702723
* - due to a possible reallocation the pointer \p target points to may
703724
* change.
704725
*/

0 commit comments

Comments
 (0)