C++: Improve the SideEffect library QLDoc.

This commit is contained in:
Geoffrey White
2020-02-14 17:22:52 +00:00
parent c94582a1c0
commit 5f7085937e

View File

@@ -18,14 +18,18 @@ abstract class SideEffectFunction extends Function {
/**
* Holds if the function never reads from memory that was defined before entry to the function.
* This memory could be from global variables, or from other memory that was reachable from a
* pointer that was passed into the function.
* pointer that was passed into the function. Input side-effects, and reads from memory that
* cannot be visible to the caller (for example a buffer inside an I/O library) are not modelled
* here.
*/
abstract predicate hasOnlySpecificReadSideEffects();
/**
* Holds if the function never writes to memory that remains allocated after the function
* returns. This memory could be from global variables, or from other memory that was reachable
* from a pointer that was passed into the function.
* from a pointer that was passed into the function. Output side-effects, and writes to memory
* that cannot be visible to the caller (for example a buffer inside an I/O library) are not
* modelled here.
*/
abstract predicate hasOnlySpecificWriteSideEffects();