mc-imperial / spirv-control-flow

Formal modelling of SPIR-V control flow using Alloy
Apache License 2.0
3 stars 0 forks source link

Incorporating structured-reachability #43

Open vili-1 opened 3 years ago

vili-1 commented 3 years ago

This Vulkan CTS graph contains unreachable nodes - b4 is unreachable (not even structured-reachable). Prompted by this, we agreed that Alloy model should require that every block is structured-reachable (a simplifying assumption on top of the structured-dominance).

struct-reach