docs/api/symex__invariant_8h_source.html

#pragma once


[[noreturn]] void symex_invariant_violated(

  const char *file,

  unsigned line,

  const char *function,

  const char *condition,

  const char *reason);


#define SYMEX_INVARIANT(condition, reason)                                     \

  ((condition) ? static_cast<void>(0)                                          \

               : symex_invariant_violated(                                     \

                   __FILE__, __LINE__, __func__, #condition, (reason)))


function
Definition module.h:12

symex_invariant_violated
void symex_invariant_violated(const char *file, unsigned line, const char *function, const char *condition, const char *reason)
Release-checked invariant for goto-symex.
Definition symex_invariant.cpp:6