From 3f31833ef58e9d9fec4e2f3c871b2176636c2cc5 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 29 Apr 2022 16:35:21 +0200
Subject: [PATCH] [kernel] AST diff: do not rely on TypByName for basic types
---
src/kernel_services/ast_queries/ast_diff.ml | 16 +++++++++++++---
1 file changed, 13 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 343fff1a0b4..7d0ed08d486 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -471,6 +471,10 @@ module Ikind = struct
type t = [%import: Cil_types.ikind] [@@deriving eq]
end
+module Fkind = struct
+ type t = [%import: Cil_types.fkind] [@@deriving eq]
+end
+
module Predicate_kind = struct
type t = [%import: Cil_types.predicate_kind] [@@deriving eq]
end
@@ -889,8 +893,13 @@ and is_same_model_info mi mi' env =
and is_same_type t t' env =
match t, t' with
- | (TVoid _ | TInt _ | TFloat _ | TBuiltin_va_list _), _ ->
- Cil_datatype.TypByName.equal t t'
+ | TVoid a, TVoid a' -> Cil_datatype.Attributes.equal a a'
+ | TInt (ik,a), TInt(ik',a') ->
+ Ikind.equal ik ik' && Cil_datatype.Attributes.equal a a'
+ | TFloat (fk,a), TFloat(fk', a') ->
+ Fkind.equal fk fk' && Cil_datatype.Attributes.equal a a'
+ | TBuiltin_va_list a, TBuiltin_va_list a' ->
+ Cil_datatype.Attributes.equal a a'
| TPtr(t,a), TPtr(t',a') ->
is_same_type t t' env && Cil_datatype.Attributes.equal a a'
| TArray(t,s,a), TArray(t',s',a') ->
@@ -920,7 +929,8 @@ and is_same_type t t' env =
| `Not_present -> false
| `Same e'' -> Cil_datatype.Enuminfo.equal e' e'') &&
Cil_datatype.Attributes.equal a a'
- | (TPtr _ | TArray _ | TFun _ | TNamed _ | TComp _ | TEnum _), _ -> false
+ | (TVoid _ | TInt _ | TFloat _ | TBuiltin_va_list _ | TPtr _ | TArray _
+ | TFun _ | TNamed _ | TComp _ | TEnum _), _ -> false
and is_same_compinfo ci ci' env =
ci.cstruct = ci'.cstruct &&
--
GitLab