Skip to content

Commit

Permalink
Templates updated.
Browse files Browse the repository at this point in the history
  • Loading branch information
@Jellix
Jellix committed Jul 15, 2020
1 parent 226096c commit a942ad4
Show file tree
Hide file tree
Showing 65 changed files with 13,558 additions and 423 deletions.
3 changes: 2 additions & 1 deletion test/spat.test-issues.g.template
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ Warning: This feature is highly experimental.
Warning: Please consult the documentation.

package Prove is
for Proof_Switches ("rflx-rflx_types.ads") use ("--prover=altergo,CVC4,Z3", "--steps=94470", "--timeout=55");
for Proof_Switches ("rflx-arrays-tests.adb") use ("--prover=Z3", "--steps=1768", "--timeout=1");
for Proof_Switches ("rflx-rflx_types.ads") use ("--prover=altergo,CVC4,Z3", "--steps=99104", "--timeout=55");
end Prove;

47 changes: 34 additions & 13 deletions test/spat.test-issues.raca.template
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,34 @@
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
RFLX.Arrays.Tests.Name => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Register_Tests => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671 => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_First => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_Last => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Valid_Data_Length => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Write_Data => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
47 changes: 34 additions & 13 deletions test/spat.test-issues.racs.template
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,34 @@
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
RFLX.Arrays.Tests.Name => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Register_Tests => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671 => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_First => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_Last => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Valid_Data_Length => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Write_Data => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
47 changes: 34 additions & 13 deletions test/spat.test-issues.ract.template
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,34 @@
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks
RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks
RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s
RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s
RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s
RFLX.RFLX_Types.U64_Insert.Read => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.U64_Insert.Write => 20.0 ms/20.0 ms/70.0 ms
RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms
RFLX.RFLX_Types.U64_Extract.D.ES => 10.0 ms/10.0 ms/10.0 ms
RFLX.RFLX_Types.Unreachable_Bit_Length => 10.0 ms/10.0 ms/10.0 ms
RFLX.Arrays.Tests.Name => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Register_Tests => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671 => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_First => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Generating_Arrays_Messages_Message.set_payloadGP51671.Set_Payload.Buffer_Last => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_AV_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Enumeration_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Message => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Messages_Message_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Modular_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Loop => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Test_Parsing_Arrays_Range_Sequential => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Valid_Data_Length => 0.0 s/0.0 s/0.0 s
RFLX.Arrays.Tests.Write_Data => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s
RFLX.RFLX_Types.Last_Bit_Index => 0.0 s/0.0 s/0.0 s
Loading

0 comments on commit a942ad4

Please sign in to comment.