Miscellaneous warnings reported by GNATprove -------------------------------------------- The following table shows default warnings reported by GNATprove outside of flow analysis and proof. .. tabularcolumns:: |p{2in}|p{3in}| .. csv-table:: :header: "Warning Tag", "Explanation" :widths: 2, 4 "address-to-access-conversion", "call to conversion function is assumed to return a valid access designating a valid value" "alias-volatile-atomic-mismatch", "aliased objects should both be volatile or non-volatile, and both be atomic or non-atomic" "alias-volatile-prop-mismatch", "aliased objects should have the same volatile properties" "attribute-valid-always-true", "attribute Valid or Valid_Scalars is assumed to return True" "auto-lemma-calls", "the automatically instantiated lemma contains calls which cannot be arbitrarily specialized" "auto-lemma-different", "the automatically instantiated lemma contains calls to its associated function with different specializations" "auto-lemma-higher-order", "the automatically instantiated lemma is not annotated with Higher_Order_Specialization" "auto-lemma-specializable", "the automatically instantiated lemma does not contain any specializable calls to its associated function" "initialization-to-alias", "initialization of object is assumed to have no effects on other non-volatile objects" "is-valid-returns-true", "function Is_Valid is assumed to return True" "generic-not-analyzed", "GNATprove doesn't analyze generics, only instances" "no-possible-termination", "procedure which does not return normally nor raises an exception cannot always terminate" "potentially-invalid-read", "invalid data might be read in the contract of a subprogram without an analyzed body; the fact that the read data is valid is not checked by SPARK" "no-check-message-justified", "no check message justified by this pragma" "proved-check-justified", "only proved check messages justified by this pragma" "deprecated-terminating", "Terminating, Always_Return, and Might_Not_Return annotations are ignored" "deprecated-external-axiomatization", "External Axiomatizations are not supported anymore, ignored" "ignored-pragma", "pragma is ignored (it is not yet supported)" "overflow-mode-ignored", "pragma Overflow_Mode in code is ignored" "precondition-statically-false", "precondition is statically False" "restriction-ignored", "restriction is ignored (it is not yet supported)" "unreferenced-function", "analyzing unreferenced function" "unreferenced-procedure", "analyzing unreferenced procedure" "useless-potentially-invalid-func-result", "function result annotated with Potentially_Invalid cannot have invalid values" "useless-potentially-invalid-object", "object annotated with Potentially_Invalid cannot have invalid values" "useless-relaxed-init-func-result", "function result annotated with Relaxed_Initialization cannot be partially initialized" "useless-relaxed-init-object", "object annotated with Relaxed_Initialization cannot be partially initialized" "variant-no-recursion", "no recursive call visible on subprogram with Subprogram_Variant" The following table shows warnings guaranteed to be reported by GNATprove. .. tabularcolumns:: |p{2in}|p{3in}| .. csv-table:: :header: "Warning Tag", "Explanation" :widths: 2, 4 "assumed-always-terminates", "no Always_Terminates aspect available for subprogram, subprogram is assumed to always terminate" "assumed-global-null", "no Global contract available for subprogram, null is assumed" "imprecise-address-specification", "object with an imprecisely supported address specification: non-atomic objects should not be accessed concurrently, volatile properties should be correct, indirect writes to object to and through potential aliases are ignored, and reads should be valid" The following warnings are disabled by default, and can be enabled collectively using switch ``--pedantic``, or individually using switch ``-W``. .. tabularcolumns:: |p{2in}|p{3in}| .. csv-table:: :header: "Warning Tag", "Explanation" :widths: 2, 4 "image-attribute-length", "string attribute has an implementation-defined length" "operator-reassociation", "possible operator reassociation due to missing parentheses" "representation-attribute-value", "representation attribute has an implementation-defined value" The following warnings are disabled by default, and can be enabled collectively using switch ``--info``, or individually using switch ``-W``. .. tabularcolumns:: |p{2in}|p{3in}| .. csv-table:: :header: "Warning Tag", "Explanation" :widths: 2, 4 "component-relaxed-init", "If all components of a given type are annotated with Relaxed_Initialization, the containing type is treated as if it had the same annotation" "full-view-visible", "The full view of an incomplete type deferred to the body of a withed unit might be visible by GNATprove" "alias-array", "Aliasing checks might be spurious for actual parameters that are array components" "imprecise-global-generation", "Global generation might wrongly classify an Output item as an In_Out for subprograms that call other subprograms with no Global contract" "array-initialization", "Initialization of arrays inside FOR loops is only recognized when assignments to array element are directly indexed by the loopparameter" "multidimensional-array-init", "Initialization of multi-dimensional array inside FOR loops is only recognized when array bounds are static" "tagged-assignment", "Assignments to record objects might cause spurious data dependencies in some components of the assigned object" "contracts-recursive", "Explicit and implicit postconditions of a recursive subprogram cannot be used on (mutually) recursive calls occurring inside assertions and contracts, but will still be available in regular code" "dic-ignored", "The Default_Initial_Condition of a type won't be assumed on subcomponents initialized by default inside assertions and contracts, but will still be available in regular code" "imprecise-address", "The adress of objects is not precisely known if it is not supplied through an address clause" "imprecise-align", "The alignment of an object might not be known for proof if it is not supplied through an attribute definition clause" "imprecise-call", "The behavior of a call might not be known by SPARK and handled in an imprecise way; its precondition might be impossible to prove and nothing will be known about its result" "imprecise-component-size", "the value of attribute Component_Size might not be known for proof if it is not supplied through an attribute definition clause" "imprecise-record-component-attribute", "the value of attributes First_Bit, Last_Bit, and Position on record components are handled in an imprecise way if the record does not have a record representation clause" "imprecise-size", "The attributes Size, Object_Size or Value_Size might not be handled precisely, nothing will be known about their evaluation" "imprecise-unchecked-conversion", "Unchecked conversion might not be handled precisely by SPARK, nothing will be known about their result" "imprecise-value", "References to the attribute Value are handled in an imprecise way; its precondition is impossible to prove and nothing will be known about the evaluation of the attribute reference" "imprecise-image", "References to the attributes Image and Img are handled in an imprecise way; nothing will be known about the evaluation of the attribute reference apart from a bound on its length" "constants-in-loops", "The initial value of constants declared before the loop invariant is not visible after the invariant; it shall be restated in the invariant if necessary" "no-reclamation-function", "No reclamation function or reclaimed value was found for an ownership type, which may make it impossible to prove that values of this type are reclaimed" "numeric-variant", "For recursive expression functions with a numeric (not structural) Subprogram_Variant, the definition of the expression function might not be available for recursive calls occurring inside assertions and contracts, but will still be available in regular code" "relaxed-mutable-discriminants", "The tool enforces that mutable discriminants of standalone objects and parameters with relaxed initialization are always initialized" "map-length-aggregates", "A type with predefined map aggregates doesn't have a Length function; the length of aggregates will not be known for this type" "set-length-aggregates", "A type with predefined set aggregates doesn't have a Length function; the length of aggregates will not be known for this type" "predefined-equality-null", "A type is annotated with Only_Null as value for the Predefined_Equality annotation, but no constant annotated with Null_Value is found; this will result in all calls to the predefined equality being rejected" "init-cond-ignored", "The initial condition of a withed package might be ignored if it is not known to be true, due to elaboration order" "unit-not-spark", "A unit whose analysis has been requested on the command-line is not annotated with SPARK_Mode Pragma" The following info messages are issued by default, and can be disabled using switch ``-A``. .. tabularcolumns:: |p{2in}|p{3in}| .. csv-table:: :header: "Warning Tag", "Explanation" :widths: 2, 4 "info-unrolling-inlining", "These messages are issued when the tool is unrolling loops or inlining subprograms, or unable to do so"