cprover
Loading...
Searching...
No Matches
fatal_assertions.cpp File Reference

Fatal Assertions. More...

#include "fatal_assertions.h"
#include <util/irep_hash.h>
#include <goto-programs/goto_functions.h>
#include <stack>
#include <unordered_set>
Include dependency graph for fatal_assertions.cpp:

Go to the source code of this file.

Classes

struct  function_loc_pairt
struct  function_itt_hasht
struct  function_loc_pair_hasht

Typedefs

using loc_sett

Functions

static loc_sett reachable_fixpoint (const loc_sett &locs, const goto_functionst &goto_functions)
void propagate_fatal_to_proven (propertiest &properties, const goto_functionst &goto_functions)
 Proven assertions after refuted fatal assertions are marked as UNKNOWN.
void propagate_fatal_assertions (propertiest &properties, const goto_functionst &goto_functions)
 Proven assertions after refuted fatal assertions are marked as UNKNOWN.

Detailed Description

Fatal Assertions.

Definition in file fatal_assertions.cpp.

Typedef Documentation

◆ loc_sett

using loc_sett
Initial value:
std::unordered_set<function_loc_pairt, function_loc_pair_hasht>

Definition at line 58 of file fatal_assertions.cpp.

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.

◆ propagate_fatal_to_proven()

void propagate_fatal_to_proven ( propertiest & properties,
const goto_functionst & goto_functions )

Proven assertions after refuted fatal assertions are marked as UNKNOWN.

Definition at line 114 of file fatal_assertions.cpp.

◆ reachable_fixpoint()

loc_sett reachable_fixpoint ( const loc_sett & locs,
const goto_functionst & goto_functions )
static

Definition at line 62 of file fatal_assertions.cpp.