Commit 7c382840 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Cleanup test-iterators

based on taste-properties 1.1.3 and installed version of asn1-iterators
parent 4a4cc367
......@@ -14,11 +14,11 @@ test-parse:
$(OPENGEODE) orchestrator.pr --check
test-ada:
mkdir -p build && cp *.pr *.ad? iter_lib/* *.asn properties build && cd build && \
mkdir -p build && cp *.pr *.asn model_checker.gpr properties build && cd build && \
../../../../opengeode/opengeode.py orchestrator.pr --shared && \
$(ASN1SCC) -Ada dataview-uniq.asn -typePrefix asn1Scc -equal && \
taste-properties -d -s properties orchestrator.pr && \
gnat make model_checker -O2 && ./model_checker
taste-asn1-iterators *.asn && gprbuild -Pmodel_checker && ./model_checker
simu: test-ada
cd build && make -f Makefile.properties && \
......
-- This file was generated automatically by TASTE: DO NOT EDIT
package body ASN1_Iterators.iterators is
-- ASN.1 File dataview-uniq.asn
-- Module TASTE_BasicTypes
package body T_Int_pkg is
function Image(Elm: ASN1_Type) return String is (Elm'Img);
procedure To_ASN1(from: Interfaces.Integer_64; to: out ASN1_Type) is
begin
to := from;
end;
end;
package body T_SeqOf_pkg is
procedure To_ASN1(from: Inner.MySeqOf; to: out ASN1_Type) is
begin
for idx in 1..from.length loop
to.data(idx) := from.data(idx);
end loop;
to.length := from.length;
end;
function Image(Elm: ASN1_Type) return String is
function Image_rec(Elm: ASN1_Type) return String is
(if Elm.Length > 0 then
(Image(Elm.Data(1)) & (if Elm.Length > 1 then "," &
Image_Rec(ASN1_Type'(Length => Elm.Length-1,
Data => Elm.Data(2..Elm.Length) &
Elm.Data(1..Elm.Data'Length-Elm.Length+1)))
else ""))
else "");
begin
return "{" & Image_rec(Elm) & " }";
end;
end;
end;
\ No newline at end of file
-- This file was generated automatically by TASTE: DO NOT EDIT
-- Generic constructs for common/basic types
with generic_integer;
with generic_seqof;
with asn1_iterators;
pragma Unreferenced (asn1_iterators);
with Interfaces;
use Interfaces;
with Ada.Strings.Unbounded;
package ASN1_Iterators.iterators is
package Str renames Ada.Strings.Unbounded;
use Str;
-- ASN.1 File dataview-uniq.asn
-- Module TASTE_BasicTypes
-- List of exported types: "T-Int", "T-SeqOf"
-- Imported modules:
-- End imported modules --
-- Type "T-Int defined at line 4
package T_Int_pkg is
subtype ASN1_Type is asn1SccT_Int;
package Inner is new Generic_Integer (Min => 0, Max => 4);
package It renames Inner.It;
procedure To_ASN1(from: Interfaces.Integer_64; to: out ASN1_Type);
subtype Instance is Inner.Instance;
function Image(Elm: ASN1_Type) return String;
end;
-- Type "T-SeqOf defined at line 6
package T_SeqOf_pkg is
subtype ASN1_Type is asn1SccT_SeqOf;
package Inner is new Generic_SeqOf (Min => 1, Max => 4, Basic => T_Int_Pkg.It);
use T_Int_Pkg;
procedure To_ASN1(from: Inner.MySeqOf; to: out ASN1_Type);
subtype Instance is Inner.Instance;
function Image(Elm: ASN1_Type) return String;
end;
end;
\ No newline at end of file
-- This file was generated automatically by TASTE: DO NOT EDIT
-- Dummy package that is used to "with" the ASN.1 modules
-- ASN.1 File dataview-uniq.asn
with TASTE_BasicTypes;
use TASTE_BasicTypes;
pragma Unreferenced(TASTE_BasicTypes);
package ASN1_Iterators is
end;
\ No newline at end of file
package body Generic_Basic is
procedure Initialize (self: in out Basic_ASN1_Iterator) is
begin
--Self.Value := create;
Self.Value.Initialize;
end;
function First (Item : Iterator) return Iterator_Ptr is
begin
Item.Ptr.Value.First;
return Item.Ptr;
end;
function Next (Item : Iterator;
Ptr : Iterator_Ptr) return Iterator_Ptr is
pragma Unreferenced (Item);
begin
Ptr.Value.Next;
return Ptr;
end;
function Iterate (self : Basic_ASN1_Iterator)
return Forward_Iterator is
begin
return I: Iterator do
I.Ptr := self'Unrestricted_Access;
end return;
end;
end;
with Ada.Iterator_Interfaces;
with Ada.Finalization;
use Ada.Finalization;
with SimpleTypes;
generic
with package P is new SimpleTypes (<>);
package Generic_Basic is
-- Provides an iterator for a basic type
subtype Element is P.Element;
type Basic_ASN1_Iterator is new Controlled
with record
Value : P.SimpleType;
end record
with Default_Iterator => Iterate,
Iterator_Element => P.Element,
Constant_Indexing => Elem_Value;
procedure Initialize(self: in out Basic_ASN1_Iterator);
type Iterator_Ptr is access all Basic_ASN1_Iterator;
function Has_Element (Ptr : Iterator_Ptr) return Boolean is
(Ptr.Value.Has_Element);
package Iterators is
new Ada.Iterator_Interfaces (Iterator_Ptr, Has_Element);
type Iterator is new Iterators.Forward_Iterator with record
Ptr : Iterator_Ptr;
end record;
function Ptr (Item: Iterator) return Iterator_Ptr is (Item.Ptr);
overriding function First (Item : Iterator) return Iterator_Ptr;
overriding function Next (Item : Iterator;
Ptr : Iterator_Ptr) return Iterator_Ptr;
subtype Forward_Iterator is Iterators.Forward_Iterator'Class;
function Iterate (self : Basic_ASN1_Iterator) return Forward_Iterator;
function Elem_Value (self : Basic_ASN1_Iterator;
Ptr : Iterator_Ptr)
return P.Element is (Ptr.Value.Element_Value);
end;
with Ada.Unchecked_Conversion;
package body Generic_Fixed_SeqOf is
procedure Initialize (self: in out ASN1_SeqOf) is
begin
self.value.length := self.length;
if self.length > 1 then
self.Rest := new ASN1_SeqOf(self.Length - 1);
self.RestIt := new ASN1_SeqOf_It'(ASN1_SeqOf_It(self.Rest.Iterate));
self.RestIt.Ptr := self.RestIt.First;
end if;
end;
function Has_Element_SeqOf (Ptr: ASN1_SeqOf_Ptr) return Boolean is
(P.Has_Element(P.Ptr(Ptr.FirstIt)));
function Iterate (self : ASN1_SeqOf)
return Iterators_SeqOf.Forward_Iterator'Class is
begin
return I: ASN1_SeqOf_It do
I.Ptr := self'Unrestricted_Access;
end return;
end;
function First (Item : ASN1_SeqOf_It) return ASN1_SeqOf_Ptr is
Ptr_elem : P.Iterator_Ptr := P.Ptr(Item.Ptr.FirstIt);
begin
-- Initialize the iterator (Compute first value)
Item.Ptr.FirstIt := P.Iterator(Item.Ptr.FirstVal.Iterate);
Ptr_elem := P.First(Item.Ptr.FirstIt);
Item.Ptr.Value.Data(1) := P.Elem_Value(Item.Ptr.FirstVal,
Ptr_elem);
if Item.Ptr.Length > 1 then
Item.Ptr.Value.Data(2 .. Item.Ptr.Length) :=
Item.Ptr.RestIt.Ptr.Value.Data(1..Item.Ptr.RestIt.Ptr.Length);
end if;
return Item.Ptr;
end;
function Next (Item : ASN1_SeqOf_It;
Ptr : ASN1_SeqOf_Ptr) return ASN1_SeqOf_Ptr is
pragma Unreferenced (Item);
Ptr_elem : P.Iterator_Ptr := P.Ptr(Ptr.FirstIt);
begin
if Ptr.Length > 1 then
Ptr.RestIt.Ptr := Ptr.RestIt.Next (Ptr.RestIt.Ptr);
if Has_Element_SeqOf (Ptr.RestIt.Ptr) then
Ptr.Value.Data (2..Ptr.Length) :=
Ptr.RestIt.Ptr.Value.Data (1..Ptr.RestIt.Ptr.Value.Length);
else
Ptr.RestIt.Ptr := Ptr.RestIt.First;
-- Exhausted "rest": iterate on the first item
Ptr_elem := P.Next(Ptr.FirstIt, Ptr_elem);
if P.Has_Element (Ptr_elem) then
Ptr.Value.Data(1) := P.Elem_Value(Ptr.FirstVal, Ptr_elem);
Ptr.Value.Data(2..Ptr.Length) := Ptr.RestIt.Ptr.Value.Data (1..Ptr.RestIt.Ptr.Length);
end if;
end if;
else
-- Size is 0 or 1
Ptr_elem := P.Next(Ptr.FirstIt, Ptr_elem);
if P.Has_Element (Ptr_elem) then
Ptr.Value.Data(1) := P.Elem_Value(Ptr.FirstVal, Ptr_elem);
end if;
end if;
return Ptr;
end;
end;
with Ada.Iterator_Interfaces;
with Ada.Finalization;
use Ada.Finalization;
with generic_basic;
generic
with package P is new Generic_Basic (<>);
package Generic_Fixed_SeqOf is
type DataArray is array(natural range <>) of P.Element;
type SeqOf (Max: Natural) is record
Length : Integer;
Data : DataArray(1..Max);
end record;
type ASN1_SeqOf_Ptr;
type ASN1_SeqOf_It;
type ASN1_SeqOf (Size: Natural) is new Controlled
with record
Length : Natural := Size;
Value : SeqOf (Size);
-- First value
FirstVal : P.Basic_ASN1_Iterator;
FirstIt : P.Iterator;
-- The rest (recursive)
Rest : access ASN1_SeqOf;
RestIt : access ASN1_SeqOf_It;
end record
with Default_Iterator => Iterate,
Iterator_Element => SeqOf,
Constant_Indexing => Element_SeqOf_Value;
type ASN1_SeqOf_Ptr is access all ASN1_SeqOf;
-- Constructor (called automatically)
procedure Initialize(self: in out ASN1_SeqOf);
function Has_Element_SeqOf (Ptr : ASN1_SeqOf_Ptr) return Boolean;
package Iterators_SeqOf is
new Ada.Iterator_Interfaces (ASN1_SeqOf_Ptr, Has_Element_SeqOf);
type ASN1_SeqOf_It is new Iterators_SeqOf.Forward_Iterator with record
Ptr : ASN1_SeqOf_Ptr;
end record;
overriding function First (Item : ASN1_SeqOf_It) return ASN1_SeqOf_Ptr;
overriding function Next (Item : ASN1_SeqOf_It;
Ptr : ASN1_SeqOf_Ptr) return ASN1_SeqOf_Ptr;
function Iterate (self : ASN1_SeqOf)
return Iterators_SeqOf.Forward_Iterator'Class;
function Element_SeqOf_Value (self : ASN1_SeqOf;
Ptr : ASN1_SeqOf_Ptr)
return SeqOf is (self.Value);
end;
with SimpleTypes;
with Generic_Basic;
with Interfaces;
use Interfaces;
generic
Min: Interfaces.Integer_64;
Max: Interfaces.Integer_64;
package Generic_Integer is
function Elem_Init return Interfaces.Integer_64 is (Min);
function Has_Elem(Value: Interfaces.Integer_64) return Boolean is
(Value <= Max);
function Elem_First return Interfaces.Integer_64 is (Min);
function Elem_Next(Value: Interfaces.Integer_64) return Interfaces.Integer_64 is
(Value + 1);
package Integer_type is new SimpleTypes(Element => Interfaces.Integer_64,
Elem_Init => Elem_Init,
Has_Elem => Has_Elem,
Elem_First => Elem_First,
Elem_Next => Elem_Next);
package It is new Generic_Basic (P => Integer_type);
subtype Instance is It.Basic_ASN1_Iterator;
end;
package body Generic_SeqOf is
procedure Initialize (self: in out ASN1_Variable_SeqOf) is
begin
self.value.length := self.length;
if self.length >= 1 then
self.RestVal := new P.ASN1_SeqOf(Self.Length);
self.RestIt := new P.ASN1_SeqOf_It'(P.ASN1_SeqOf_It(Self.RestVal.Iterate));
self.RestIt.Ptr := self.RestIt.First;
end if;
end;
function Has_Element_Variable_SeqOf (Ptr: ASN1_Variable_SeqOf_Ptr)
return Boolean is (Length_Pkg.Has_Element(Length_Pkg.Ptr(Ptr.LenIt)));
function Iterate (self : ASN1_Variable_SeqOf)
return Iterators_Variable_SeqOf.Forward_Iterator'Class is
begin
return I: ASN1_Variable_SeqOf_It do
I.Ptr := Self'Unrestricted_Access;
end return;
end;
function First (Item : ASN1_Variable_SeqOf_It) return ASN1_Variable_SeqOf_Ptr is
begin
-- Initialize the iterator (Compute first value)
Item.Ptr.LenIt := Length_Pkg.Iterator(Item.Ptr.LenVal.Iterate);
--Item.Ptr.Value := Item.Ptr.RestIt.Ptr.Value;
-- Copy only the actual size, since the arrays may be different in size
Item.Ptr.Value.Data(1..Item.Ptr.RestIt.Ptr.Value.Data'Length) := Item.Ptr.RestIt.Ptr.Value.Data;
return Item.Ptr;
end;
function Next (Item : ASN1_Variable_SeqOf_It;
Ptr : ASN1_Variable_SeqOf_Ptr) return ASN1_Variable_SeqOf_Ptr is
pragma Unreferenced (Item);
Ptr_elem : Length_Pkg.Iterator_Ptr := Length_Pkg.Ptr(Ptr.LenIt);
begin
Ptr.RestIt.Ptr := Ptr.RestIt.Next (Ptr.RestIt.Ptr);
if P.Has_Element_SeqOf (Ptr.RestIt.Ptr) then
--Ptr.Value := Ptr.RestIt.Ptr.Value;
Ptr.Value.Data(1..Ptr.RestIt.Ptr.Value.Data'Length) := Ptr.RestIt.Ptr.Value.Data;
else
Ptr.RestIt.Ptr := Ptr.RestIt.First;
-- Exhausted "rest": iterate on the first item
Ptr_elem := Ptr.LenIt.Next(Ptr_elem);
if Length_Pkg.Has_Element (Ptr_elem) then
Ptr.Value.Length := Integer(Ptr_elem.Value.Value);
Ptr.Length := Ptr.Value.Length;
Ptr.RestVal := new P.ASN1_SeqOf(Ptr.Value.Length);
Ptr.RestIt := new P.ASN1_SeqOf_It'(P.ASN1_SeqOf_It(Ptr.RestVal.Iterate));
Ptr.RestIt.Ptr := Ptr.RestIt.First;
--Ptr.Value := Ptr.RestIt.Ptr.Value;
Ptr.Value.Data(1..Ptr.RestIt.Ptr.Value.Data'Length) := Ptr.RestIt.Ptr.Value.Data;
end if;
end if;
return Ptr;
end;
end;
with Ada.Iterator_Interfaces;
with Ada.Finalization;
use Ada.Finalization;
with generic_fixed_seqof;
with generic_integer;
with generic_basic;
with Interfaces;
use Interfaces;
-- Iterator for a variable-size array of basic type
generic
Min : Natural;
Max : Natural;
with package Basic is new Generic_Basic (<>);
package Generic_SeqOf is
Package P is new Generic_Fixed_SeqOF (P => Basic);
-- Create an integer type with a range constraint to iterate on
package Length_ty is new Generic_Integer (Integer_64(Min),
Integer_64(Max));
-- Instantiate the package to iterate on the integer for the length
package Length_Pkg renames Length_ty.It;
type ASN1_Variable_SeqOf_Ptr is private;
subtype MySeqOf is P.SeqOf(Max);
type ASN1_Variable_SeqOf is new Controlled
with record
Length : Natural := Min;
Value : MySeqOf; -- P.SeqOf(Max);
-- Iterate on the length
LenVal : Length_ty.Instance;
LenIt : Length_Pkg.Iterator;
-- And on the value
RestVal : access P.ASN1_SeqOf;
RestIt : access P.ASN1_SeqOf_It;
end record
with Default_Iterator => Iterate,
Iterator_Element => MySeqOf, --P.SeqOf,
Constant_Indexing => Element_Variable_SeqOf_Value;
-- Constructor (called automatically)
procedure Initialize(self: in out ASN1_Variable_SeqOf);
function Has_Element_Variable_SeqOf (Ptr : ASN1_Variable_SeqOf_Ptr)
return Boolean;
package Iterators_Variable_SeqOf is
new Ada.Iterator_Interfaces (ASN1_Variable_SeqOf_Ptr,
Has_Element_Variable_SeqOf);
type ASN1_Variable_SeqOf_It
is new Iterators_Variable_SeqOf.Forward_Iterator with record
Ptr : ASN1_Variable_SeqOf_Ptr;
end record;
overriding
function First (Item : ASN1_Variable_SeqOf_It)
return ASN1_Variable_SeqOf_Ptr;
overriding
function Next (Item : ASN1_Variable_SeqOf_It;
Ptr : ASN1_Variable_SeqOf_Ptr)
return ASN1_Variable_SeqOf_Ptr;
function Iterate (self : ASN1_Variable_SeqOf)
return Iterators_Variable_SeqOf.Forward_Iterator'Class;
function Element_Variable_SeqOf_Value (Self : ASN1_Variable_SeqOf;
Ptr : ASN1_Variable_SeqOf_Ptr)
--return P.SeqOf is (Self.Value);
return MySeqOf is (Self.Value);
subtype Instance is ASN1_Variable_SeqOf;
private
type ASN1_Variable_SeqOf_Ptr is access all ASN1_Variable_SeqOf;
end;
package body SimpleTypes is
procedure Initialize (Self : in out SimpleType) is
begin
Self.Value := Elem_Init;
end;
procedure First (Self : in out SimpleType) is
begin
Self.Value := Elem_First;
end;
procedure Next (Self : in out SimpleType) is
begin
Self.Value := Elem_Next (Self.Value);
end;
end;
generic
type Element is private;
with function Elem_Init return Element;
with function Has_Elem (Value: Element) return Boolean;
with function Elem_First return Element;
with function Elem_Next (Value: Element) return Element;
package SimpleTypes is
type SimpleType is tagged
record
Value: Element;
end record;
procedure Initialize (Self : in out SimpleType);
function Has_Element (Self : in out SimpleType) return Boolean is
(Has_Elem (Self.Value));
procedure First (Self : in out SimpleType);
procedure Next (Self : in out SimpleType);
function Element_Value (Self : in out SimpleType) return Element is
(Self.Value);
end;
with orchestrator;
use orchestrator;
with orchestrator_stop_conditions;
with asn1_iterators.iterators;
use asn1_iterators.iterators;
with TASTE_BasicTypes;
use TASTE_BasicTypes;
with Ada.Text_IO;
use Ada.Text_IO;
with GNAT.MD5;
with Ada.Streams;
use Ada.Streams;
with Ada.Unchecked_Conversion;
with System;
with Ada.Strings.Hash;
with Ada.Containers.Ordered_Maps;
with Ada.Containers.Ordered_Sets;
with Ada.Containers.Vectors;
use Ada.Containers;
with Ada.Calendar;
use Ada.Calendar;
procedure model_checker is
subtype Context_ty is orchestrator_ctxt_ty;
Process_Ctxt : Context_ty renames orchestrator_Ctxt;
-- To save/restore the context when calling a PI:
backup_ctxt : Context_ty;
backup_hash : Hash_Type;
start_hash : Hash_Type;