postcondition.h File Reference

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

Go to the source code of this file.

Functions
void	postcondition (const namespacet &ns, const value_setst &value_sets, const symex_target_equationt &equation, const class goto_symex_statet &s, exprt &dest)

Detailed Description

Generate Equation using Symbolic Execution

Definition in file postcondition.h.

Function Documentation

postcondition()

void postcondition	(	const namespacet &	ns,
		const value_setst &	value_sets,
		const symex_target_equationt &	equation,
		const class goto_symex_statet &	s,
		exprt &	dest
	)