#include <java_multi_path_symex_checker.h>
+ Inheritance diagram for java_multi_path_symex_checkert:
+ Collaboration diagram for java_multi_path_symex_checkert:
Builds and returns the complete trace.
Builds and returns the trace for the FAILed property with the given property_id.
Builds and returns the trace up to the first failed property.
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by
incremental_goto_checkert hold.
Builds and returns the complete trace.
Builds and returns the trace up to the first failed property.
Builds and returns the trace for the FAILed property with the given property_id.
Returns the namespace associated with the traces.
Returns the most likely fault locations for the given FAILed property_id.
Additional reporting that may result from the underlying solver, no-op by default.
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by
incremental_goto_checkert hold.
Additional Inherited Members
Prepare the property decider for solving.
Run the property decider, which calls the SAT solver, and set the status of checked properties accordingly.
Generates the equation by running goto-symex.
Updates the properties from the equation and adds their property IDs to updated_properties.
Detailed Description
Constructor & Destructor Documentation
◆ java_multi_path_symex_checkert()
java_multi_path_symex_checkert::java_multi_path_symex_checkert
(
const optionst &
options,
)
inline
Member Function Documentation
◆ build_full_trace()
goto_tracet java_multi_path_symex_checkert::build_full_trace
(
)
const
overridevirtual
◆ build_shortest_trace()
goto_tracet java_multi_path_symex_checkert::build_shortest_trace
(
)
const
overridevirtual
◆ build_trace()
The documentation for this class was generated from the following files:
