Merge branch...

Merge branch 'fix/martin/kernel/1243-kernel-comportement-erratique-de-l-iterateur-des-property-status' into 'master'

Resolve "[kernel] comportement erratique de l'itérateur des property status"

Closes #1243

See merge request frama-c/frama-c!4421

src/plugins/variadic/environment.ml

@@ -90,6 +90,12 @@ let find_type (env : t) (namespace : Logic_typing.type_namespace)
   | Logic_typing.Enum ->
     TEnum (find_enum env tname, [])
 
+let mem_global (env : t) (vname : string) : bool =
+  Table.mem env.globals vname
+
+let mem_function (env : t) (vname : string) : bool =
+  Table.mem env.functions vname
+
 let from_file (file : file) : t =
   let env = empty () in
   let v = object inherit Cil.nopCilVisitor

src/plugins/variadic/environment.mli

@@ -34,3 +34,6 @@ val find_struct : t -> string ->  Cil_types.compinfo
 val find_union : t -> string ->  Cil_types.compinfo
 val find_enum : t -> string ->  Cil_types.enuminfo
 val find_type : t -> Logic_typing.type_namespace -> string -> Cil_types.typ
+
+val mem_global : t -> string -> bool
+val mem_function : t -> string -> bool

src/plugins/variadic/standard.ml

@@ -173,23 +173,34 @@ let match_call ~builder new_callee new_tparams args =
   Build.(List.iter pure (of_exp_list unused_args));
   Build.(translated_call (var new_callee) (of_exp_list new_args))
 
+
+let check_available_name env name =
+  not @@ Environment.mem_global env name
+  && not @@ Environment.mem_function env name
+
+let get_next_name env id name =
+  let rec aux id =
+    let next_name = name ^ (string_of_int id) in
+    if check_available_name env next_name then
+      next_name, id
+    else
+      aux (id + 1)
+  in
+  aux id
+
 (* ************************************************************************ *)
 (* Fallback calls                                                           *)
 (* ************************************************************************ *)
 
-let fallback_fun_call ~builder ~callee vf args =
+let fallback_fun_call ~builder ~callee env vf args =
   let module Build = (val builder : Builder.S) in
 
   (* Choose function name *)
   let name = callee.vname in
   let vorig_name = callee.vorig_name in
-  let count =
-    try Fallback_counts.find name
-    with Not_found -> 0
-  in
-  let count = count + 1 in
-  Fallback_counts.replace name count;
-  let new_name = name ^ "_fallback_" ^ (string_of_int count) in
+  let count = try Fallback_counts.find name + 1 with Not_found -> 1 in
+  let new_name, new_count = get_next_name env count (name ^ "_fallback_") in
+  Fallback_counts.replace name new_count;
 
   (* Start building the function *)
   let loc = vf.vf_decl.vdecl in
@@ -431,15 +442,15 @@ let valid_read_nstring typ =
 let format_length typ =
   find_predicate_by_width typ "format_length" "wformat_length"
 
-
 let build_specialized_fun ~builder env vf format_fun tvparams =
   let open Format_types in
   let module Build = (val builder : Builder.S) in
 
   (* Choose function name *)
   let name = vf.vf_decl.vorig_name in
-  vf.vf_specialization_count <- vf.vf_specialization_count + 1;
-  let new_name = name ^ "_va_" ^ (string_of_int vf.vf_specialization_count) in
+  let id = vf.vf_specialization_count + 1 in
+  let new_name, new_count = get_next_name env id (name ^ "_va_") in
+  vf.vf_specialization_count <- new_count;
 
   (* Start building the function *)
   let loc = vf.vf_decl.vdecl in

src/plugins/variadic/standard.mli

@@ -24,6 +24,7 @@ exception Translate_call_exn of Cil_types.varinfo
 
 val fallback_fun_call :
   builder:Builder.t -> callee:Cil_types.varinfo ->
+  Environment.t ->
   Va_types.variadic_function -> Cil_types.exp list -> unit
 
 val aggregator_call :

src/plugins/variadic/tests/known/oracle/print_libc.pretty.c

@@ -51,12 +51,12 @@ int printf_va_1(char const * restrict format);
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
  */
-int printf_va_1(char const * restrict format);
+int printf_va_2(char const * restrict format);
 
 int main(void)
 {
   int __retres;
-  printf(""); /* printf_va_1 */
+  printf(""); /* printf_va_2 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/translate.ml

@@ -200,7 +200,7 @@ let translate_variadics (file : file) =
             try
               f ~builder args
             with Standard.Translate_call_exn callee ->
-              Standard.fallback_fun_call ~callee ~builder vf args
+              Standard.fallback_fun_call ~callee ~builder env vf args
         in
         match vf.vf_class with
         | Overload o -> cover_failure (Standard.overloaded_call o vf)

tests/syntax/oracle/variadic_fresh_names.res.oracle

+[kernel] Parsing variadic_fresh_names.c (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+                 int param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_2(FILE * restrict stream, char const * restrict format,
+                 int param0);
+
+void main(void)
+{
+  fprintf(__fc_stderr,"%d ",42); /* fprintf_va_2 */
+  return;
+}
+
+

tests/syntax/variadic_fresh_names.c

+/* run.config
+PLUGIN: variadic
+STDOPT:
+*/
+#include "stdio.h"
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+                 int param0);
+
+void main(void)
+{
+  fprintf(__fc_stderr,"%d ",42); /* fprintf_va_1 */
+  return;
+}