508 lines
24 KiB
Plaintext
508 lines
24 KiB
Plaintext
(***********************************************************************************
|
|
* Copyright (c) 2016-2020 The University of Sheffield, UK
|
|
* 2019-2020 University of Exeter, UK
|
|
*
|
|
* All rights reserved.
|
|
*
|
|
* Redistribution and use in source and binary forms, with or without
|
|
* modification, are permitted provided that the following conditions are met:
|
|
*
|
|
* * Redistributions of source code must retain the above copyright notice, this
|
|
* list of conditions and the following disclaimer.
|
|
*
|
|
* * Redistributions in binary form must reproduce the above copyright notice,
|
|
* this list of conditions and the following disclaimer in the documentation
|
|
* and/or other materials provided with the distribution.
|
|
*
|
|
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
|
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
|
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
|
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
|
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
|
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
|
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
|
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
|
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
|
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|
*
|
|
* SPDX-License-Identifier: BSD-2-Clause
|
|
***********************************************************************************)
|
|
|
|
(* This file is automatically generated, please do not modify! *)
|
|
|
|
section\<open>Testing slots\_fallback\<close>
|
|
text\<open>This theory contains the test cases for slots\_fallback.\<close>
|
|
|
|
theory slots_fallback
|
|
imports
|
|
"Shadow_DOM_BaseTest"
|
|
begin
|
|
|
|
definition slots_fallback_heap :: "heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l" where
|
|
"slots_fallback_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])),
|
|
(cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 8)] fmempty None)),
|
|
(cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6), cast (element_ptr.Ref 7)] fmempty None)),
|
|
(cast (element_ptr.Ref 3), cast (create_element_obj ''title'' [cast (character_data_ptr.Ref 1)] fmempty None)),
|
|
(cast (character_data_ptr.Ref 1), cast (create_character_data_obj ''Shadow%20DOM%3A%20Slots%20and%20fallback%20contents'')),
|
|
(cast (element_ptr.Ref 4), cast (create_element_obj ''meta'' [] (fmap_of_list [(''name'', ''author''), (''title'', ''Hayato Ito''), (''href'', ''mailto:hayato@google.com'')]) None)),
|
|
(cast (element_ptr.Ref 5), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''/resources/testharness.js'')]) None)),
|
|
(cast (element_ptr.Ref 6), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''/resources/testharnessreport.js'')]) None)),
|
|
(cast (element_ptr.Ref 7), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''resources/shadow-dom.js'')]) None)),
|
|
(cast (element_ptr.Ref 8), cast (create_element_obj ''body'' [cast (element_ptr.Ref 9), cast (element_ptr.Ref 13), cast (element_ptr.Ref 14), cast (element_ptr.Ref 19), cast (element_ptr.Ref 20), cast (element_ptr.Ref 26), cast (element_ptr.Ref 27), cast (element_ptr.Ref 33), cast (element_ptr.Ref 34), cast (element_ptr.Ref 46)] fmempty None)),
|
|
(cast (element_ptr.Ref 9), cast (create_element_obj ''div'' [cast (element_ptr.Ref 10)] (fmap_of_list [(''id'', ''test1'')]) None)),
|
|
(cast (element_ptr.Ref 10), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 1))))),
|
|
(cast (shadow_root_ptr.Ref 1), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 11)])),
|
|
(cast (element_ptr.Ref 11), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 12)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
|
|
(cast (element_ptr.Ref 12), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
|
|
(cast (element_ptr.Ref 13), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 2)] fmempty None)),
|
|
(cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
|
|
(cast (element_ptr.Ref 14), cast (create_element_obj ''div'' [cast (element_ptr.Ref 15)] (fmap_of_list [(''id'', ''test2'')]) None)),
|
|
(cast (element_ptr.Ref 15), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 2))))),
|
|
(cast (shadow_root_ptr.Ref 2), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 16)])),
|
|
(cast (element_ptr.Ref 16), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 17)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
|
|
(cast (element_ptr.Ref 17), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 18)] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
|
|
(cast (element_ptr.Ref 18), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
|
|
(cast (element_ptr.Ref 19), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 3)] fmempty None)),
|
|
(cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
|
|
(cast (element_ptr.Ref 20), cast (create_element_obj ''div'' [cast (element_ptr.Ref 21)] (fmap_of_list [(''id'', ''test3'')]) None)),
|
|
(cast (element_ptr.Ref 21), cast (create_element_obj ''div'' [cast (element_ptr.Ref 22)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 3))))),
|
|
(cast (element_ptr.Ref 22), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
|
|
(cast (shadow_root_ptr.Ref 3), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 23)])),
|
|
(cast (element_ptr.Ref 23), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 24)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
|
|
(cast (element_ptr.Ref 24), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 25)] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
|
|
(cast (element_ptr.Ref 25), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
|
|
(cast (element_ptr.Ref 26), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 4)] fmempty None)),
|
|
(cast (character_data_ptr.Ref 4), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
|
|
(cast (element_ptr.Ref 27), cast (create_element_obj ''div'' [cast (element_ptr.Ref 28)] (fmap_of_list [(''id'', ''test4'')]) None)),
|
|
(cast (element_ptr.Ref 28), cast (create_element_obj ''div'' [cast (element_ptr.Ref 29)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 4))))),
|
|
(cast (element_ptr.Ref 29), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot2'')]) None)),
|
|
(cast (shadow_root_ptr.Ref 4), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 30)])),
|
|
(cast (element_ptr.Ref 30), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 31)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
|
|
(cast (element_ptr.Ref 31), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 32)] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
|
|
(cast (element_ptr.Ref 32), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
|
|
(cast (element_ptr.Ref 33), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 5)] fmempty None)),
|
|
(cast (character_data_ptr.Ref 5), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
|
|
(cast (element_ptr.Ref 34), cast (create_element_obj ''div'' [cast (element_ptr.Ref 35)] (fmap_of_list [(''id'', ''test5'')]) None)),
|
|
(cast (element_ptr.Ref 35), cast (create_element_obj ''div'' [cast (element_ptr.Ref 36)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 5))))),
|
|
(cast (element_ptr.Ref 36), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
|
|
(cast (shadow_root_ptr.Ref 5), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 37)])),
|
|
(cast (element_ptr.Ref 37), cast (create_element_obj ''div'' [cast (element_ptr.Ref 38)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 6))))),
|
|
(cast (element_ptr.Ref 38), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 39), cast (element_ptr.Ref 41)] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2''), (''slot'', ''slot3'')]) None)),
|
|
(cast (element_ptr.Ref 39), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 40)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
|
|
(cast (element_ptr.Ref 40), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
|
|
(cast (element_ptr.Ref 41), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f2'')]) None)),
|
|
(cast (shadow_root_ptr.Ref 6), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 42)])),
|
|
(cast (element_ptr.Ref 42), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 43), cast (element_ptr.Ref 45)] (fmap_of_list [(''id'', ''s4''), (''name'', ''slot4'')]) None)),
|
|
(cast (element_ptr.Ref 43), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 44)] (fmap_of_list [(''id'', ''s3''), (''name'', ''slot3'')]) None)),
|
|
(cast (element_ptr.Ref 44), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f3'')]) None)),
|
|
(cast (element_ptr.Ref 45), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f4'')]) None)),
|
|
(cast (element_ptr.Ref 46), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 6)] fmempty None)),
|
|
(cast (character_data_ptr.Ref 6), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
|
|
|
definition slots_fallback_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "slots_fallback_document = Some (cast (document_ptr.Ref 1))"
|
|
|
|
|
|
text \<open>'Slots fallback: Basic.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test1'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test1'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
tmp2 \<leftarrow> n . ''f1'';
|
|
tmp3 \<leftarrow> tmp2 . assignedSlot;
|
|
assert_equals(tmp3, None);
|
|
tmp4 \<leftarrow> n . ''s1'';
|
|
tmp5 \<leftarrow> tmp4 . assignedNodes();
|
|
assert_array_equals(tmp5, []);
|
|
tmp6 \<leftarrow> n . ''s1'';
|
|
tmp7 \<leftarrow> tmp6 . assignedNodes(True);
|
|
tmp8 \<leftarrow> n . ''f1'';
|
|
assert_array_equals(tmp7, [tmp8])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Basic, elements only.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test1'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''s1'';
|
|
tmp2 \<leftarrow> tmp1 . assignedElements();
|
|
assert_array_equals(tmp2, []);
|
|
tmp3 \<leftarrow> n . ''s1'';
|
|
tmp4 \<leftarrow> tmp3 . assignedElements(True);
|
|
tmp5 \<leftarrow> n . ''f1'';
|
|
assert_array_equals(tmp4, [tmp5])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Slots in Slots.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test2'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test2'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
tmp2 \<leftarrow> n . ''f1'';
|
|
tmp3 \<leftarrow> tmp2 . assignedSlot;
|
|
assert_equals(tmp3, None);
|
|
tmp4 \<leftarrow> n . ''s1'';
|
|
tmp5 \<leftarrow> tmp4 . assignedNodes();
|
|
assert_array_equals(tmp5, []);
|
|
tmp6 \<leftarrow> n . ''s2'';
|
|
tmp7 \<leftarrow> tmp6 . assignedNodes();
|
|
assert_array_equals(tmp7, []);
|
|
tmp8 \<leftarrow> n . ''s1'';
|
|
tmp9 \<leftarrow> tmp8 . assignedNodes(True);
|
|
tmp10 \<leftarrow> n . ''f1'';
|
|
assert_array_equals(tmp9, [tmp10]);
|
|
tmp11 \<leftarrow> n . ''s2'';
|
|
tmp12 \<leftarrow> tmp11 . assignedNodes(True);
|
|
tmp13 \<leftarrow> n . ''f1'';
|
|
assert_array_equals(tmp12, [tmp13])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Slots in Slots, elements only.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test2'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''s1'';
|
|
tmp2 \<leftarrow> tmp1 . assignedElements();
|
|
assert_array_equals(tmp2, []);
|
|
tmp3 \<leftarrow> n . ''s2'';
|
|
tmp4 \<leftarrow> tmp3 . assignedElements();
|
|
assert_array_equals(tmp4, []);
|
|
tmp5 \<leftarrow> n . ''s1'';
|
|
tmp6 \<leftarrow> tmp5 . assignedElements(True);
|
|
tmp7 \<leftarrow> n . ''f1'';
|
|
assert_array_equals(tmp6, [tmp7]);
|
|
tmp8 \<leftarrow> n . ''s2'';
|
|
tmp9 \<leftarrow> tmp8 . assignedElements(True);
|
|
tmp10 \<leftarrow> n . ''f1'';
|
|
assert_array_equals(tmp9, [tmp10])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Fallback contents should not be used if a node is assigned.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test3'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test3'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
tmp2 \<leftarrow> n . ''c1'';
|
|
tmp3 \<leftarrow> tmp2 . assignedSlot;
|
|
tmp4 \<leftarrow> n . ''s1'';
|
|
assert_equals(tmp3, tmp4);
|
|
tmp5 \<leftarrow> n . ''f1'';
|
|
tmp6 \<leftarrow> tmp5 . assignedSlot;
|
|
assert_equals(tmp6, None);
|
|
tmp7 \<leftarrow> n . ''s1'';
|
|
tmp8 \<leftarrow> tmp7 . assignedNodes();
|
|
tmp9 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp8, [tmp9]);
|
|
tmp10 \<leftarrow> n . ''s2'';
|
|
tmp11 \<leftarrow> tmp10 . assignedNodes();
|
|
assert_array_equals(tmp11, []);
|
|
tmp12 \<leftarrow> n . ''s1'';
|
|
tmp13 \<leftarrow> tmp12 . assignedNodes(True);
|
|
tmp14 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp13, [tmp14]);
|
|
tmp15 \<leftarrow> n . ''s2'';
|
|
tmp16 \<leftarrow> tmp15 . assignedNodes(True);
|
|
tmp17 \<leftarrow> n . ''f1'';
|
|
assert_array_equals(tmp16, [tmp17])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Slots in Slots: Assigned nodes should be used as fallback contents of another slot'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test4'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test4'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
tmp2 \<leftarrow> n . ''c1'';
|
|
tmp3 \<leftarrow> tmp2 . assignedSlot;
|
|
tmp4 \<leftarrow> n . ''s2'';
|
|
assert_equals(tmp3, tmp4);
|
|
tmp5 \<leftarrow> n . ''f1'';
|
|
tmp6 \<leftarrow> tmp5 . assignedSlot;
|
|
assert_equals(tmp6, None);
|
|
tmp7 \<leftarrow> n . ''s1'';
|
|
tmp8 \<leftarrow> tmp7 . assignedNodes();
|
|
assert_array_equals(tmp8, []);
|
|
tmp9 \<leftarrow> n . ''s2'';
|
|
tmp10 \<leftarrow> tmp9 . assignedNodes();
|
|
tmp11 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp10, [tmp11]);
|
|
tmp12 \<leftarrow> n . ''s1'';
|
|
tmp13 \<leftarrow> tmp12 . assignedNodes(True);
|
|
tmp14 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp13, [tmp14]);
|
|
tmp15 \<leftarrow> n . ''s2'';
|
|
tmp16 \<leftarrow> tmp15 . assignedNodes(True);
|
|
tmp17 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp16, [tmp17])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Complex case.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test5'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test5'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
tmp2 \<leftarrow> n . ''s1'';
|
|
tmp3 \<leftarrow> tmp2 . assignedNodes();
|
|
tmp4 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp3, [tmp4]);
|
|
tmp5 \<leftarrow> n . ''s2'';
|
|
tmp6 \<leftarrow> tmp5 . assignedNodes();
|
|
assert_array_equals(tmp6, []);
|
|
tmp7 \<leftarrow> n . ''s3'';
|
|
tmp8 \<leftarrow> tmp7 . assignedNodes();
|
|
tmp9 \<leftarrow> n . ''s2'';
|
|
assert_array_equals(tmp8, [tmp9]);
|
|
tmp10 \<leftarrow> n . ''s4'';
|
|
tmp11 \<leftarrow> tmp10 . assignedNodes();
|
|
assert_array_equals(tmp11, []);
|
|
tmp12 \<leftarrow> n . ''s1'';
|
|
tmp13 \<leftarrow> tmp12 . assignedNodes(True);
|
|
tmp14 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp13, [tmp14]);
|
|
tmp15 \<leftarrow> n . ''s2'';
|
|
tmp16 \<leftarrow> tmp15 . assignedNodes(True);
|
|
tmp17 \<leftarrow> n . ''c1'';
|
|
tmp18 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp16, [tmp17, tmp18]);
|
|
tmp19 \<leftarrow> n . ''s3'';
|
|
tmp20 \<leftarrow> tmp19 . assignedNodes(True);
|
|
tmp21 \<leftarrow> n . ''c1'';
|
|
tmp22 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp20, [tmp21, tmp22]);
|
|
tmp23 \<leftarrow> n . ''s4'';
|
|
tmp24 \<leftarrow> tmp23 . assignedNodes(True);
|
|
tmp25 \<leftarrow> n . ''c1'';
|
|
tmp26 \<leftarrow> n . ''f2'';
|
|
tmp27 \<leftarrow> n . ''f4'';
|
|
assert_array_equals(tmp24, [tmp25, tmp26, tmp27])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Complex case, elements only.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test5'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''s1'';
|
|
tmp2 \<leftarrow> tmp1 . assignedElements();
|
|
tmp3 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp2, [tmp3]);
|
|
tmp4 \<leftarrow> n . ''s2'';
|
|
tmp5 \<leftarrow> tmp4 . assignedElements();
|
|
assert_array_equals(tmp5, []);
|
|
tmp6 \<leftarrow> n . ''s3'';
|
|
tmp7 \<leftarrow> tmp6 . assignedElements();
|
|
tmp8 \<leftarrow> n . ''s2'';
|
|
assert_array_equals(tmp7, [tmp8]);
|
|
tmp9 \<leftarrow> n . ''s4'';
|
|
tmp10 \<leftarrow> tmp9 . assignedElements();
|
|
assert_array_equals(tmp10, []);
|
|
tmp11 \<leftarrow> n . ''s1'';
|
|
tmp12 \<leftarrow> tmp11 . assignedElements(True);
|
|
tmp13 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp12, [tmp13]);
|
|
tmp14 \<leftarrow> n . ''s2'';
|
|
tmp15 \<leftarrow> tmp14 . assignedElements(True);
|
|
tmp16 \<leftarrow> n . ''c1'';
|
|
tmp17 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp15, [tmp16, tmp17]);
|
|
tmp18 \<leftarrow> n . ''s3'';
|
|
tmp19 \<leftarrow> tmp18 . assignedElements(True);
|
|
tmp20 \<leftarrow> n . ''c1'';
|
|
tmp21 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp19, [tmp20, tmp21]);
|
|
tmp22 \<leftarrow> n . ''s4'';
|
|
tmp23 \<leftarrow> tmp22 . assignedElements(True);
|
|
tmp24 \<leftarrow> n . ''c1'';
|
|
tmp25 \<leftarrow> n . ''f2'';
|
|
tmp26 \<leftarrow> n . ''f4'';
|
|
assert_array_equals(tmp23, [tmp24, tmp25, tmp26])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Mutation. Append fallback contents.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test5'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test5'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
d1 \<leftarrow> slots_fallback_document . createElement(''div'');
|
|
tmp2 \<leftarrow> n . ''s2'';
|
|
tmp2 . appendChild(d1);
|
|
tmp3 \<leftarrow> n . ''s1'';
|
|
tmp4 \<leftarrow> tmp3 . assignedNodes(True);
|
|
tmp5 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp4, [tmp5]);
|
|
tmp6 \<leftarrow> n . ''s2'';
|
|
tmp7 \<leftarrow> tmp6 . assignedNodes(True);
|
|
tmp8 \<leftarrow> n . ''c1'';
|
|
tmp9 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp7, [tmp8, tmp9, d1]);
|
|
tmp10 \<leftarrow> n . ''s3'';
|
|
tmp11 \<leftarrow> tmp10 . assignedNodes(True);
|
|
tmp12 \<leftarrow> n . ''c1'';
|
|
tmp13 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp11, [tmp12, tmp13, d1]);
|
|
tmp14 \<leftarrow> n . ''s4'';
|
|
tmp15 \<leftarrow> tmp14 . assignedNodes(True);
|
|
tmp16 \<leftarrow> n . ''c1'';
|
|
tmp17 \<leftarrow> n . ''f2'';
|
|
tmp18 \<leftarrow> n . ''f4'';
|
|
assert_array_equals(tmp15, [tmp16, tmp17, d1, tmp18])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Mutation. Remove fallback contents.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test5'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test5'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
tmp2 \<leftarrow> n . ''f2'';
|
|
tmp2 . remove();
|
|
tmp3 \<leftarrow> n . ''s1'';
|
|
tmp4 \<leftarrow> tmp3 . assignedNodes(True);
|
|
tmp5 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp4, [tmp5]);
|
|
tmp6 \<leftarrow> n . ''s2'';
|
|
tmp7 \<leftarrow> tmp6 . assignedNodes(True);
|
|
tmp8 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp7, [tmp8]);
|
|
tmp9 \<leftarrow> n . ''s3'';
|
|
tmp10 \<leftarrow> tmp9 . assignedNodes(True);
|
|
tmp11 \<leftarrow> n . ''c1'';
|
|
assert_array_equals(tmp10, [tmp11]);
|
|
tmp12 \<leftarrow> n . ''s4'';
|
|
tmp13 \<leftarrow> tmp12 . assignedNodes(True);
|
|
tmp14 \<leftarrow> n . ''c1'';
|
|
tmp15 \<leftarrow> n . ''f4'';
|
|
assert_array_equals(tmp13, [tmp14, tmp15])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Mutation. Assign a node to a slot so that fallback contens are no longer used.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test5'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test5'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
d2 \<leftarrow> slots_fallback_document . createElement(''div'');
|
|
d2 . setAttribute(''slot'', ''slot2'');
|
|
tmp2 \<leftarrow> n . ''host1'';
|
|
tmp2 . appendChild(d2);
|
|
tmp3 \<leftarrow> n . ''s2'';
|
|
tmp4 \<leftarrow> tmp3 . assignedNodes();
|
|
assert_array_equals(tmp4, [d2]);
|
|
tmp5 \<leftarrow> n . ''s2'';
|
|
tmp6 \<leftarrow> tmp5 . assignedNodes(True);
|
|
assert_array_equals(tmp6, [d2]);
|
|
tmp7 \<leftarrow> n . ''s3'';
|
|
tmp8 \<leftarrow> tmp7 . assignedNodes(True);
|
|
assert_array_equals(tmp8, [d2]);
|
|
tmp9 \<leftarrow> n . ''s4'';
|
|
tmp10 \<leftarrow> tmp9 . assignedNodes(True);
|
|
tmp11 \<leftarrow> n . ''f4'';
|
|
assert_array_equals(tmp10, [d2, tmp11])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Mutation. Remove an assigned node from a slot so that fallback contens will be used.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test5'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test5'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
tmp2 \<leftarrow> n . ''c1'';
|
|
tmp2 . remove();
|
|
tmp3 \<leftarrow> n . ''s1'';
|
|
tmp4 \<leftarrow> tmp3 . assignedNodes();
|
|
assert_array_equals(tmp4, []);
|
|
tmp5 \<leftarrow> n . ''s1'';
|
|
tmp6 \<leftarrow> tmp5 . assignedNodes(True);
|
|
tmp7 \<leftarrow> n . ''f1'';
|
|
assert_array_equals(tmp6, [tmp7]);
|
|
tmp8 \<leftarrow> n . ''s2'';
|
|
tmp9 \<leftarrow> tmp8 . assignedNodes(True);
|
|
tmp10 \<leftarrow> n . ''f1'';
|
|
tmp11 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp9, [tmp10, tmp11]);
|
|
tmp12 \<leftarrow> n . ''s3'';
|
|
tmp13 \<leftarrow> tmp12 . assignedNodes(True);
|
|
tmp14 \<leftarrow> n . ''f1'';
|
|
tmp15 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp13, [tmp14, tmp15]);
|
|
tmp16 \<leftarrow> n . ''s4'';
|
|
tmp17 \<leftarrow> tmp16 . assignedNodes(True);
|
|
tmp18 \<leftarrow> n . ''f1'';
|
|
tmp19 \<leftarrow> n . ''f2'';
|
|
tmp20 \<leftarrow> n . ''f4'';
|
|
assert_array_equals(tmp17, [tmp18, tmp19, tmp20])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
text \<open>'Slots fallback: Mutation. Remove a slot which is a fallback content of another slot.'\<close>
|
|
|
|
lemma "test (do {
|
|
tmp0 \<leftarrow> slots_fallback_document . getElementById(''test5'');
|
|
n \<leftarrow> createTestTree(tmp0);
|
|
tmp1 \<leftarrow> n . ''test5'';
|
|
removeWhiteSpaceOnlyTextNodes(tmp1);
|
|
tmp2 \<leftarrow> n . ''s1'';
|
|
tmp2 . remove();
|
|
tmp3 \<leftarrow> n . ''s1'';
|
|
tmp4 \<leftarrow> tmp3 . assignedNodes();
|
|
assert_array_equals(tmp4, []);
|
|
tmp5 \<leftarrow> n . ''s1'';
|
|
tmp6 \<leftarrow> tmp5 . assignedNodes(True);
|
|
assert_array_equals(tmp6, [], ''fall back contents should be empty because s1 is not in a shadow tree.'');
|
|
tmp7 \<leftarrow> n . ''s2'';
|
|
tmp8 \<leftarrow> tmp7 . assignedNodes(True);
|
|
tmp9 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp8, [tmp9]);
|
|
tmp10 \<leftarrow> n . ''s3'';
|
|
tmp11 \<leftarrow> tmp10 . assignedNodes(True);
|
|
tmp12 \<leftarrow> n . ''f2'';
|
|
assert_array_equals(tmp11, [tmp12]);
|
|
tmp13 \<leftarrow> n . ''s4'';
|
|
tmp14 \<leftarrow> tmp13 . assignedNodes(True);
|
|
tmp15 \<leftarrow> n . ''f2'';
|
|
tmp16 \<leftarrow> n . ''f4'';
|
|
assert_array_equals(tmp14, [tmp15, tmp16])
|
|
}) slots_fallback_heap"
|
|
by eval
|
|
|
|
|
|
end
|