symex_nondet_generatort Class Reference

Functor generating fresh nondet symbols. More...

#include <path_storage.h>

Public Member Functions
nondet_symbol_exprt	operator() (typet type, source_locationt location)

Private Attributes
std::size_t	nondet_count = 0

Detailed Description

Functor generating fresh nondet symbols.

Definition at line 22 of file path_storage.h.

Member Function Documentation

operator()()

nondet_symbol_exprt symex_nondet_generatort::operator()	(	typet	type,
		source_locationt	location
	)

Definition at line 16 of file path_storage.cpp.

Member Data Documentation

nondet_count

std::size_t symex_nondet_generatort::nondet_count = 0

private

Definition at line 28 of file path_storage.h.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-symex/path_storage.h
• /home/runner/work/cbmc/cbmc/src/goto-symex/path_storage.cpp