lala::IDiagnostics Class Reference

#include <diagnostics.hpp>

Public Types
using	allocator_type = battery::standard_allocator
using	F = TFormula< allocator_type >
using	this_type = IDiagnostics

Public Member Functions
CUDA NI	IDiagnostics ()
template<class F2 >
CUDA NI	IDiagnostics (bool fatal, battery::string< allocator_type > ad_name, battery::string< allocator_type > description, const F2 &uninterpretable_formula, AType aty=UNTYPED)
CUDA NI this_type &	add_suberror (IDiagnostics &&suberror)
CUDA size_t	num_suberrors () const
CUDA void	cut (size_t i)
CUDA void	merge (bool succeeded, size_t i)
CUDA NI void	print (int indent=0) const
CUDA bool	is_fatal () const
CUDA bool	has_warning () const

Detailed Description

IDiagnostics is used in abstract domains to diagnose why a formula cannot be interpreted (error) or if it was interpreted by under- or over-approximation (warnings). If the abstract domain cannot interpret the formula, it must explain why. This is similar to compilation errors in compiler.

Member Typedef Documentation

allocator_type

using lala::IDiagnostics::allocator_type = battery::standard_allocator

F

using lala::IDiagnostics::F = TFormula<allocator_type>

this_type

using lala::IDiagnostics::this_type = IDiagnostics

Constructor & Destructor Documentation

IDiagnostics() [1/2]

CUDA NI lala::IDiagnostics::IDiagnostics ( )

inline

IDiagnostics() [2/2]

template<class F2 >

CUDA NI lala::IDiagnostics::IDiagnostics ( bool  fatal, battery::string< allocator_type >  ad_name, battery::string< allocator_type >  description, const F2 &  uninterpretable_formula, AType  aty = UNTYPED  )

inline

Member Function Documentation

add_suberror()

CUDA NI this_type & lala::IDiagnostics::add_suberror ( IDiagnostics &&  suberror )

inline

num_suberrors()

CUDA size_t lala::IDiagnostics::num_suberrors ( ) const

inline

cut()

CUDA void lala::IDiagnostics::cut ( size_t  i )

inline

Deletes all suberrors between i and n-1.

merge()

CUDA void lala::IDiagnostics::merge ( bool  succeeded, size_t  i  )

inline

This operator moves all suberrors[i..(n-1)] as a suberror of suberrors[i-1]. If only warnings are present, suberrors[i-1] is converted into a warning. If succeeded is true, then all suberrors are erased.

print()

CUDA NI void lala::IDiagnostics::print ( int  indent = 0 ) const

inline

is_fatal()

CUDA bool lala::IDiagnostics::is_fatal ( ) const

inline

has_warning()

CUDA bool lala::IDiagnostics::has_warning ( ) const

inline

---

The documentation for this class was generated from the following file:

• include/lala/logic/diagnostics.hpp