From 931459d13a731a2a8db1601ce688a3d66d2fd801 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Wed, 21 Nov 2018 16:45:24 +0100
Subject: [PATCH] Renames and fixes the behavior of getNameLastFormal is
presence of ghost parameters for variadic
---
src/kernel_internals/typing/cabs2cil.ml | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 8f061f3f097..1004eaa7c5b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6689,9 +6689,10 @@ and doExp local_env
| _ -> e
in
(* Get the name of the last formal *)
- let getNameLastFormal () : string =
+ let getNameLastNonGhostFormal () : string =
match !currentFunctionFDEC.svar.vtype with
| TFun(_, Some args, true, _) -> begin
+ let args, _ = Cil.argsToPairOfLists (Some args) in
match List.rev args with
| (last_par_name, _, _) :: _ -> last_par_name
| _ -> ""
@@ -6740,7 +6741,7 @@ and doExp local_env
let isOk =
match (dropCasts last).enode with
| Lval (Var lastv, NoOffset) ->
- lastv.vname = getNameLastFormal ()
+ lastv.vname = getNameLastNonGhostFormal ()
| _ -> false
in
if not isOk && variad then
@@ -6776,7 +6777,7 @@ and doExp local_env
let isOk =
match (dropCasts last).enode with
| Lval (Var lastv, NoOffset) ->
- lastv.vname = getNameLastFormal ()
+ lastv.vname = getNameLastNonGhostFormal ()
| _ -> false
in
if not isOk then
@@ -6815,7 +6816,7 @@ and doExp local_env
let isOk =
match (dropCasts last).enode with
| Lval (Var lastv, NoOffset) ->
- lastv.vname = getNameLastFormal ()
+ lastv.vname = getNameLastNonGhostFormal ()
| _ -> false
in
if not isOk then
--
GitLab