From 8ece719c8c4b9261da2ca35a5154ad47e9fe305e Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 5 Mar 2024 10:07:59 +0100
Subject: [PATCH] [kernel] Always the same 2nd value in this couple, simplified
---
src/kernel_services/ast_queries/cil.ml | 21 ++++++++++-----------
1 file changed, 10 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index eb576984e72..ad024ecf84e 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6205,9 +6205,9 @@ let combineTypesGen ?emitwith (combF : combineFunction)
raise (Cannot_combine "different vararg specifiers");
(* If one does not have arguments, believe the one with the
* arguments *)
- let newargs, olda' =
- if oldargs = None then args, olda
- else if args = None then oldargs, olda
+ let newargs =
+ if oldargs = None then args
+ else if args = None then oldargs
else
let (oldargslist, oldghostargslist) = argsToPairOfLists oldargs in
let (argslist, ghostargslist) = argsToPairOfLists args in
@@ -6239,21 +6239,20 @@ let combineTypesGen ?emitwith (combF : combineFunction)
in
let a = addAttributes oa aa in
(n, t, a))
- oldargslist argslist),
- olda
+ oldargslist argslist)
in
(* Drop missingproto as soon as one of the type is a properly declared one*)
- let olda =
+ let olda' =
if not (hasAttribute "missingproto" a) then
- dropAttribute "missingproto" olda'
- else olda'
+ dropAttribute "missingproto" olda
+ else olda
in
- let a =
- if not (hasAttribute "missingproto" olda') then
+ let a' =
+ if not (hasAttribute "missingproto" olda) then
dropAttribute "missingproto" a
else a
in
- TFun (newrt, newargs, oldva, combineAttributes what olda a)
+ TFun (newrt, newargs, oldva, combineAttributes what olda' a')
| TBuiltin_va_list olda, TBuiltin_va_list a ->
TBuiltin_va_list (combineAttributes what olda a)
--
GitLab