ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
show_claims.h
Go to the documentation of this file.
1#ifndef CPROVER_GOTO_PROGRAMS_SHOW_CLAIMS_H
2#define CPROVER_GOTO_PROGRAMS_SHOW_CLAIMS_H
3
4#include <goto-programs/goto_functions.h>
5#include <util/symtab/namespace.h>
6#include <util/message/message.h>
7
8void show_claims(const namespacet &ns, const goto_functionst &goto_functions);
9
10void show_claims(const namespacet &ns, const goto_programt &goto_program);
11
12#endif
goto_functionst
Definition goto_functions.h:56
goto_programt
A generic container class for a control flow graph for one function, in the form of a goto-program.
Definition goto_program.h:63
namespacet
Definition namespace.h:10
goto_functions.h
show_claims
void show_claims(const namespacet &ns, const goto_functionst &goto_functions)
Definition show_claims.cpp:37