safety_checker.h File Reference

Safety Checker Interface. More...

#include <util/invariant.h>
#include <util/message.h>
#include "goto_trace.h"

Include dependency graph for safety_checker.h:

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

Go to the source code of this file.

Classes
class	safety_checkert

Functions
safety_checkert::resultt &	operator&= (safety_checkert::resultt &a, safety_checkert::resultt const &b)
	The worst of two results. More...
safety_checkert::resultt &	operator|= (safety_checkert::resultt &a, safety_checkert::resultt const &b)
	The best of two results. More...

Detailed Description

Safety Checker Interface.

Definition in file safety_checker.h.

Function Documentation

operator&=()

safety_checkert::resultt& operator&= ( safety_checkert::resultt &  a, safety_checkert::resultt const &  b  )

inline

The worst of two results.

A result of PAUSED means that the safety check has not yet completed, thus it makes no sense to compare it to the result of a completed safety check. Therefore do not pass safety_checkert::resultt:PAUSED as an argument to this function.

Definition at line 64 of file safety_checker.h.

operator|=()

safety_checkert::resultt& operator|= ( safety_checkert::resultt &  a, safety_checkert::resultt const &  b  )

inline

The best of two results.

A result of PAUSED means that the safety check has not yet completed, thus it makes no sense to compare it to the result of a completed safety check. Therefore do not pass safety_checkert::resultt:PAUSED as an argument to this function.

Definition at line 92 of file safety_checker.h.