# GNATProve fails to catch invalid Unchecked\_Conversion?
**URL:** https://forum.ada-lang.io/t/gnatprove-fails-to-catch-invalid-unchecked-conversion/4782
**Category:** General
**Created:** [September 30, 2026, 9:59pm UTC](https://forum.ada-lang.io/t/gnatprove-fails-to-catch-invalid-unchecked-conversion/4782 "2026-09-30T21:59:58Z")
**Posts on this page:** 2
**Page:** 1
### Author:  [@lunarlattice0](https://forum.ada-lang.io/u/lunarlattice0)
#### Post date: [September 30, 2026, 9:59pm UTC](https://forum.ada-lang.io/t/gnatprove-fails-to-catch-invalid-unchecked-conversion/4782/1 "2026-09-30T21:59:58Z")
Hi,
I recently used Unchecked\_Conversion to convert arbitrary data (i.e. an array of bytes) into a record type for a toy ELF header parser. To my knowledge, Unchecked\_Conversion can be verified by gnatprove to not result in any runtime errors, by proving that the end result type does not have any invalid arrangement of bits. My code managed to pass gnatprove, but still managed to execute with erroneous behavior, corrupting the stack.
My original code is as follows. Note that the implementation of the record is wrong, since the index is incorrectly in bits instead of bytes. In addition, there are no bounds on the record (no size aspect on the record) and it doesn’t manage endian differences.
.ads:
```ada
type Elf64_Ehdr is record
e_ident : E_Ident_Array;
e_type : Elf64_Half;
e_machine : Elf64_Half;
e_version : Elf64_Word;
e_entry : Elf64_Addr;
e_phoff : Elf64_Off;
e_shoff : Elf64_Off;
e_flags : Elf64_Word;
e_ehsize : Elf64_Half;
e_phentsize : Elf64_Half;
e_phnum : Elf64_Half;
e_shentsize : Elf64_Half;
e_shnum : Elf64_Half;
e_shstrndx : Elf64_Half;
end record
with Convention => C, Alignment => 8;
-- C-compatible layout for Elf64_Ehdr.
-- Note: 'at' and 'range' are in bits.
for Elf64_Ehdr use record
e_ident at 0 range 0 .. 127; -- 0 .. 15 bytes
e_type at 128 range 0 .. 15; -- 16 .. 17 bytes
e_machine at 144 range 0 .. 15; -- 18 .. 19 bytes
e_version at 160 range 0 .. 31; -- 20 .. 23 bytes
e_entry at 192 range 0 .. 63; -- 24 .. 31 bytes
e_phoff at 256 range 0 .. 63; -- 32 .. 39 bytes
e_shoff at 320 range 0 .. 63; -- 40 .. 47 bytes
e_flags at 384 range 0 .. 31; -- 48 .. 51 bytes
e_ehsize at 416 range 0 .. 15; -- 52 .. 53 bytes
e_phentsize at 432 range 0 .. 15; -- 54 .. 55 bytes
e_phnum at 448 range 0 .. 15; -- 56 .. 57 bytes
e_shentsize at 464 range 0 .. 15; -- 58 .. 59 bytes
e_shnum at 480 range 0 .. 15; -- 60 .. 61 bytes
e_shstrndx at 496 range 0 .. 15; -- 62 .. 63 bytes
end record;
type ByteArray is array (size_t range <>) of unsigned_char;
```
.adb:
```ada
function GetELFHeader64 (fPath : in chars_ptr) return Elf64_Ehdr
is
bArray : constant ByteArray (1 .. 64) := ReadChunkFromMmap(fPath, 64, 0);
elfHeader64 : Elf64_Ehdr;
function ByteArrayToElf64_Ehdr_Bytes is
new Ada.Unchecked_Conversion(Source => ByteArray, Target => Elf64_Ehdr);
begin
pragma assert (bArray'First = 1);
elfHeader64 := ByteArrayToElf64_Ehdr_Bytes(bArray);
return elfHeader64;
end;
```
I managed to fix the bug causing UB by fixing the indices of the record, and enforce a strict size with Aspect Size =\> 512.
Is gnatprove intended to deal with situations like this?
---
### Author:  [@OneWingedShark](https://forum.ada-lang.io/u/OneWingedShark)
#### Post date: [September 30, 2026, 10:53pm UTC](https://forum.ada-lang.io/t/gnatprove-fails-to-catch-invalid-unchecked-conversion/4782/2 "2026-09-30T22:53:38Z")
> [@lunarlattice0](#):
>
> Is gnatprove intended to deal with situations like this?
There are several “unsafe” and “unprovable” things that GNATProve cannot detect and which would greatly hinder SPARK usability; `Unchecked_Conversion` is one of these. — The compiler already warns you about size mismatches in the types, and that’s about all it _can_ do.
That said, there is the `'Valid` attribute that you can look into. (Its purpose is exactly for cases like `Unchecked_Conversion`, streams, and memory-mapped IO where you can get a value but it might violate some constraint.)