diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml index b2767a1a9e131934f3e15fb13b508496e8715180..75b1683898f297a5fd421c9c038acb77ffcf566d 100644 --- a/src/kernel_services/ast_building/cil_builder.ml +++ b/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 diff --git a/src/plugins/variadic/tests/defined/oracle/va_arg_cast.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_arg_cast.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..7d4f6bbe42c510298deabb8bccb7d78cd06e7efb --- /dev/null +++ b/src/plugins/variadic/tests/defined/oracle/va_arg_cast.res.oracle @@ -0,0 +1,52 @@ +[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; +} + + diff --git a/src/plugins/variadic/tests/defined/va_arg_cast.c b/src/plugins/variadic/tests/defined/va_arg_cast.c new file mode 100644 index 0000000000000000000000000000000000000000..0f643ab62247c7385929df1b2c5b6f45d1e5825c --- /dev/null +++ b/src/plugins/variadic/tests/defined/va_arg_cast.c @@ -0,0 +1,18 @@ +#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); +}