Merge branch 'fix/kernel/assign-builder' into 'master'

[kernel] Cil builder: insert a cast in assign instructions when needed.

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

src/kernel_services/ast_building/cil_builder.ml

@@ -745,7 +745,10 @@ struct
     | Skip ->
       Cil_types.Skip (loc)
     | Assign (dest,src) ->
-      Cil_types.Set (build_lval ~loc dest, build_exp ~loc src, loc)
+      let dest' = build_lval ~loc dest
+      and src' = build_exp ~loc src in
+      let src' = Cil.mkCast ~newt:(Cil.typeOfLval dest') src' in
+      Cil_types.Set (dest', src', loc)
     | Call (dest,callee,args) ->
       let dest' = Option.map (build_lval ~loc) dest
       and callee' = build_exp ~loc callee

src/plugins/variadic/tests/defined/oracle/va_arg_cast.res.oracle

+[kernel:parser:decimal-float] va_arg_cast.c:17: Warning: 
+  Floating-point constant 7.1 is not represented exactly. Will use 0x1.c666666666666p2.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[variadic] va_arg_cast.c:10: Declaration of variadic function c.
+[variadic] va_arg_cast.c:17: Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function b:
+  a ∈ {4619679907765970542}
+  ap ∈ {{ &__va_args[2] }}
+[eva:final-states] Values at end of function c:
+  a ∈ {4619679907765970542}
+  ap ∈ {{ &__va_args[0] }}
+[eva:final-states] Values at end of function main:
+  a ∈ {4619679907765970542}
+/* Generated by Frama-C */
+#include "stdarg.h"
+long a;
+void b(va_list ap)
+{
+  long tmp;
+  a = (long)*((double *)*ap);
+  ap ++;
+  tmp = *((long *)*ap);
+  ap ++;
+  a += tmp;
+  return;
+}
+
+void c(int d, void * const *__va_params)
+{
+  va_list ap;
+  ap = __va_params;
+  b(ap);
+  return;
+}
+
+void main(void)
+{
+  {
+    double __va_arg0 = 8.1;
+    double __va_arg1 = 7.1;
+    void *__va_args[2] = {& __va_arg0, & __va_arg1};
+    c(0,(void * const *)(__va_args));
+  }
+  return;
+}
+
+

src/plugins/variadic/tests/defined/va_arg_cast.c

+#include <stdarg.h>
+
+long a;
+
+void b(va_list ap) {
+  a = va_arg(ap, double);
+  a += va_arg(ap, long);
+}
+
+void c(int d, ...) {
+  va_list ap;
+  va_start(ap, d);
+  b(ap);
+}
+
+void main() {
+    c(0, 8.1, 7.1);
+}