Implement array literals as functions (see ArrayFunction, which has already been added to the model)
Implement constant ArrayFunctions for implicit default values and insert them into declarations using the ImplicitInitialValueInserter
Ensure that several ArrayFunction instances can reference the same ArrayFunction in their chainedFunction attribute
Whenever an array assignment occurs, i. e. WPStrategy::visit(Assignment) is called:
Instantiate a new ArrayFunction that maps the assignment index to the assignment value and any other index to the assignment array's initial value
Instantiate a new array type VariableDeclaration whose initial value is the just instantiated ArrayFunction
Replace all variable references in the weakest precondition by a reference to the just instantiated VariableDeclaration
Do not forget to recurse into the ArrayFunction chains referenced in the weakest precondition to replace VariableReferences which can occur both in the index and the value Expressions
ArrayFunction, which has already been added to the model)ArrayFunctions for implicit default values and insert them into declarations using theImplicitInitialValueInserterArrayFunctioninstances can reference the sameArrayFunctionin theirchainedFunctionattributeWPStrategy::visit(Assignment)is called:ArrayFunctionthat maps the assignment index to the assignment value and any other index to the assignment array's initial valueVariableDeclarationwhose initial value is the just instantiatedArrayFunctionVariableDeclarationArrayFunctionchains referenced in the weakest precondition to replaceVariableReferenceswhich can occur both in the index and the valueExpressions