diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml index 3a1cad261993528fc7b8c93dd1c0e06cc1705d2d..f2165fb862b5d8ff00dcd8f4cf0ac3eb20ff15ce 100644 --- a/src/kernel_services/ast_queries/filecheck.ml +++ b/src/kernel_services/ast_queries/filecheck.ml @@ -1310,6 +1310,15 @@ module Base_checker = struct | Local_init (v, ConsInit(f,args,k),loc) -> self#check_initialized_var v; Cil.treat_constructor_as_func treat_call v f args k loc + | Set(lv, rv, _) -> + let t1 = Cil.typeOfLval lv in + let t2 = Cil.typeOf rv in + if not (is_admissible_conversion rv t2 t1) then + check_abort + "Incompatible types in assignment %a:\ + location has type %a, value has type %a" + Printer.pp_instr i Printer.pp_typ t1 Printer.pp_typ t2; + Cil.DoChildren | Asm(_,_,Some { asm_gotos },_) -> List.iter self#check_label asm_gotos; Cil.DoChildren | _ -> Cil.DoChildren