cprover
insert_final_assert_false.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Insert assert(false) at end of entry function
4
5Author: Nathan Chong, Kareem Khazem
6
7\*******************************************************************/
8
11
16
17#ifndef CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
18#define CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
19
20#include <string>
21
22#include <util/message.h>
23
24class goto_modelt;
25
27{
28public:
29 explicit insert_final_assert_falset(message_handlert &_message_handler);
30 bool operator()(goto_modelt &, const std::string &);
31
32private:
34};
35
45 goto_modelt &goto_model,
46 const std::string &function_to_instrument,
47 message_handlert &message_handler);
48
49// clang-format off
50#define OPT_INSERT_FINAL_ASSERT_FALSE \
51 "(insert-final-assert-false):"
52
53#define HELP_INSERT_FINAL_ASSERT_FALSE \
54 " --insert-final-assert-false <function>\n" \
55 /* NOLINTNEXTLINE(whitespace/line_length) */ \
56 " generate assert(false) at end of function\n"
57// clang-format on
58
59#endif // CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
bool operator()(goto_modelt &, const std::string &)
insert_final_assert_falset(message_handlert &_message_handler)
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
bool insert_final_assert_false(goto_modelt &goto_model, const std::string &function_to_instrument, message_handlert &message_handler)
Transform a goto program by inserting assert(false) at the end of a given function function_to_instru...