Externals-C++STL.NonThrowingAllocator¶

User-provided summary of relevant effects of a function

This rule describes the effects of a function specifically for pointer/semantic analysis and several error checks. This can, for example, be used to tell the analysis about relevant effects of calls to the function if the function body itself is unknown to the analysis because it is only linked into the project as binary code and thus not seen during analysis (e.g. functions from third-party libraries that your project links against).

Possible Messages

This rule has no predefined messages.

Options¶

The following places define options that affect this rule: Analysis-GlobalOptions

exceptions¶

exceptions : None | bool | set[bauhaus.analysis.config.QualifiedName] = False

This option provides multiple options to specify exceptions possibly escaping the function.

If this option is None:
- Use what the declaration in source explicitly says
- If the declaration does not specify exceptions explicitly, then option StaticSemanticAnalysis/semantics.exceptions.missing_specifier_means_throw_any determines the effect:
  - either consider as noexcept(true) to accelerate analysis,
  - or refer to the language standard's definition of potentially-throwing and non-throwing functions
- Otherwise, if you set this option, you explicitly overwrite the source/language specification with either:
  - False, meaning no exception will escape (like noexcept(true))
  - True, meaning some exceptions may escape (like noexcept(false)); option StaticSemanticAnalysis/semantics.exceptions.base_class_for_throw_any can be used to improve the analysis by restricting the set of possibly escaping exception types
  - or an explicit set of type names that could escape (an empty set here has the same effect as throw() or noexcept(true))

frees¶

frees : int | None = None

Pointer targets of the parameter given here as index (starting with 0) are freed after a call to this function. The implicit this-parameter is also counted.

functions¶

functions

Type: set[bauhaus.analysis.config.GlobPattern]

Default: {'operator new(size_t, const std::nothrow_t&)', 'operator new(size_t, std::align_val_t, const std::nothrow_t&)', 'operator new(std::size_t, const std::nothrow_t&)', 'operator new(std::size_t, std::align_val_t, const std::nothrow_t&)', 'operator new(unsigned int, const std::nothrow_t&)', 'operator new(unsigned int, std::align_val_t, const std::nothrow_t&)', 'operator new(unsigned long long, const std::nothrow_t&)', 'operator new(unsigned long long, std::align_val_t, const std::nothrow_t&)', 'operator new(unsigned long, const std::nothrow_t&)', 'operator new(unsigned long, std::align_val_t, const std::nothrow_t&)', 'operator new[](size_t, const std::nothrow_t&)', 'operator new[](size_t, std::align_val_t, const std::nothrow_t&)', 'operator new[](std::size_t, const std::nothrow_t&)', 'operator new[](std::size_t, std::align_val_t, const std::nothrow_t&)', 'operator new[](unsigned int, const std::nothrow_t&)', 'operator new[](unsigned int, std::align_val_t, const std::nothrow_t&)', 'operator new[](unsigned long long, const std::nothrow_t&)', 'operator new[](unsigned long long, std::align_val_t, const std::nothrow_t&)', 'operator new[](unsigned long, const std::nothrow_t&)', 'operator new[](unsigned long, std::align_val_t, const std::nothrow_t&)'}

A set of names or globbing patterns of functions for which the summary applies

noreturn¶

noreturn : bool = False

Manual provision of a noreturn attribute if set to true. If false, reads from declaration attribute in source

post_conditions¶

post_conditions : set[str] = set()

Optional formulas expressing conditions holding after calling the function. Analyses can use this information to refine their results.

Formula Syntax

Terms that can be used in formulas:

Integers given in decimal notation like 0 or 42
Null pointer value, expressed by @null
Values of first, second, etc. function parameters are expressed by @param0, @param1, etc.
Return value of a call is expressed by @ret
Dereferencing parameters is expressed by *term, e.g. *@param0
Fields of memory objects are specified by ., e.g. @param0.field or (*@param1).field
To refer to the value of a memory access (like a parameter value) evaluated before the call, @pre can be used, e.g. @pre(@param0)
The predicate @alloc_with_size(pointer,size) specifies that a block of memory with size size in bytes at the location pointer will be allocated if the function returns.
For specifying the behaviour of operations dealing with smart pointers, the predicate @valid_ref can be used to express that a memory access (like a return value of an operation) is a smart pointer instance that can be dereferenced, e.g. @valid_ref(@ret)
For specifying the behaviour of operations dealing with iterators, the predicates @iterator_of resp. @end_iterator_of to express that a memory access (like a return value of an operation) is an iterator into a container resp. is an end iterator into a container (i.e., an iterator that is *not* safely dereferenceable). The first argument of the predicate is the iterator instance, the second refers to the container of the iterator, e.g. @end_iterator_of(@ret, *@param0) as condition for std::vector::end().
For expressing that two iterators or smart pointers point to the same element, the predicate @same_ref can be used, e.g. @same_ref(*@param0, *@param1)
The predicate @same_container(m1, m2) is true if the iterator instance m1 refers to the same container as m2. In contrast to @same_ref(m1, m2), @same_container(m1, m2) being true does not necessarily mean that arguments m1 and m2 refer to the same iterator value, i.e. to the same position within the container, but to positions within the same container. This is useful for representing effects of increment / decrement operators. E.g., @same_container(@pre(*@param0), @ret) is used to model the behaviour of post-decrement operators like operator++. Here @pre() is used to express that the iterator instance *@param0 before the call refers to the same instance as the return value @ret of the call.

