Missing test cases: - Store an array value, and make sure that the array elements are accessible directly using execution traces of type array index. - After copying an array value, it must still be possible to access array elements directly. - Writing a value to an existing execution trace must not fail. (Writing or marshaling a value twice could be a good enough test.)
Missing test cases: