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 = std::unordered_set< function_loc_pairt, function_loc_pair_hasht >

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 = 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()

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

static

Definition at line 62 of file fatal_assertions.cpp.

Classes

Typedefs