Skip to content
This repository has been archived by the owner on May 22, 2023. It is now read-only.

Commit

Permalink
prove rom test
Browse files Browse the repository at this point in the history
ref #80
  • Loading branch information
jklmnn committed Aug 27, 2019
1 parent 9f6fa1b commit aad2620
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 4 deletions.
8 changes: 6 additions & 2 deletions src/rom/client/muen/componolit-gneiss-rom-client.adb
Original file line number Diff line number Diff line change
Expand Up @@ -18,16 +18,20 @@ is
Rom_Name : constant Musinfo.Name_Type :=
(if Name = "" then CIM.String_To_Name ("config") else CIM.String_To_Name (Name));
begin
C.Mem := Musinfo.Instance.Memory_By_Name (Rom_Name);
if Musinfo.Instance.Is_Valid then
C.Mem := Musinfo.Instance.Memory_By_Name (Rom_Name);
end if;
end Initialize;

procedure Load (C : in out Client_Session)
is
use type Standard.Interfaces.Unsigned_64;
function Max_Index (Size : Standard.Interfaces.Unsigned_64) return Index is
(if Standard.Interfaces.Unsigned_64 (Index'Last) > Size then Index (Size) else Index'Last);
(if Standard.Interfaces.Unsigned_64 (Index'Last - Index'First) > Size
and then Standard.Interfaces.Unsigned_64 (Index'Last) <= Size then Index (Size) else Index'Last);
I : constant Index := Max_Index (C.Mem.Size / (Element'Size / 8));
B : Buffer (Index'First .. Index'First + I - 1) with
Import,
Address => System'To_Address (C.Mem.Address);
begin
Parse (B);
Expand Down
4 changes: 3 additions & 1 deletion src/rom/muen/componolit-gneiss-rom.adb
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@

with Musinfo;
with Musinfo.Instance;

package body Componolit.Gneiss.Rom with
SPARK_Mode
Expand All @@ -8,6 +9,7 @@ is
use type Musinfo.Memregion_Type;

function Initialized (C : Client_Session) return Boolean is
(C.Mem /= Musinfo.Null_Memregion);
(Musinfo.Instance.Is_Valid
and then C.Mem /= Musinfo.Null_Memregion);

end Componolit.Gneiss.Rom;
9 changes: 8 additions & 1 deletion test/rom/component.adb
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,19 @@ is
if not Componolit.Gneiss.Log.Initialized (Log) and then Data'Length > 1 then
for I in Data'Range loop
if Data (I) = ASCII.LF then
Last := I - 1;
if I > Data'First then
Last := I - 1;
else
Last := Data'First;
end if;
exit;
end if;
end loop;
Componolit.Gneiss.Log.Client.Initialize (Log, C, Data (Data'First .. Last));
if Componolit.Gneiss.Log.Initialized (Log) then
if Data (Data'First .. Last)'Length > Componolit.Gneiss.Log.Maximum_Message_Length (Log) - 35 then
Last := Data'First + (Componolit.Gneiss.Log.Maximum_Message_Length (Log) - 36);
end if;
Componolit.Gneiss.Log.Client.Info (Log, "Log session configured with label: "
& Data (Data'First .. Last));
else
Expand Down

0 comments on commit aad2620

Please sign in to comment.