Format of allowed formulae:

Arithmetic comparisons between parameters and constants: E.g. @param0 > 100, @param1 == 0, 1 != param. Only atomic types can be compared by ==, not structured type instances like struct or class instances (but see also @same_ref).
Null checks: E.g. @param0 == @null or *@param1 != @null
Predicates for boolean checks: @is_true(term) resp. @is_false(term) evaluate to true resp. false if the boolean term given as argument corresponds to true resp. false: e.g. @is_true(@ret)
Predicate to express that the function call does not return: @noret()
Combination of "or", "and", "implication", and "equivalence": E.g. @param0 == 1 || @param0 == 2, @param0 == 1 && @param1 != 0, @param0 == 0 ==> @noret(), @is_true(@ret) <-> ((*@param0)._Ptr == (*@param1)._Ptr)


Parentheses can be used to group formulas


A more complex example: if the first parameter is a null pointer and the field f of the dereferenced second parameter
contains a number greater 100, then the function does not return:

(@param0 == @null && (*@param1).f > 100) ==> @noret()

Specifying properties of smart pointer / iterator operations
In the following formulae examples for the special predicates
for smart pointers and iterators are given that can efficiently be processed and used by the corresponding
analysis. Use these as templates if you want to specify effects of operators acting on iterator / smart pointer instances.
You can adapt e.g. parameter indices to match the semantics.

@is_true(@ret) <-> @same_ref(*@param0, *@param1) resp. @is_true(@ret) <-> !@same_ref(*@param0, *@param1) for specifying
that the return value of the call is true if and only if the following holds:
the values to which the first and second parameter refer to (*@param0 and *@param1)
are the same reference or iterator value (resp. are not the same reference or iterator value).
Used for comparison operators like operator==() or operator!=().

@is_true(@ret) <-> @valid_ref(*@param0) resp. @is_true(@ret) <-> !@valid_ref(*@param0) for specifying
that the return value of the call is true if and only if the value the first parameter refers to (i.e., *@param0) can be safely dereferenced
(resp. cannot be safely dereferenced). Used e.g. for operator bool() or special comparisons against nullptr.

@iterator_of(@ret, *@param0) for specifying
that the return value of the call is an iterator of the container specified by *@param0.
 Used e.g. for find() operations.

@same_ref(@ret, @pre(*@param0)) for specifying
that @ret refers to the same memory location as the value of *param0 before
invoking the call. Here @ret often is an actual raw pointer. Used e.g. for operator->() or
operator*() of smart pointer types.

@same_container(@pre(*@param0), *@ret) for specifying
that *@ret is an iterator referencing the same container as @pre(*@param0), the value of *@param0
before executing the call. The variant
@same_container(@pre(*@param0), @ret) can be used if the operator does return by value (not in form of a reference to the iterator).
Used e.g. for increment/decrement operations on iterators (e.g. operator++(), operator--()).

*@param0 == @pre(*@param1) for specifying that *@param0 is assigned the value
of *@param1 before the call. Used e.g. for operator=() of smart pointer types.



pre_conditions¶
pre_conditions : set[str] = set()
Optional contract formulae expressing conditions that are expected to hold before
calling the function.  Used by
FaultDetection-InvalidArgumentInCall
to check validity of calls. See option
post_conditions for format of condition formulae.
For preconditions, currently only logical combinations of arithmetic comparisons
over parameters and integers are supported, e.g.

@param0 == 0 ||  @param1 == 0 || @param2 > 0

 

prepare_action¶
prepare_action : typing.Callable[[bauhaus.ir.Graph, bauhaus.ir.Node], NoneType] | None = None
Action executed before summary is evaluated.
 

return_value¶
return_value : bauhaus.ir.common.routines.external_summaries.ValueSummary = 'alloc'
Details regarding the possible return values. Terms that can be used:

  alloc: function is an allocator, returns a freshly created
      instance
  nonnull: return value is never nullptr
  null: return value can be nullptr
  integer literal: the function returns the given integer value
  [a:b] or a:b with integers a and
      b: the function returns an integer value within the bounds of
      the given interval
  name: the name of a variable of which the value is
      returned; you can also use *name for the dereferenced value, or
      &name for the address. To refer to a parameter, you can use the
      syntax param0 for the first, param1 for the
      second parameter, etc.

If you want to use multiple of these terms, specify the return value as
{ term1, ...., termN }.
 

writes¶
writes : dict[bauhaus.ir.common.routines.external_summaries.ObjectDescription, bauhaus.ir.common.routines.external_summaries.ValueSummary] | None = {}
Definition side-effects of the function: Objects/Access paths that are
modified, and possibly some details about the value of them.

  If writes has the value None, the rule does not
      specify side-effects, i.e., there are unknown/unspecified side-effects for
      the function.
  If writes is a non-empty dictionary, its entries specify the
      side-effects of the function completely.
  If writes is an empty dictionary, there are no write side-effects
      at all when calling the function.

Axivion Suite 7.12.0

Navigation

Externals-C++STL.NonThrowingAllocator¶

Options¶

exceptions¶

frees¶

functions¶

noreturn¶

post_conditions¶

Formula Syntax

Specifying properties of smart pointer / iterator operations

pre_conditions¶

prepare_action¶

return_value¶

writes¶