mirror of
https://github.com/AdaCore/spark2014.git
synced 2026-02-12 12:39:11 -08:00
01c95a1abb
We agreed that it is safer for volatile variables (or state abstractions) with Async_Writers to be explicitly initialized (or imported), despite SPARK RM 7.1.2(14) didn't require them to be initialized. [changelog] * docs/lrm/source/packages.rst (External State): Remove rule 7.1.2(14); renumber subsequent rules. * src/flow/flow-control_flow_graph-utility.adb (Make_Variable_Attribute): Remove implementation of the mentioned rule. * testsuite/gnatprove/tests/932__flow_async_import/test.out New check on a volatile variable with no explicit initialization.