__ASTREE_asynchronous_loop. An additional directive
__ASTREE_shared_variableallows the explicit specification of shared variables. Shared variables can also be detected automatically during the analysis when the option
automatic-shared-variablesis enabled. Finally, the list of automatically detected shared variables can be reported by enabling the option
enumtypes can now be configured in the ABI. It can either be
sizeof(int)or the size of the smallest possible integer type that can hold all
enumvalues. The latter may be chosen either among signed integers only or among signed and unsigned integers.
cut-invalid-pointercontrols whether or not the analyzer stops on computations with invalid pointers. With
cut-invalid-pointers=no, the analyzer continues assuming that the result of such an operation is again an invalid pointer. Read accesses to invalid pointers are assumed to return unknown values whereas write accesses are treated as
The output of analyses with version number ≤ 6 can no longer be displayed by release 13.10. When converting such analyses to a more recent analysis, old analysis results are deleted. To prevent data loss, we recommend exporting all analyses with version number ≤ 6 using an older release of Astrée.
__ASTREE_partition_control) in log and report files. These directives appear right after the list of semantic hypotheses in the output.
astree.cfg) that end with a comment.
__ASTREE_global_assertdirectives can now be written as constant expressions, including hexadecimal and binary values.
insert afterannotations, or to create annotations with a minimal distance of lines between annotation target and the original position of the directive.