From 24cea04dc857947081464fb7a63a41c07c28c5b8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 21 Mar 2022 15:55:34 +0100
Subject: [PATCH] [kernel] filecheck checks coherence of types in assignments
---
src/kernel_services/ast_queries/filecheck.ml | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 3a1cad26199..f2165fb862b 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
--
GitLab