CBMC
fatal_assertions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fatal Assertions
4 
5 Author: 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 
17 class goto_functionst;
18 
21 void 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