simplification_check_stats Namespace Reference

How much check() actually decided, over every caller. More...

Functions
void	report ()

Variables
std::atomic< unsigned long >	proved {0}
std::atomic< unsigned long >	declined {0}
std::atomic< unsigned long >	ill_sorted {0}
	Of the declines, those whose before was already ill-sorted – a defect elsewhere in ESBMC rather than a limit of the check, so a nonzero count is something to go and look at.
std::atomic< unsigned long >	violations {0}
	Rewrites the check rejected.

Detailed Description

How much check() actually decided, over every caller.

Without this a run that declined every rewrite is indistinguishable from one that proved them all, which is the failure mode that would make the whole check worthless.

Function Documentation

report()

void simplification_check_stats::report

(

)

Variable Documentation

declined

std::atomic< unsigned long > simplification_check_stats::declined {0}

ill_sorted

std::atomic< unsigned long > simplification_check_stats::ill_sorted {0}

Of the declines, those whose before was already ill-sorted – a defect elsewhere in ESBMC rather than a limit of the check, so a nonzero count is something to go and look at.

proved

std::atomic< unsigned long > simplification_check_stats::proved {0}

violations

std::atomic< unsigned long > simplification_check_stats::violations {0}

Rewrites the check rejected.

Reported as they are found rather than on the first one, so a run surfaces the whole set (esbmc/esbmc#7326).