1package Sync2 with 2 SPARK_Mode, 3 Abstract_State => (State with Synchronous) 4is 5 pragma Elaborate_Body; 6end Sync2; 7