Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add manual section on RLC inference #6340

Merged
merged 16 commits into from
Jan 28, 2024
Merged
21 changes: 11 additions & 10 deletions docs/manual/resource-leak-checker.tex
Original file line number Diff line number Diff line change
Expand Up @@ -632,16 +632,17 @@
then verify the code using a method other than the Resource Leak Checker.


%% TODO: Uncomment when the feature is ready to be publicized.
% \sectionAndLabel{Resource Leak Checker Annotation Inference Algorithm}{resource-leak-checker-inference-algo}
%
% We are developing a special inference mechanism to infer annotations for
% the Resource Leak Checker. By default, this mechanism operates when the
% -Ainfer flag is enabled. To utilize the whole-program inference mechanism outlined in
% section \ref{whole-program-inference} in addition to this mechanism for the Resource
% Leak Checker and its sub-checkers, you should provide the \<-AenableWpiForRlc> flag.
%
% The paper \href={https://arxiv.org/pdf/2306.11953.pdf}{Automatic Inference of Resource Leak Specifications}, published at OOPSLA 2023, gives more details on the inference algorithm. Currently, only the first phase of the algorithm described in the paper is available, and the complete implementation will be available soon.
\sectionAndLabel{Resource Leak Checker Annotation Inference Algorithm}{resource-leak-checker-inference-algo}

We have developed a specialized algorithm to infer annotations for
the Resource Leak Checker. This algorithm runs by default when the
\<-Ainfer> flag is enabled. To utilize the whole-program inference mechanism outlined in
msridhar marked this conversation as resolved.
Show resolved Hide resolved
section \ref{whole-program-inference} in addition to this mechanism for the Resource
Leak Checker and its sub-checkers, you should provide the \<-AenableWpiForRlc> flag. The paper
msridhar marked this conversation as resolved.
Show resolved Hide resolved
``Inference of Resource Management Specifications''~\cite{ShadabGTEKLLS2023} (OOPSLA 2023,
\myurl{https://homes.cs.washington.edu/~mernst/pubs/resource-inference-oopsla2023-abstract.html})
gives more details about the inference algorithm.



% LocalWords: de subchecker OutputStream MustCall MustCallUnknown RAII Un
Expand Down