Note that this only applies to goto programs that are user provided, that internal transformations on goto programs don't produce invalid programs should be guarded by invariants instead.

See also: invariant.h

Definition at line 91 of file exception_utils.h.

Constructor & Destructor Documentation

◆ incorrect_goto_program_exceptiont() [1/3]

incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont ( std::string message )

explicit

Definition at line 52 of file exception_utils.cpp.

◆ incorrect_goto_program_exceptiont() [2/3]

template<typename Diagnostic , typename... Diagnostics>

incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont ( std::string message,

Diagnostic && diagnostic,

Diagnostics &&... diagnostics

)

Definition at line 117 of file exception_utils.h.

◆ incorrect_goto_program_exceptiont() [3/3]

template<typename... Diagnostics>

incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont ( std::string message,

source_locationt source_location,

Diagnostics &&... diagnostics

)

Definition at line 130 of file exception_utils.h.

Member Function Documentation

◆ what()

std::string incorrect_goto_program_exceptiont::what ( ) const

overridevirtual

A human readable description of what went wrong.

For readability, implementors should not add a leading or trailing newline to this description.

Reimplemented from cprover_exception_baset.

Definition at line 59 of file exception_utils.cpp.

Member Data Documentation

◆ diagnostics

std::string incorrect_goto_program_exceptiont::diagnostics

private

Definition at line 113 of file exception_utils.h.

◆ source_location

source_locationt incorrect_goto_program_exceptiont::source_location

private

Definition at line 111 of file exception_utils.h.

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

/home/runner/work/cbmc/cbmc/src/util/exception_utils.h
/home/runner/work/cbmc/cbmc/src/util/exception_utils.cpp