CBMC
fatal_assertions.h File Reference

Fatal Assertions. More...

#include "properties.h"
+ Include dependency graph for fatal_assertions.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void propagate_fatal_assertions (propertiest &, const goto_functionst &)
 Proven assertions after refuted fatal assertions are marked as UNKNOWN. More...
 

Detailed Description

Fatal Assertions.

Definition in file fatal_assertions.h.

Function Documentation

◆ propagate_fatal_assertions()

void propagate_fatal_assertions ( propertiest properties,
const goto_functionst goto_functions 
)

Proven assertions after refuted fatal assertions are marked as UNKNOWN.

Definition at line 167 of file fatal_assertions.cpp.