diff --git a/doc/value/main.tex b/doc/value/main.tex index 212c430d7b9dc9e7a5b62c67c6ff6e273124e511..0afcb450bff549d6154ee7f9f9d44de778deaae3 100644 --- a/doc/value/main.tex +++ b/doc/value/main.tex @@ -5372,15 +5372,13 @@ They are listed here for completeness. \begin{tabular}{llll} \multicolumn{3}{c}{Dynamic memory allocation builtins} \\ \hline - \lstinline|Frama_C_alloc_by_stack| & - \lstinline|Frama_C_vla_alloc_by_stack| & - \lstinline|Frama_C_malloc_fresh| \\ - \lstinline|Frama_C_calloc_by_stack| & - \lstinline|Frama_C_calloc_fresh| & - \lstinline|Frama_C_free| \\ - \lstinline|Frama_C_realloc| & - \lstinline|Frama_C_realloc_multiple| & - \lstinline|Frama_C_vla_free| + \lstinline|Frama_C_malloc| & + \lstinline|Frama_C_alloca| & + \lstinline|Frama_C_vla_alloc| \\ + \lstinline|Frama_C_calloc| & + \lstinline|Frama_C_free| & + \lstinline|Frama_C_vla_free| \\ + \lstinline|Frama_C_realloc| \end{tabular} \end{table}