Detect memory allocations whose requested size can exceed a configurable byte bound K (CWE-789, "Memory Allocation with Excessive Size Value"). More...

#include <goto_check_excessive_alloc.h>

Inheritance diagram for goto_check_excessive_alloc:

[legend]

Public Member Functions
	goto_check_excessive_alloc (contextt &context, const BigInt &max_alloc_bytes)
Public Member Functions inherited from goto_functions_algorithm
	goto_functions_algorithm (bool sideffect)
unsigned	get_number_of_functions ()
unsigned	get_number_of_loops ()
bool	run (goto_functionst &) override
	Executes the algorithm over a T object.
void	setTarget (const std::string &_tgt)
Public Member Functions inherited from algorithm< goto_functionst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Protected Member Functions
bool	runOnFunction (std::pair< const irep_idt, goto_functiont > &F) override
Protected Member Functions inherited from goto_functions_algorithm
virtual bool	runOnLoop (loopst &loop, goto_programt &goto_program)
virtual bool	runOnProgram (goto_functionst &)

Protected Attributes
contextt &	context
BigInt	max_alloc_bytes
Protected Attributes inherited from goto_functions_algorithm
std::string	target_function = ""
Protected Attributes inherited from algorithm< goto_functionst >
const bool	sideeffect

Detailed Description

Detect memory allocations whose requested size can exceed a configurable byte bound K (CWE-789, "Memory Allocation with Excessive Size Value").

For every ASSIGN lhs = <alloc> whose right-hand side is a dynamic allocation side-effect — malloc/calloc (calloc lowers to malloc in the operational model), realloc, or operator new[] — the pass inserts ASSERT(byte_size <= K) immediately before the assignment, with comment excessive allocation size: <fn> and property excessive-allocation. If symex finds a model with byte_size > K, that is a CWE-789 witness.

byte_size is the total request in bytes: malloc/realloc already carry a byte size; operator new[n] is pre-scaled to bytes by the Clang frontend (do_cpp_new multiplies the element count by sizeof(element) before setting cmt_size), so the pass compares it directly.

The bound K is a policy choice, not a soundness property: the pass proves "no path reaches an allocation with size > K", not "no path can exhaust memory" (the latter is undecidable in general). The check is independent of --force-malloc-success: the assertion precedes the allocation, so an excessive size is reported whether or not the allocation is forced to succeed.

Runs as a preprocessing algorithm, mirroring goto_check_unchecked_return.

Constructor & Destructor Documentation

◆ goto_check_excessive_alloc()

goto_check_excessive_alloc::goto_check_excessive_alloc	(	contextt &	context,
		const BigInt &	max_alloc_bytes )

inline

Member Function Documentation

◆ runOnFunction()

bool goto_check_excessive_alloc::runOnFunction ( std::pair< const irep_idt, goto_functiont > & F )

overrideprotectedvirtual

Reimplemented from goto_functions_algorithm.

Member Data Documentation

◆ context

contextt& goto_check_excessive_alloc::context

protected

◆ max_alloc_bytes

BigInt goto_check_excessive_alloc::max_alloc_bytes

protected

The documentation for this class was generated from the following files:

src/goto-programs/goto_check_excessive_alloc.h
src/goto-programs/goto_check_excessive_alloc.cpp

Public Member Functions

Protected Member Functions

Protected Attributes