precondition.h File Reference

#include "goto-programs/goto_program.h"

Include dependency graph for precondition.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	precondition (const namespacet &ns, value_setst &value_sets, const goto_programt::const_targett target, const symex_target_equationt &equation, const class goto_symex_statet &s, exprt &dest)

Detailed Description

Generate Equation using Symbolic Execution

Definition in file precondition.h.

Function Documentation

precondition()

void precondition	(	const namespacet &	ns,
		value_setst &	value_sets,
		const goto_programt::const_targett	target,
		const symex_target_equationt &	equation,
		const class goto_symex_statet &	s,
		exprt &	dest
	)