cprover
symex_nondet_generatort Class Reference

Functor generating fresh nondet symbols. More...

#include <goto_symex.h>

Public Member Functions

nondet_symbol_exprt operator() (typet &type)
 

Private Attributes

unsigned nondet_count = 0
 

Detailed Description

Functor generating fresh nondet symbols.

Definition at line 42 of file goto_symex.h.

Member Function Documentation

◆ operator()()

nondet_symbol_exprt symex_nondet_generatort::operator() ( typet type)

Definition at line 24 of file goto_symex.cpp.

Member Data Documentation

◆ nondet_count

unsigned symex_nondet_generatort::nondet_count = 0
private

Definition at line 48 of file goto_symex.h.


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