CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
fatal_assertions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Fatal Assertions
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H
13#define CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H
14
15#include "properties.h"
16
17class goto_functionst;
18
21void propagate_fatal_assertions(propertiest &, const goto_functionst &);
22
23#endif // CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H
goto_functionst
A collection of goto functions.
Definition goto_functions.h:25
propagate_fatal_assertions
void propagate_fatal_assertions(propertiest &, const goto_functionst &)
Proven assertions after refuted fatal assertions are marked as UNKNOWN.
Definition fatal_assertions.cpp:167
properties.h
Properties.
propertiest
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76