test.adb 1.55 KB
Newer Older
1
2
with orchestrator;
with orchestrator_stop_conditions;
3
with asn1_iterators;
4
5
6
use  asn1_iterators;
with TASTE_BasicTypes;
use  TASTE_BasicTypes;
7
8
9
10
11

with ada.text_io;
use ada.text_io;

procedure test is
12
13
    count : natural := 0;

14
    function check(errno: out natural) return boolean is
15
        res : Boolean := false;
16
17
    begin
        errno := 0;
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
        res := orchestrator_stop_conditions.pproperty_0;
        count := count + 1;
        return res;
    end;

    procedure check_and_report is
        errno: Natural := 0;
    begin
        if check(errno) then
            put_line("Property " & errno'img & " is not verified");
        end if;
    end;

    procedure exhaust_pulse is
        pulse_it : T_Int_pkg.Instance;
        asn1_p   : aliased asn1SccT_Int;
    begin
        for each of pulse_it loop
            asn1_p := asn1SccT_Int'(asn1SccT_Int(each));
            orchestrator.pulse(asn1_p'access);
            check_and_report;
        end loop;
    end;

    procedure exhaust_arr is
        arr_it : T_SeqOf_pkg.Instance;
        asn1_p : aliased asn1SccT_SeqOf;
    begin
        for each of arr_it loop
            asn1_p.Length := each.Length;
            for idx in 1..asn1_p.Length loop
                asn1_p.Data(idx) := asn1SccT_Int'(asn1SccT_Int(each.Data(idx)));
            end loop;
            orchestrator.arr(asn1_p'access);
            check_and_report;
        end loop;
54
    end;
55
56
57
begin
    put_line("hello");
    orchestrator.startup;
58
59
60
61
    check_and_report;
    exhaust_pulse;
    exhaust_arr;
    put_line("Executed" & count'img & " functions");
62
end;