The bug visitor will walk all the nodes in a path and collect all the constraints. More...
#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
Classes | |
| struct | Z3Result |
Public Member Functions | |
| Z3CrosscheckVisitor (Z3CrosscheckVisitor::Z3Result &Result, const AnalyzerOptions &Opts) | |
| void | Profile (llvm::FoldingSetNodeID &ID) const override |
| PathDiagnosticPieceRef | VisitNode (const ExplodedNode *N, BugReporterContext &BRC, PathSensitiveBugReport &BR) override |
| Return a diagnostic piece which should be associated with the given node. | |
| void | finalizeVisitor (BugReporterContext &BRC, const ExplodedNode *EndPathNode, PathSensitiveBugReport &BR) override |
| Last function called on the visitor, no further calls to VisitNode would follow. | |
| Public Member Functions inherited from clang::ento::BugReporterVisitor | |
| BugReporterVisitor ()=default | |
| BugReporterVisitor (const BugReporterVisitor &)=default | |
| BugReporterVisitor (BugReporterVisitor &&) | |
| BugReporterVisitor & | operator= (const BugReporterVisitor &)=delete |
| BugReporterVisitor & | operator= (BugReporterVisitor &&)=delete |
| virtual | ~BugReporterVisitor () |
| virtual PathDiagnosticPieceRef | getEndPath (BugReporterContext &BRC, const ExplodedNode *N, PathSensitiveBugReport &BR) |
| Provide custom definition for the final diagnostic piece on the path - the piece, which is displayed before the path is expanded. | |
Additional Inherited Members | |
| Static Public Member Functions inherited from clang::ento::BugReporterVisitor | |
| static PathDiagnosticPieceRef | getDefaultEndPath (const BugReporterContext &BRC, const ExplodedNode *N, const PathSensitiveBugReport &BR) |
| Generates the default final diagnostic piece. | |
Detailed Description
The bug visitor will walk all the nodes in a path and collect all the constraints.
When it reaches the root node, will create a refutation manager and check if the constraints are satisfiable.
Definition at line 24 of file Z3CrosscheckVisitor.h.
Constructor & Destructor Documentation
◆ Z3CrosscheckVisitor()
| Z3CrosscheckVisitor::Z3CrosscheckVisitor | ( | Z3CrosscheckVisitor::Z3Result & | Result, |
| const AnalyzerOptions & | Opts ) |
Definition at line 52 of file Z3CrosscheckVisitor.cpp.
Member Function Documentation
◆ finalizeVisitor()
|
overridevirtual |
Last function called on the visitor, no further calls to VisitNode would follow.
Reimplemented from clang::ento::BugReporterVisitor.
Definition at line 57 of file Z3CrosscheckVisitor.cpp.
References clang::ento::BugReporterContext::getASTContext(), and clang::ento::SMTConv::getRangeExpr().
◆ Profile()
|
overridevirtual |
Implements clang::ento::BugReporterVisitor.
Definition at line 144 of file Z3CrosscheckVisitor.cpp.
◆ VisitNode()
|
overridevirtual |
Return a diagnostic piece which should be associated with the given node.
Note that this function does not get run on the very last node of the report, as the PathDiagnosticPiece associated with the last node should be unique. Use getEndPath to customize the note associated with the report end instead.
The last parameter can be used to register a new visitor with the given BugReport while processing a node.
Implements clang::ento::BugReporterVisitor.
Definition at line 138 of file Z3CrosscheckVisitor.cpp.
The documentation for this class was generated from the following files:
- include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
- lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
Generated on for clang by
1.14.0