insert_final_assert_false.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Insert assert(false) at end of entry function
 
Author: Nathan Chong, Kareem Khazem
 
\*******************************************************************/
 
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
#define CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
 
#include <string>
 
#include <util/message.h>
 
class goto_modelt;
 
class insert_final_assert_falset
{
public:
  explicit insert_final_assert_falset(message_handlert &_message_handler);
  bool operator()(goto_modelt &, const std::string &);
 
private:
  messaget log;
};
 
bool insert_final_assert_false(
  goto_modelt &goto_model,
  const std::string &function_to_instrument,
  message_handlert &message_handler);
 
// clang-format off
#define OPT_INSERT_FINAL_ASSERT_FALSE \
  "(insert-final-assert-false):"
 
#define HELP_INSERT_FINAL_ASSERT_FALSE \
  " --insert-final-assert-false <function>\n" \
  /* NOLINTNEXTLINE(whitespace/line_length) */ \
  "                              generate assert(false) at end of function\n"
// clang-format on
 
#endif // CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H