--- 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 }