From ee84f7cb88556f7d150be44862d5529189edecf0 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 7 May 2020 17:27:31 +0200
Subject: [PATCH] [link] merge names of formals when old prototype has
 anonymous parameter

---
 src/kernel_internals/typing/mergecil.ml | 36 ++++++++++++++++---------
 tests/spec/anon_arg_1.i                 |  8 ++++++
 tests/spec/anon_arg_2.i                 | 15 +++++++++++
 tests/spec/oracle/anon_arg_2.res.oracle | 19 +++++++++++++
 4 files changed, 66 insertions(+), 12 deletions(-)
 create mode 100644 tests/spec/anon_arg_1.i
 create mode 100644 tests/spec/anon_arg_2.i
 create mode 100644 tests/spec/oracle/anon_arg_2.res.oracle

diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index f1a939b213f..396af5ea5ac 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -2637,6 +2637,29 @@ let equalInitOpts (x: init option) (y: init option) : bool =
     | _,_ -> false
   end
 
+let merge_arg_names merged_args curr_args =
+  let do_one_arg merged_arg curr_arg =
+    (* if curr_arg is also anonymous, this doesn't do much,
+       but at least doesn't worsen things. *)
+    if merged_arg.vname = "" then merged_arg.vname <- curr_arg.vname
+  in
+  (* if both list have different lengths, merge should have failed earlier. *)
+  List.iter2 do_one_arg merged_args curr_args
+
+let update_formals_names merged_vi curr_vi =
+  (* if the reference varinfo already has formals, everything
+     is renamed accordingly. However, if the old prototype contains
+     anonymous formal declarations, while the corresponding current formal
+     has a name, we keep the new name. *)
+  match Cil.getFormalsDecl curr_vi with
+  | curr_args ->
+    (match Cil.getFormalsDecl merged_vi with
+     | merged_args -> merge_arg_names merged_args curr_args
+     | exception Not_found ->
+       (*existing prototype does not have formals list. Just use current one*)
+       Cil.unsafeSetFormalsDecl merged_vi curr_args)
+  | exception Not_found -> ()
+    (* current prototype does not have formals list, nothing to merge. *)
 
 (* Now we go once more through the file and we rename the globals that we
  * keep. We also scan the entire body and we replace references to the
@@ -2730,18 +2753,7 @@ let oneFilePass2 (f: file) =
         if not (is_ignored_vi vi) then begin
           (* Drop the decl, keep the spec *)
           mergeSpec vi' vi spec';
-          (try
-             (* if the reference varinfo already has formals, everything
-                is renamed accordingly. *)
-             ignore (Cil.getFormalsDecl vi')
-           with Not_found ->
-           (* Otherwise, if we have formals here, register them with
-              the reference varinfo *)
-           try
-             let my_formals = Cil.getFormalsDecl vi in
-             Cil.unsafeSetFormalsDecl vi' my_formals
-           with Not_found -> ()
-           (* Neither decl has formals. Do nothing. *));
+          update_formals_names vi' vi;
         end;
         Cil.removeFormalsDecl vi
       end
diff --git a/tests/spec/anon_arg_1.i b/tests/spec/anon_arg_1.i
new file mode 100644
index 00000000000..386a5754268
--- /dev/null
+++ b/tests/spec/anon_arg_1.i
@@ -0,0 +1,8 @@
+/* run.config*
+DONTRUN: main test in anon_arg_2.i
+*/
+
+int f(int*, int);
+
+/*@ ensures \result == x; */
+int g(int*, int x);
diff --git a/tests/spec/anon_arg_2.i b/tests/spec/anon_arg_2.i
new file mode 100644
index 00000000000..9e3ef0cb8d0
--- /dev/null
+++ b/tests/spec/anon_arg_2.i
@@ -0,0 +1,15 @@
+/* run.config*
+STDOPT: #"@PTEST_DIR@/anon_arg_1.i @PTEST_FILE@"
+*/
+
+/*@ requires \valid(p);
+    assigns *p \from x;
+    ensures \result == x && *p == x;
+*/
+int f(int* p, int x);
+
+/*@ requires \valid(p);
+    assigns *p;
+    ensures *p == \result;
+*/
+int g(int*p, int);
diff --git a/tests/spec/oracle/anon_arg_2.res.oracle b/tests/spec/oracle/anon_arg_2.res.oracle
new file mode 100644
index 00000000000..54b9b9f1cd7
--- /dev/null
+++ b/tests/spec/oracle/anon_arg_2.res.oracle
@@ -0,0 +1,19 @@
+[kernel] Parsing tests/spec/anon_arg_1.i (no preprocessing)
+[kernel] Parsing tests/spec/anon_arg_2.i (no preprocessing)
+[kernel] tests/spec/anon_arg_1.i:7: Warning: found two contracts. Merging them
+/* Generated by Frama-C */
+/*@ requires \valid(p);
+    ensures \result ≡ \old(x) ∧ *\old(p) ≡ \old(x);
+    assigns *p;
+    assigns *p \from x;
+ */
+int f(int *p, int x);
+
+/*@ requires \valid(p);
+    ensures \result ≡ \old(x);
+    ensures *\old(p) ≡ \result;
+    assigns *p;
+ */
+int g(int *p, int x);
+
+
-- 
GitLab