muen/kernel/src/sk-mp.adb:51:22: warning: loop range is null, loop will not execute
compilation of sk-mp.adb failed
gprbuild: *** compilation phase failed
make[1]: *** [/home/habeeb/muen5/muen/kernel/obj/debug/kernel] Error 4
make[1]: Leaving directory `/home/habeeb/muen5/muen/kernel'
make: *** [kernel] Error 2
kernel/src/sk-mp.adb
procedure Set_Minor_Frame_Barrier_Config
(Config : Skp.Scheduling.Barrier_Config_Array)
with
Refined_Global => (In_Out => Minor_Frame_Barriers),
Refined_Depends => (Minor_Frame_Barriers =>+ Config)
is
begin
for I in Config'Range loop
line 52 Barriers.Initialize (Barrier => Minor_Frame_Barriers (I),
Size => SK.Byte (Config (I)));
end loop;
end Set_Minor_Frame_Barrier_Config;
<scheduling tickRate="10000">
<majorFrame>
<cpu id="0">
<minorFrame barrier="none" subject="tau0" ticks="20"/>
<minorFrame barrier="none" subject="vt" ticks="50"/>
<minorFrame barrier="none" subject="nic_linux" ticks="50"/>
<minorFrame barrier="none" subject="storage_linux" ticks="50"/>
<minorFrame barrier="none" subject="time" ticks="10"/>
<minorFrame barrier="none" subject="dbgserver" ticks="30"/>
</cpu>
<barriers/>
</majorFrame>
</scheduling>
type Barrier_Index_Range is range 0 .. 0;
subtype Barrier_Range is
Barrier_Index_Range range 1 .. Barrier_Index_Range'Last;
type Barrier_Config_Array is array (Barrier_Range) of Barrier_Size_Type;
Thanks for the reply.
We are trying to verify the muen separation kernel.
we would like to start with a simpler (single CPU) system.
Is it possible to modify the code to work in single CPU system?
If you have such a code please share with us.
Thanking you
HABEEB P