Skip to content

GitLab

Commit c0f40a86 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Add test cases from ib krates

parent 89e3a3e9
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 3441 additions and 0 deletions
tests/regression/test-ibk/Makefile 0 → 100644
View file @ c0f40a86
include ../shared.mk
all: test-ada test-llvm
edit:
$(OPENGEODE) packetmanager.pr system_structure.pr
test-parse:
$(OPENGEODE) packetmanager.pr system_structure.pr --check
test-ada: packetmanager.ali
test-c: packetmanager.c
$(CC) -c packetmanager.c
test-llvm: packetmanager.o
coverage:
coverage run -p $(OPENGEODE) packetmanager.pr system_structure.pr --toAda
.PHONY: all edit test-parse test-ada test-llvm coverage
tests/regression/test-ibk/dataview-uniq.asn 0 → 100755
View file @ c0f40a86
TASTE-Dataview DEFINITIONS ::=
BEGIN
-- Boolean
MyBoolean ::= BOOLEAN
-- 4 bit array
My4BitArray ::= SEQUENCE (SIZE (4)) OF BOOLEAN
-- 8 bit array
My8BitArray ::= SEQUENCE (SIZE (8)) OF BOOLEAN
-- Integer for 8 bit array numbering
My8BitArrayInteger ::= INTEGER (0..7)
-- Integer for 8 bit array value numbering
My8BitArrayValueInteger ::= INTEGER (0..255)
-- 16 bit array
My16BitArray ::= SEQUENCE (SIZE (16)) OF BOOLEAN
-- Integer for 16 bit array numbering
My16BitArrayInteger ::= INTEGER (0..15)
-- Integer for 16 bit array value numbering
My16BitArrayValueInteger ::= INTEGER (0..65535)
-- Packet structure
MyPacket ::= SEQUENCE (SIZE (0..255)) OF MyFrame
-- Stack for data in bits
MyDataStack ::= SEQUENCE (SIZE (40..2000)) OF BOOLEAN
-- Stack for data of FCS calculation
MyFcsStack ::= SEQUENCE (SIZE (224..2192)) OF BOOLEAN -- Frame has empty info or is full
-- Integer for data of FCS calculation
MyFcsStackInteger ::= INTEGER (0..2175)
-- Polynomial for FCS calculation
MyFcsPolynomial ::= SEQUENCE (SIZE (17)) OF BOOLEAN
-- Integer for polynomial numbering
MyFcsPolynomialInteger ::= INTEGER (0..16)
-- Frame structure
MyFrame ::= SEQUENCE {
startFlag MyFlag,
addr MyAddr,
control MyControl,
pid MyPid,
info MyInfo,
fcs MyFcs,
endFlag MyFlag
}
-- FRAME: Frame delimiter
MyFlag ::= My8BitArray -- Fixed value 0x7E
-- FRAME: Source of frame and destination
MyAddr ::= SEQUENCE {
destinationAddress MyDestinationAddress,
sourceAddress MySourceAddress
}
-- ADDR: Destination address
MyDestinationAddress ::= SEQUENCE (SIZE (7)) OF My8BitArray
-- ADDR: Source address
MySourceAddress ::= SEQUENCE (SIZE (7)) OF My8BitArray
-- FRAME: Type of frame
MyControl ::= My8BitArray
-- FRAME: Protocol of info
MyPid ::= My8BitArray -- Fixed value 0xF0
-- FRAME: Info structure
MyInfo ::= SEQUENCE {
ba MyBa,
cntrl MyCntrl,
code MyCode,
operationData MyOperationData,
ifcs MyIfcs,
auth MyAuth OPTIONAL
}
-- INFO: Bus address
MyBa ::= SEQUENCE {
srcAddr MySrcAddr,
dstAddr MyDstAddr
}
-- BA: Source address
MySrcAddr ::= My4BitArray
-- BA: Destination address
MyDstAddr ::= My4BitArray
-- INFO: Control - frame type
MyCntrl ::= My8BitArray -- Fixed value 0x03
-- INFO: Code - operation
MyCode ::= My8BitArray
-- INFO: Operation data
MyOperationData ::= SEQUENCE (SIZE (0..250)) OF My8BitArray
-- INFO: Info Frame check sequence
MyIfcs ::= My16BitArray
-- INFO: Authentication
MyAuth ::= My16BitArray
-- FRAME: Frame check sequence
MyFcs ::= My16BitArray
-- Stack of L3 frames
MyL3Stack ::= SEQUENCE (SIZE (0..255)) OF MyL3Data
-- Stack of L3 frame numbers
MyL3StackNumbers ::= SEQUENCE (SIZE (0..255)) OF BOOLEAN
-- Integer for L3 frame stack numbering
MyL3StackInteger ::= INTEGER (0..254)
-- Stack of L3 missing frame numbers in octets
MyL3MissingStack ::= SEQUENCE (SIZE (0..255)) OF My8BitArray
-- Stack for L3 data in bits
MyL3DataStack ::= SEQUENCE (SIZE (0..1960)) OF BOOLEAN
-- Stack for data of L3 FCS calculation
MyL3FcsStack ::= SEQUENCE (SIZE (80..2040)) OF BOOLEAN -- L3 frame is empty or full
-- Integer for data of L3 FCS calculation
MyL3FcsStackInteger ::= INTEGER (0..2023)
-- Polynomial for L3 FCS calculation
MyL3FcsPolynomial ::= SEQUENCE (SIZE (17)) OF BOOLEAN
-- L3 frame structure
MyL3Frame ::= SEQUENCE {
l3Ba MyL3Ba,
l3Cntrl MyL3Cntrl,
l3Code MyL3Code,
l3Tte MyL3Tte,
l3Mrt MyL3Mrt,
l3Fnum MyL3Fnum,
l3Data MyL3Data,
l3Fcs MyL3Fcs
}
-- L3 FRAME: Bus address
MyL3Ba ::= SEQUENCE {
l3SrcAddr MyL3SrcAddr,
l3DstAddr MyL3DstAddr
}
-- L3BA: Source address
MyL3SrcAddr ::= My4BitArray
-- L3BA: Destination address
MyL3DstAddr ::= My4BitArray
-- L3 FRAME: Control - frame type
MyL3Cntrl ::= My8BitArray -- Fixed value 0x03
-- L3 FRAME: Code - data frame identificator
MyL3Code ::= My8BitArray
-- L3 FRAME: Time to end
MyL3Tte ::= My16BitArray
-- L3 FRAME: Maximum response time
MyL3Mrt ::= My16BitArray
-- L3 FRAME: Frame counter
MyL3Fnum ::= My8BitArray
-- L3 FRAME: Data
MyL3Data ::= SEQUENCE (SIZE (0..245)) OF My8BitArray
-- Integer for L3 data
MyL3DataInteger ::= INTEGER (0..244)
-- Stack for L3 acknowledgement data in bits
MyL3AckDataStack ::= SEQUENCE (SIZE (0..1952)) OF BOOLEAN
-- Stack for data of L3 acknowledgement FCS calculation
MyL3AckFcsStack ::= SEQUENCE (SIZE (88..2040)) OF BOOLEAN -- L3 acknowledgement frame is empty or full
-- Stack of L3 missing frame numbers
MyL3AckMissingStack ::= SEQUENCE (SIZE (0..244)) OF INTEGER (0..255)
-- Integer for stack of L3 missing frame stack numbering
MyL3AckMissingStackInteger ::= INTEGER (0..243)
-- L3 FRAME: Frame check sequence
MyL3Fcs ::= My16BitArray
-- L3 acknowledgement frame structure
MyL3AckFrame ::= SEQUENCE {
l3Ba MyL3Ba,
l3Cntrl MyL3Cntrl,
l3Code MyL3Code,
l3Tte MyL3Tte,
l3Mrt MyL3Mrt,
l3Lfn MyL3Lfn,
l3Hfn MyL3Hfn,
l3Rrq MyL3Rrq,
l3Fcs MyL3Fcs
}
-- L3 ACKNOWLEDGEMENT FRAME: Lowest sequential frame number
MyL3Lfn ::= My8BitArray
-- L3 ACKNOWLEDGEMENT FRAME: Highest frame sequence number
MyL3Hfn ::= My8BitArray
-- L3 ACKNOWLEDGEMENT FRAME: Frame numbers missing
MyL3Rrq ::= SEQUENCE (SIZE (0..244)) OF My8BitArray
-- Integer for L3 frame numbers missing
MyL3RrqInteger ::= INTEGER (0..243)
-- Input data structure
MyInputData ::= SEQUENCE {
ba MyBa,
code MyCode,
rawData MyRawData OPTIONAL,
l3Mrt MyL3Mrt OPTIONAL,
l3AckMissingStack MyL3AckMissingStack OPTIONAL
}
-- INPUT DATA: Raw data
MyRawData ::= SEQUENCE (SIZE (0..62475)) OF My8BitArray -- Up to 255 frames of data
-- Integer for raw data numbering
MyRawDataInteger ::= INTEGER (0..62475)
-- Acknowledgement data structure
MyAckData ::= SEQUENCE {
ba MyBa,
code MyCode,
l3Mrt MyL3Mrt,
l3Lfn MyL3Lfn,
l3Hfn MyL3Hfn,
l3MissingData MyL3MissingStack
}
END
TASTE-BasicTypes DEFINITIONS ::=
BEGIN
-- Set of TASTE predefined basic types
T-Int32 ::= INTEGER (-2147483648 .. 2147483647)
T-UInt32 ::= INTEGER (0 .. 4294967295)
T-Int8 ::= INTEGER (-128 .. 127)
T-UInt8 ::= INTEGER (0 .. 255)
T-Boolean ::= BOOLEAN
END
tests/regression/test-ibk/packetmanager.pr 0 → 100755
View file @ c0f40a86
/* CIF PROCESS (250, 150), (150, 75) */
PROCESS packetmanager;
STATE AGGREGATION wait;
SUBSTRUCTURE
STATE packetReceival;
SUBSTRUCTURE
/* CIF TEXT (673, 16), (357, 140) */
-- Text area for declarations and comments
DCL noOfSentPackets My8BitArrayValueInteger := 1;
/* CIF ENDTEXT */
/* CIF START (28, 0), (70, 35) */
START;
/* CIF NEXTSTATE (0, 58), (127, 35) */
NEXTSTATE frameReceival;
/* CIF STATE (345, 0), (127, 35) */
STATE frameReceival;
/* CIF INPUT (318, 55), (181, 35) */
INPUT ReceivePacket(packet);
/* CIF OUTPUT (287, 105), (244, 35) */
OUTPUT SendFrameCount(length(packet));
/* CIF LABEL (348, 155), (122, 54) */
frameSending:
/* CIF OUTPUT (264, 224), (290, 35) */
OUTPUT SendFrame(packet(noOfSentPackets - 1));
/* CIF DECISION (258, 274), (301, 50) */
DECISION length(packet) = noOfSentPackets;
/* CIF ANSWER (137, 344), (70, 23) */
(true):
/* CIF RETURN (155, 382), (35, 35) */
RETURN ;
/* CIF ANSWER (618, 344), (70, 23) */
(false):
/* CIF TASK (339, 382), (628, 35) */
TASK noOfSentPackets := if noOfsentPackets = 255 then noOfSentPackets else noOfSentPackets + 1 fi;
/* CIF JOIN (636, 432), (35, 35) */
JOIN frameSending;
ENDDECISION;
ENDSTATE;
ENDSUBSTRUCTURE;
STATE frameReceival;
SUBSTRUCTURE
/* CIF TEXT (1100, 14), (336, 140) */
-- Text area for declarations and comments
DCL frameCounter My8BitArrayValueInteger := 0;
/* CIF ENDTEXT */
/* CIF START (69, 0), (70, 35) */
START;
/* CIF NEXTSTATE (22, 50), (164, 35) */
NEXTSTATE frameCountReceival;
/* CIF STATE (270, 0), (164, 35) */
STATE frameCountReceival;
/* CIF INPUT (231, 55), (243, 35) */
INPUT ReceiveFrameCount(frameCount);
/* CIF NEXTSTATE (289, 105), (127, 35) */
NEXTSTATE frameReceival;
ENDSTATE;
/* CIF STATE (726, 0), (127, 35) */
STATE frameReceival;
/* CIF INPUT (695, 55), (189, 35) */
INPUT ReceiveFrame(frame);
/* CIF TASK (515, 105), (548, 38) */
TASK frameCounter := if frameCounter = 255 then frameCounter else frameCounter + 1 fi,
packet(frameCounter - 1) := frame;
/* CIF DECISION (675, 161), (229, 41) */
DECISION frameCounter = frameCount;
/* CIF ANSWER (631, 222), (70, 23) */
(true):
/* CIF OUTPUT (585, 260), (162, 35) */
OUTPUT SendPacket(packet);
/* CIF RETURN (648, 310), (35, 35) */
RETURN ;
/* CIF ANSWER (873, 222), (70, 23) */
(false):
/* CIF NEXTSTATE (844, 260), (127, 35) */
NEXTSTATE frameReceival;
ENDDECISION;
ENDSTATE;
ENDSUBSTRUCTURE;
/* CIF STATE (11, 0), (134, 35) */
STATE frameReceival;
ENDSTATE;
/* CIF STATE (0, 49), (159, 35) */
STATE packetReceival;
ENDSTATE;
ENDSUBSTRUCTURE;
/* CIF TEXT (328, 13), (300, 140) */
-- Text area for declarations and comments
DCL frameCount My8BitArrayValueInteger;
DCL frame MyFrame;
DCL packet MyPacket;
/* CIF ENDTEXT */
/* CIF START (49, 1), (70, 35) */
START;
/* CIF LABEL (49, 56), (70, 35) */
waiting:
/* CIF NEXTSTATE (49, 111), (70, 35) */
NEXTSTATE wait;
/* CIF STATE (175, 1), (70, 35) */
STATE wait;
ENDSTATE;
ENDPROCESS packetmanager;
\ No newline at end of file
tests/regression/test-ibk/system_structure.pr 0 → 100755
View file @ c0f40a86
/* CIF Keep Specific Geode ASNFilename 'dataview-uniq.asn' */
USE Datamodel;
SYSTEM packetmanager;
/* CIF Keep Specific Geode PARAMNAMES frame */
SIGNAL ReceiveFrame (MyFrame);
/* CIF Keep Specific Geode PARAMNAMES packet */
SIGNAL ReceivePacket (MyPacket);
/* CIF Keep Specific Geode PARAMNAMES frameCount */
SIGNAL ReceiveFrameCount (My8BitArrayValueInteger);
/* CIF Keep Specific Geode PARAMNAMES frame */
SIGNAL SendFrame (MyFrame);
/* CIF Keep Specific Geode PARAMNAMES packet */
SIGNAL SendPacket (MyPacket);
/* CIF Keep Specific Geode PARAMNAMES frameCount */
SIGNAL SendFrameCount (My8BitArrayValueInteger);
CHANNEL c
FROM ENV TO packetmanager WITH ReceiveFrame,ReceivePacket,ReceiveFrameCount;
FROM packetmanager TO ENV WITH SendFrame,SendPacket,SendFrameCount;
ENDCHANNEL;
BLOCK packetmanager;
SIGNALROUTE r
FROM ENV TO packetmanager WITH ReceiveFrame,ReceivePacket,ReceiveFrameCount;
FROM packetmanager TO ENV WITH SendFrame,SendPacket,SendFrameCount;
CONNECT c and r;
PROCESS packetmanager REFERENCED;
ENDBLOCK;
ENDSYSTEM;
\ No newline at end of file
tests/regression/test-ibk2/Makefile 0 → 100644
View file @ c0f40a86
include ../shared.mk
all: test-ada test-llvm
edit:
$(OPENGEODE) framemanager.pr system_structure.pr
test-parse:
$(OPENGEODE) framemanager.pr system_structure.pr --check
test-ada: framemanager.ali
test-c: framemanager.c
$(CC) -c framemanager.c
test-llvm: framemanager.o
coverage:
coverage run -p $(OPENGEODE) framemanager.pr system_structure.pr --toAda
.PHONY: all edit test-parse test-ada test-llvm coverage
tests/regression/test-ibk2/dataview-uniq.asn 0 → 100755
View file @ c0f40a86
TASTE-Dataview DEFINITIONS ::=
BEGIN
-- Boolean
MyBoolean ::= BOOLEAN
-- 4 bit array
My4BitArray ::= SEQUENCE (SIZE (4)) OF BOOLEAN
-- 8 bit array
My8BitArray ::= SEQUENCE (SIZE (8)) OF BOOLEAN
-- Integer for 8 bit array numbering
My8BitArrayInteger ::= INTEGER (0..7)
-- Integer for 8 bit array value numbering
My8BitArrayValueInteger ::= INTEGER (0..255)
-- 16 bit array
My16BitArray ::= SEQUENCE (SIZE (16)) OF BOOLEAN
-- Integer for 16 bit array numbering
My16BitArrayInteger ::= INTEGER (0..15)
-- Integer for 16 bit array value numbering
My16BitArrayValueInteger ::= INTEGER (0..65535)
-- Packet structure
MyPacket ::= SEQUENCE (SIZE (0..255)) OF MyFrame
-- Stack for data in bits
MyDataStack ::= SEQUENCE (SIZE (40..2000)) OF BOOLEAN
-- Stack for data of FCS calculation
MyFcsStack ::= SEQUENCE (SIZE (224..2192)) OF BOOLEAN -- Frame has empty info or is full
-- Integer for data of FCS calculation
MyFcsStackInteger ::= INTEGER (0..2175)
-- Polynomial for FCS calculation
MyFcsPolynomial ::= SEQUENCE (SIZE (17)) OF BOOLEAN
-- Integer for polynomial numbering
MyFcsPolynomialInteger ::= INTEGER (0..16)
-- Frame structure
MyFrame ::= SEQUENCE {
startFlag MyFlag,
addr MyAddr,
control MyControl,
pid MyPid,
info MyInfo,
fcs MyFcs,
endFlag MyFlag
}
-- FRAME: Frame delimiter
MyFlag ::= My8BitArray -- Fixed value 0x7E
-- FRAME: Source of frame and destination
MyAddr ::= SEQUENCE {
destinationAddress MyDestinationAddress,
sourceAddress MySourceAddress
}
-- ADDR: Destination address
MyDestinationAddress ::= SEQUENCE (SIZE (7)) OF My8BitArray
-- ADDR: Source address
MySourceAddress ::= SEQUENCE (SIZE (7)) OF My8BitArray
-- FRAME: Type of frame
MyControl ::= My8BitArray
-- FRAME: Protocol of info
MyPid ::= My8BitArray -- Fixed value 0xF0
-- FRAME: Info structure
MyInfo ::= SEQUENCE {
ba MyBa,
cntrl MyCntrl,
code MyCode,
operationData MyOperationData,
ifcs MyIfcs,
auth MyAuth OPTIONAL
}
-- INFO: Bus address
MyBa ::= SEQUENCE {
srcAddr MySrcAddr,
dstAddr MyDstAddr
}
-- BA: Source address
MySrcAddr ::= My4BitArray
-- BA: Destination address
MyDstAddr ::= My4BitArray
-- INFO: Control - frame type
MyCntrl ::= My8BitArray -- Fixed value 0x03
-- INFO: Code - operation
MyCode ::= My8BitArray
-- INFO: Operation data
MyOperationData ::= SEQUENCE (SIZE (0..250)) OF My8BitArray
-- INFO: Info Frame check sequence
MyIfcs ::= My16BitArray
-- INFO: Authentication
MyAuth ::= My16BitArray
-- FRAME: Frame check sequence
MyFcs ::= My16BitArray
-- Stack of L3 frames
MyL3Stack ::= SEQUENCE (SIZE (0..255)) OF MyL3Data
-- Stack of L3 frame numbers
MyL3StackNumbers ::= SEQUENCE (SIZE (0..255)) OF BOOLEAN
-- Integer for L3 frame stack numbering
MyL3StackInteger ::= INTEGER (0..254)
-- Stack of L3 missing frame numbers in octets
MyL3MissingStack ::= SEQUENCE (SIZE (0..255)) OF My8BitArray
-- Stack for L3 data in bits
MyL3DataStack ::= SEQUENCE (SIZE (0..1960)) OF BOOLEAN
-- Stack for data of L3 FCS calculation
MyL3FcsStack ::= SEQUENCE (SIZE (80..2040)) OF BOOLEAN -- L3 frame is empty or full
-- Integer for data of L3 FCS calculation
MyL3FcsStackInteger ::= INTEGER (0..2023)
-- Polynomial for L3 FCS calculation
MyL3FcsPolynomial ::= SEQUENCE (SIZE (17)) OF BOOLEAN
-- L3 frame structure
MyL3Frame ::= SEQUENCE {
l3Ba MyL3Ba,
l3Cntrl MyL3Cntrl,
l3Code MyL3Code,
l3Tte MyL3Tte,
l3Mrt MyL3Mrt,
l3Fnum MyL3Fnum,
l3Data MyL3Data,
l3Fcs MyL3Fcs
}
-- L3 FRAME: Bus address
MyL3Ba ::= SEQUENCE {
l3SrcAddr MyL3SrcAddr,
l3DstAddr MyL3DstAddr
}
-- L3BA: Source address
MyL3SrcAddr ::= My4BitArray
-- L3BA: Destination address
MyL3DstAddr ::= My4BitArray
-- L3 FRAME: Control - frame type
MyL3Cntrl ::= My8BitArray -- Fixed value 0x03
-- L3 FRAME: Code - data frame identificator
MyL3Code ::= My8BitArray
-- L3 FRAME: Time to end
MyL3Tte ::= My16BitArray