1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
--- CompCert calling native:
si8u: 177
si8s: -79
si16u: 64305
si16s: -1231
s1: { a = 'a' }
s2: { a = 'a', b = 'b' }
s3: { a = 'a', b = 'b', c = ' c' }
s4: { a = 'a', b = 'b', c = ' c', d = 'd' }
s5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
s6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
s7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
s8: "Hello world!"
t1: { a = 123 }
t2: { a = 123, b = 456 }
t3: { a = 123, b = 456, c = 789 }
t4: { a = 123, b = 456, c = 789, d = -111 }
t5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
u1: { a = 12 }
u2: { a = 12, b = -34 }
u3: { a = 12, b = 34, c = -56 }
u4: { a = 12, b = 34, c = 56, d = -78 }
u5: { a = 1234, b = 'u' }
u6: { a = 55555, b = 666 }
u7: { a = -10001, b = -789, c = 'z' }
u8: { a = 'x', b = 12345 }
after ms4, x = { 's', 'a', 'm', 'e' }
after mu4, x = { a = { 11, 22, 33, 44 } }
rs1: { a = 'a' }
rs2: { a = 'a', b = 'b' }
rs3: { a = 'a', b = 'b', c = ' c' }
rs4: { a = 'a', b = 'b', c = ' c', d = 'd' }
rs5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
rs6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
rs7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
rs8: "Hello world!"
rt1: { a = 123 }
rt2: { a = 123, b = 456 }
rt3: { a = 123, b = 456, c = 789 }
rt4: { a = 123, b = 456, c = 789, d = -111 }
rt5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
ru1: { a = 12 }
ru2: { a = 12, b = -34 }
ru3: { a = 12, b = 34, c = -56 }
ru4: { a = 12, b = 34, c = 56, d = -78 }
ru5: { a = 1234, b = 'u' }
ru6: { a = 55555, b = 666 }
ru7: { a = -10001, b = -789, c = 'z' }
ru8: { a = 'x', b = 12345 }
--- native calling CompCert:
si8u: 177
si8s: -79
si16u: 64305
si16s: -1231
s1: { a = 'a' }
s2: { a = 'a', b = 'b' }
s3: { a = 'a', b = 'b', c = ' c' }
s4: { a = 'a', b = 'b', c = ' c', d = 'd' }
s5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
s6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
s7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
s8: "Hello world!"
t1: { a = 123 }
t2: { a = 123, b = 456 }
t3: { a = 123, b = 456, c = 789 }
t4: { a = 123, b = 456, c = 789, d = -111 }
t5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
u1: { a = 12 }
u2: { a = 12, b = -34 }
u3: { a = 12, b = 34, c = -56 }
u4: { a = 12, b = 34, c = 56, d = -78 }
u5: { a = 1234, b = 'u' }
u6: { a = 55555, b = 666 }
u7: { a = -10001, b = -789, c = 'z' }
u8: { a = 'x', b = 12345 }
after ms4, x = { 's', 'a', 'm', 'e' }
after mu4, x = { a = { 11, 22, 33, 44 } }
rs1: { a = 'a' }
rs2: { a = 'a', b = 'b' }
rs3: { a = 'a', b = 'b', c = ' c' }
rs4: { a = 'a', b = 'b', c = ' c', d = 'd' }
rs5: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e' }
rs6: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f' }
rs7: { a = 'a', b = 'b', c = ' c', d = 'd', e = 'e', f = 'f', g = 'g' }
rs8: "Hello world!"
rt1: { a = 123 }
rt2: { a = 123, b = 456 }
rt3: { a = 123, b = 456, c = 789 }
rt4: { a = 123, b = 456, c = 789, d = -111 }
rt5: { a = 123, b = 456, c = 789, d = -999, e = 'x' }
ru1: { a = 12 }
ru2: { a = 12, b = -34 }
ru3: { a = 12, b = 34, c = -56 }
ru4: { a = 12, b = 34, c = 56, d = -78 }
ru5: { a = 1234, b = 'u' }
ru6: { a = 55555, b = 666 }
ru7: { a = -10001, b = -789, c = 'z' }
ru8: { a = 'x', b = 12345 }
|
