runtimeverification/match

RV-Match issue tracker and releases

match's Issues

Find slides presenting RV-Match - its structure/architecture: the K framework, backend(s). Not too high level.

Include it in the report.

HIGH - Linker OOM

Kevin got an out of memory error when linking 300+ objects.

PID USER      PR  NI    VIRT    RES    SHR S  %CPU %MEM

8495 root      20   0 14.118g 0.013t  13092 R 100.0 88.4

The platform that runs RV-Match has 16G of memory.

Log :

Fatal error: exception Out of memory
Raised by primitive operation at file "buffer.ml", line 70, characters 19-40
Called from file "buffer.ml" (inlined), line 79, characters 26-36
Called from file "prelude.ml", line 106, characters 8-44
Called from file "prelude.ml", line 127, characters 83-97
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml", line 118, characters 13-24
Called from file "prelude.ml" (inlined), line 118, characters 26-39
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41
Called from file "prelude.ml" (inlined), line 118, characters 13-24
Called from file "prelude.ml", line 126, characters 29-46
Called from file "prelude.ml", line 121, characters 12-41

LOW - Weak attribute

Kevin asked if RV-Match supports the weak attribute ( https://gcc.gnu.org/onlinedocs/gcc-3.2/gcc/Function-Attributes.html ). He says that it would be more practical to them than the kcc_extends_tu_of one. I personally didn't find anything by looking through the code, but he showed me that we have this: https://github.com/runtimeverification/rv-match_testing/blob/master/tests/reduced/published/commonfunctionattributes.c

Even if we don't support it, he asked how hard would it be to implement it.

Per Virgil: To be specific, the weak attribute would be more practical than kcc_extends_tu_of because it's hard for them to find the right TU for a given function.

MEDIUM - Message readability

The error messages do not have enough information in them. Specifically, the "Conversion to unsigned integer outside the range..." message says that something happened in the middle of a possibly large formula, together with (only) the line on which it happened. The column information seems to not be accurate.

Examples of things that would help:

1. Print the value that was converted.
2. Print the expression that did overflow.
3. Print the start and end columns of the expression.

MEDIUM - Allow short int and other types in bitfields.

MEDIUM - Early loop termination

Denso has valid infinite loops in their code, and they would like to be able to run those with Klee+RV-Match. I think they patched Klee so that it exits any loop after a maximum number of steps, and they would like to be able to do the same with RV-Match. I guess a flag --max-loop-steps=<number> would be a good solution for them.

2020 progress report

HIGH - Compilation error for klee_get_obj_size

Per Virgil: Not fully investigated, here is the most likely interpretation:

Denso is using klee_get_obj_size for volatile pointers. However, we declare its argument as void* internally, so they will get compilation errors when passing those pointers.

Notes for detected errors in definition of macro

Kevin describes potentially needing notes for detected errors in definition of macro. In their production code there are macros sometime as complicate as a function. Without notes for detected errors in the definition of macro, there is difficulty to locate errors.

He points out that the preprocessing in kcc is done by gcc, so there are information that might not be available.
At his request, we creat an issue to investigate whether this is realizable or not. Any other Ideas of how to locate such errors are also welcome.

Here is the reporting template:

1      Brief description of the issue.
In our production code there are macros sometime as complicate as a function. Without notes for detected errors in the definition of macro, there is difficulty to locate errors.
2      The executed command (screenshot / text).
     kcc macro_note.c. && ./a.out
3      Relevant environment variables affecting translation / execution.
  NA
4       The observed failure, i.e. the output printed as a result of the failed executed command (screenshot / text as appropriate). If the error is a compilation error, please run
  NA
5      Access to triggering input (attach or share links).
  NA
6       "Reduced" example that triggers the error (attach or share links) - when possible (as indicated by the nature of the reported issue).
 Please refer to the attachment. I also attached the excepted output for your reference. 

macro_note.c.txt

macro_note.c.exe.ref.txt

Test issue

LOW - Investigate and optimize memory consumption and time increase resulting from column information for errors.

As a result of adding column information of errors, Kevin observed increased time and memory consumption.

The source compiled here is the one full of conditional branches in macro, used in their production.

1      Brief description of the issue.
  The usage of memory after the version that column information is added (e.g., 834e487) is much larger than before (32b52ce) as well as the time. For this particular source, roughly 3 times slower and 3 times memory usage than the version before.
2      The executed command (screenshot / text).
     /usr/bin/time -v make -f ../rv-action/Makefile rv > /dev/null
3      Relevant environment variables affecting translation / execution.
  None
4       The observed failure, i.e. the output printed as a result of the failed executed command (screenshot / text as appropriate). If the error is a compilation error, please run
  None
5      Access to triggering input (attach or share links).
  None
6       "Reduced" example that triggers the error (attach or share links) - when possible (as indicated by the nature of the reported issue).
  None.

834e487:
Command being timed: "make -f ../rv-action/Makefile rv"
        User time (seconds): 892.20
        System time (seconds): 31.24
        Percent of CPU this job got: 99%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 15:25.94
        Average shared text size (kbytes): 0
        Average unshared data size (kbytes): 0
        Average stack size (kbytes): 0
        Average total size (kbytes): 0
        Maximum resident set size (kbytes): 18413108
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 354
        Minor (reclaiming a frame) page faults: 652799
        Voluntary context switches: 5438
        Involuntary context switches: 2327
        Swaps: 0
        File system inputs: 6249736
        File system outputs: 9035112
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 0
 
32b52ce:
Command being timed: "make -f ../rv-action/Makefile system"
        User time (seconds): 289.97
        System time (seconds): 2.29
        Percent of CPU this job got: 100%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 4:52.19
        Average shared text size (kbytes): 0
        Average unshared data size (kbytes): 0
        Average stack size (kbytes): 0
        Average total size (kbytes): 0
        Maximum resident set size (kbytes): 4883300
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 0
        Minor (reclaiming a frame) page faults: 341129
        Voluntary context switches: 2626
        Involuntary context switches: 501
        Swaps: 0
        File system inputs: 0
        File system outputs: 2067552
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 0

LOW - Allow disabling all implementation-defined behaviour in a given (platform-dependant) file

The reasoning here is that they have files which are full of hardware-dependent code, and it would be tedious to disable all implementation-defined behaviour warnings one by one for each file.

HIGH - struct size different from gcc/clang

This struct:

typedef struct ISD_PK_IMPORT_EXT
{
   
    const uint32_t             *p_x509_certificate;
    uint16_t                    x509_certificate_size_in_bytes;
    
} ISD_PK_IMPORT_EXT_t;

has size 12 with clang/gcc, but 16 with kcc.

MEDIUM - Value information for errors

Denso would like to have actual values for warnings like "Conversion to unsigned integer outside the range" (e.g. it may be fairly informative if -1 is being converted to unsigned).