CBMC
all_properties_verifier_with_fault_localization.h File Reference

Goto verifier for verifying all properties that stores traces and localizes faults. More...

+ Include dependency graph for all_properties_verifier_with_fault_localization.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >
 Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert. More...
 

Detailed Description

Goto verifier for verifying all properties that stores traces and localizes faults.

Definition in file all_properties_verifier_with_fault_localization.h.