From 0c17ac42814c64b233bb790d5ac25d1632d021b2 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 12 Nov 2020 16:37:24 -0800 Subject: [PATCH] [sledge] Add check that frontend preserves sizes of types Reviewed By: jvillard Differential Revision: D24772953 fbshipit-source-id: 269f0d7cb --- sledge/cli/frontend.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index 9d13d4068..67e26bd58 100644 --- a/sledge/cli/frontend.ml +++ b/sledge/cli/frontend.ml @@ -306,7 +306,12 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t = ; xlate_type_ llt |> - [%Trace.retn fun {pf} -> pf "%a" Typ.pp_defn] ) + [%Trace.retn fun {pf} ty -> + pf "%a" Typ.pp_defn ty ; + assert ( + (not (Llvm.type_is_sized llt)) + || (not (Typ.is_sized ty)) + || Typ.size_of ty = size_of x llt )] ) and xlate_type_opt : x -> Llvm.lltype -> Typ.t option = fun x llt ->