From 01491b5632f4b32e963eab4ba9a92cc4494bfbb6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Mon, 20 Dec 2021 11:39:24 +0100 Subject: [PATCH] [kernel] Cil builder: insert a cast in assign instructions when needed. When the right expression and the lvalue have different types, inserts a cast. --- src/kernel_services/ast_building/cil_builder.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml index b2767a1a9e1..75b1683898f 100644 --- a/src/kernel_services/ast_building/cil_builder.ml +++ b/src/kernel_services/ast_building/cil_builder.ml @@ -745,7 +745,10 @@ struct | Skip -> Cil_types.Skip (loc) | Assign (dest,src) -> - Cil_types.Set (build_lval ~loc dest, build_exp ~loc src, loc) + let dest' = build_lval ~loc dest + and src' = build_exp ~loc src in + let src' = Cil.mkCast ~newt:(Cil.typeOfLval dest') src' in + Cil_types.Set (dest', src', loc) | Call (dest,callee,args) -> let dest' = Option.map (build_lval ~loc) dest and callee' = build_exp ~loc callee -- GitLab