goto_coverage.cpp File Reference

#include <goto-programs/goto_coverage.h>
#include <goto-programs/k_path_spanning.h>
#include <irep2/irep2_utils.h>
#include <algorithm>
#include <cassert>
#include <deque>
#include <map>
#include <set>
#include <vector>

Include dependency graph for goto_coverage.cpp:

Functions
static size_t	expr_depth (const expr2tc &e, size_t cap)
static bool	kpath_atoms_comparison_unsat (const std::vector< std::pair< expr2tc, bool > > &atoms)
static void	replace_operands (expr2tc &expr, bool sub_top_level, const std::function< expr2tc(const expr2tc &, bool)> &recurse)
	Recursively maps each operand of expr through handle_single_guard (with the supplied sub_top_level), in place.

Function Documentation

expr_depth()

size_t expr_depth ( const expr2tc & e, size_t cap )

static

kpath_atoms_comparison_unsat()

bool kpath_atoms_comparison_unsat ( const std::vector< std::pair< expr2tc, bool > > & atoms )

static

replace_operands()

void replace_operands ( expr2tc & expr, bool sub_top_level, const std::function< expr2tc(const expr2tc &, bool)> & recurse )

static

Recursively maps each operand of expr through handle_single_guard (with the supplied sub_top_level), in place.

Foreach_operand detaches the irep_container before mutating, so this is safe even when expr shares storage with its caller.