synchronize with frama-c master

c-testsuite/.frama-c/00214.parse/warnings.log

-00214.c:52:[kernel:CERT:MSC:37] warning: Body of function chk falls-through. Adding a return statement
+00214.c:54:[kernel:CERT:MSC:37] warning: Body of function chk falls-through. Adding a return statement
 [variadic:libc:frama-c] warning: Unable to locate ACSL predicate valid_read_string which should be in the Frama-C LibC. Correct specifications can't be generated.
 [variadic:libc:frama-c] warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.

c-testsuite/.frama-c/00218.parse/warnings.log

-00218.c:47:[kernel:CERT:MSC:37] warning: Body of function convert_like_real falls-through. Adding a return statement
+00218.c:48:[kernel:CERT:MSC:37] warning: Body of function convert_like_real falls-through. Adding a return statement
 [variadic:libc:frama-c] warning: Unable to locate ACSL predicate valid_read_string which should be in the Frama-C LibC. Correct specifications can't be generated.
 [variadic:libc:frama-c] warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.

cerberus/.frama-c/pointer_copy_user_ctrlflow_bytewise.parse/warnings.log

-pointer_copy_user_ctrlflow_bytewise.c:260:[kernel:CERT:MSC:37] warning: Body of function control_flow_copy falls-through. Adding a return statement
+pointer_copy_user_ctrlflow_bytewise.c:262:[kernel:CERT:MSC:37] warning: Body of function control_flow_copy falls-through. Adding a return statement

cerberus/.frama-c/pointer_copy_user_ctrlflow_bytewise_abbrev.parse/warnings.log

-pointer_copy_user_ctrlflow_bytewise_abbrev.c:8:[kernel:CERT:MSC:37] warning: Body of function control_flow_copy falls-through. Adding a return statement
+pointer_copy_user_ctrlflow_bytewise_abbrev.c:10:[kernel:CERT:MSC:37] warning: Body of function control_flow_copy falls-through. Adding a return statement

cerberus/.frama-c/pointer_offset_from_subtraction_1_auto.eva/warnings.log

@@ -3,5 +3,5 @@ because of arithmetic operation on addresses.
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   pointer_offset_from_subtraction_1_auto.c:5: arithmetic operation on addresses
-    (read in 4 statements, propagated through 4 statements)
+    (read in 3 statements, propagated through 4 statements)
     garbled mix of &{x; y}

cerberus/.frama-c/pointer_offset_from_subtraction_1_global.eva/warnings.log

@@ -3,5 +3,5 @@ because of arithmetic operation on addresses.
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   pointer_offset_from_subtraction_1_global.c:5: arithmetic operation on addresses
-    (read in 4 statements, propagated through 4 statements)
+    (read in 3 statements, propagated through 4 statements)
     garbled mix of &{y; x}

cerberus/.frama-c/pointer_offset_from_subtraction_2_auto.eva/warnings.log

@@ -6,7 +6,7 @@ because of arithmetic operation on addresses.
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   pointer_offset_from_subtraction_2_auto.c:8: arithmetic operation on addresses
-    (read in 5 statements, propagated through 3 statements)
+    (read in 4 statements, propagated through 3 statements)
     garbled mix of &{w; z; x}
   pointer_offset_from_subtraction_2_auto.c:5: arithmetic operation on addresses
     (read in 2 statements, propagated through 4 statements)

cerberus/.frama-c/pointer_offset_from_subtraction_2_global.eva/warnings.log

@@ -6,7 +6,7 @@ because of arithmetic operation on addresses.
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   pointer_offset_from_subtraction_2_global.c:8: arithmetic operation on addresses
-    (read in 5 statements, propagated through 3 statements)
+    (read in 4 statements, propagated through 3 statements)
     garbled mix of &{w; z; x}
   pointer_offset_from_subtraction_2_global.c:5: arithmetic operation on addresses
     (read in 2 statements, propagated through 4 statements)

frama-c @ 7f8f1b43

-Subproject commit 305ef50d6a1be8482ae6fedf6d3a64ab02122828
+Subproject commit 7f8f1b43c60499d7d98dd6764c10a633617f3e8a

gzip124/.frama-c/gzip124.eva/warnings.log

@@ -27,10 +27,7 @@ gzip.c:817:[eva:locals-escaping] warning: locals {attr} escaping the scope of zi
                      __malloc_w_huft_build_l403_11;
                      __malloc_w_huft_build_l403_12;
                      __malloc_w_huft_build_l403_13}
-  util.c:186: assigns clause on addresses
-    (read in 59 statements, propagated through 55 statements)
-    garbled mix of &{argv0; ifname; ofname}
-  inflate.c:446: misaligned read of addresses
+  inflate.c:423: misaligned read of addresses
     (read in 43 statements, propagated through 30 statements)
     garbled mix of &{__malloc_w_huft_build_l403;
                      __malloc_w_huft_build_l403_2;
@@ -38,6 +35,9 @@ gzip.c:817:[eva:locals-escaping] warning: locals {attr} escaping the scope of zi
                      __malloc_w_huft_build_l403_7;
                      __malloc_w_huft_build_l403_9;
                      __malloc_w_huft_build_l403_12}
+  util.c:186: assigns clause on addresses
+    (read in 11 statements, propagated through 8 statements)
+    garbled mix of &{argv0; ifname; ofname}
   gzip.c:1487: assigns clause on addresses
     (read in 3 statements, propagated through 2 statements)
     garbled mix of &{ofname}

hiredis/.frama-c/hiredis-format.eva/warnings.log

@@ -732,7 +732,7 @@ test.c:256:[eva:locals-escaping] warning: locals {__va_arg0_152, __va_arg1_154,
 test.c:256:[eva:locals-escaping] warning: locals {__va_arg0_152, __va_arg1_154, __va_arg2_156, __va_args_158} escaping the scope of a block of test_format_commands through __malloc_redisvFormatCommand_l476_18
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   sds.c:523: assigns clause on addresses
-    (read in 163 statements, propagated through 112 statements)
+    (read in 168 statements, propagated through 114 statements)
     garbled mix of &{__va_arg0_80; __va_arg1_82; __va_args_84; __va_arg0_86;
                      __va_arg1_88; __va_args_90; __va_arg0_92; __va_arg1_94;
                      __va_args_96; __va_arg0_98; __va_arg1_100;
@@ -861,16 +861,8 @@ test.c:256:[eva:locals-escaping] warning: locals {__va_arg0_152, __va_arg1_154,
                      __malloc_w_sdsMakeRoomFor_l230_48;
                      __realloc_w_sdsMakeRoomFor_l221_50;
                      __malloc_w_sdsMakeRoomFor_l230_49;
-                     __malloc_w_sdsMakeRoomFor_l230_50}
-  sds.c:208: arithmetic operation on addresses
-    (read in 111 statements, propagated through 83 statements)
-    garbled mix of &{__va_arg0_152; __va_arg1_154; __va_arg2_156;
-                     __va_args_158; "foo"; __malloc_sdsnewlen_l91_37;
-                     __realloc_w_sdsMakeRoomFor_l221_48;
-                     __malloc_w_sdsnewlen_l91_38;
-                     __realloc_w_sdsMakeRoomFor_l221_49;
-                     __malloc_w_sdsMakeRoomFor_l230_48;
-                     __realloc_w_sdsMakeRoomFor_l221_50;
-                     __malloc_w_sdsMakeRoomFor_l230_49;
                      __malloc_w_sdsMakeRoomFor_l230_50;
                      __malloc_redisvFormatCommand_l476_18}
+  sds.c:208: arithmetic operation on addresses
+    (read in 12 statements, propagated through 9 statements)
+    garbled mix of &{"foo"}

ioccc/.frama-c/2019_yang_violet.eva/alarms.csv

@@ -54,10 +54,10 @@ directory	file	line	function	property kind	status	property
 2019/yang	violet.c	41	main	mem_access	Unknown	\valid_read(&(U + h)->y)
 2019/yang	violet.c	42	main	initialization	Unknown	\initialized(&(U + h)->x)
 2019/yang	violet.c	42	main	mem_access	Unknown	\valid_read(&(U + h)->x)
-2019/yang	violet.c	42	main	initialization	Unknown	\initialized(&(U + h)->y)
-2019/yang	violet.c	42	main	mem_access	Unknown	\valid_read(&(U + h)->y)
 2019/yang	violet.c	42	main	initialization	Unknown	\initialized(&(U + h)->x)
 2019/yang	violet.c	42	main	mem_access	Unknown	\valid_read(&(U + h)->x)
+2019/yang	violet.c	42	main	initialization	Unknown	\initialized(&(U + h)->y)
+2019/yang	violet.c	42	main	mem_access	Unknown	\valid_read(&(U + h)->y)
 2019/yang	violet.c	43	main	initialization	Unknown	\initialized(&(U + (_)(h - 1))->z)
 2019/yang	violet.c	43	main	mem_access	Unknown	\valid_read(&(U + (_)(h - 1))->z)
 2019/yang	violet.c	45	main	mem_access	Unknown	\valid_read(Z)

itc-benchmarks/.frama-c/01_w_Defects.parse/warnings.log

 01_w_Defects/data_lost.c:56:[kernel:parser:decimal-float] warning: Floating-point constant 2.14748365e+09F is not represented exactly. Will use 0x1.0000000000000p31.
 (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
-01_w_Defects/not_return.c:20:[kernel:CERT:MSC:37] warning: Body of function not_return_001_func_001 falls-through. Adding a return statement
-01_w_Defects/not_return.c:39:[kernel:CERT:MSC:37] warning: Body of function not_return_002_func_001 falls-through. Adding a return statement
-01_w_Defects/not_return.c:74:[kernel:CERT:MSC:37] warning: Body of function not_return_003_func_001 falls-through. Adding a return statement
-01_w_Defects/not_return.c:98:[kernel:CERT:MSC:37] warning: Body of function not_return_004_func_001 falls-through. Adding a return statement
+01_w_Defects/not_return.c:24:[kernel:CERT:MSC:37] warning: Body of function not_return_001_func_001 falls-through. Adding a return statement
+01_w_Defects/not_return.c:50:[kernel:CERT:MSC:37] warning: Body of function not_return_002_func_001 falls-through. Adding a return statement
+01_w_Defects/not_return.c:76:[kernel:CERT:MSC:37] warning: Body of function not_return_003_func_001 falls-through. Adding a return statement
+01_w_Defects/not_return.c:99:[kernel:CERT:MSC:37] warning: Body of function not_return_004_func_001 falls-through. Adding a return statement

kgflags/.frama-c/kgflags-full_api.eva/alarms.csv

@@ -33,13 +33,9 @@ directory	file	line	function	property kind	status	property
 .	kgflags.h	550	kgflags_double_array_get_item	mem_access	Unknown	\valid_read(arr->_items + at)
 .	kgflags.h	608	_kgflags_get_flag	precondition of strcmp	Unknown	valid_string_s1: valid_read_string(s1)
 .	kgflags.h	608	_kgflags_get_flag	precondition of strcmp	Unknown	valid_string_s2: valid_read_string(s2)
-.	kgflags.h	611	_kgflags_get_flag	precondition of strstr	Unknown	valid_string_haystack: valid_read_string(haystack)
-.	kgflags.h	612	_kgflags_get_flag	precondition of strcmp	Unknown	valid_string_s1: valid_read_string(s1)
 .	kgflags.h	612	_kgflags_get_flag	precondition of strcmp	Unknown	valid_string_s2: valid_read_string(s2)
 .	kgflags.h	626	_kgflags_parse_int	precondition of strtol	Unknown	valid_string_nptr: valid_read_string(nptr)
-.	kgflags.h	627	_kgflags_parse_int	ptr_comparison	Unknown	\pointer_comparable((void *)end, (void *)str)
 .	kgflags.h	639	_kgflags_parse_double	precondition of strtod	Unknown	valid_string_nptr: valid_read_string(nptr)
-.	kgflags.h	640	_kgflags_parse_double	ptr_comparison	Unknown	\pointer_comparable((void *)end, (void *)str)
 .	kgflags.h	641	_kgflags_parse_double	is_nan_or_infinite	Unknown	\is_finite(res)
 .	kgflags.h	641	_kgflags_parse_double	is_nan_or_infinite	Invalid or unreachable	\is_finite((float)INFINITY)
 .	kgflags.h	675	_kgflags_assign_default_values	mem_access	Unknown	\valid(flag->result.bool_value)
@@ -81,7 +77,6 @@ FRAMAC_SHARE/libc	stdlib.h	99	strtod	precondition	Unknown	valid_string_nptr: val
 FRAMAC_SHARE/libc	stdlib.h	166	strtol	precondition	Unknown	valid_string_nptr: valid_read_string(nptr)
 FRAMAC_SHARE/libc	string.h	153	strcmp	precondition	Unknown	valid_string_s1: valid_read_string(s1)
 FRAMAC_SHARE/libc	string.h	154	strcmp	precondition	Unknown	valid_string_s2: valid_read_string(s2)
-FRAMAC_SHARE/libc	string.h	236	strstr	precondition	Unknown	valid_string_haystack: valid_read_string(haystack)
 examples	full_api.c	34	main	precondition of printf_va_1	Unknown	valid_read_string(param0)
 examples	full_api.c	37	main	is_nan_or_infinite	Unknown	\is_finite(double_val)
 examples	full_api.c	41	main	precondition of printf_va_6	Unknown	valid_read_string(param1)

kgflags/.frama-c/kgflags-full_api.eva/warnings.log

@@ -26,12 +26,12 @@ fc_stubs.c:21:[eva:locals-escaping] warning: locals {double_arr} escaping the sc
   kgflags.h:735: imprecise merge of addresses
     (read in 4 statements, propagated through 8 statements)
     garbled mix of &{argv}
+  kgflags.h:522: misaligned read of addresses
+    (read in 2 statements, propagated through 3 statements)
+    garbled mix of &{argv0; argv1; argv2; argv3; argv4}
   kgflags.h:533: misaligned read of addresses
-    (read in 3 statements, propagated through 3 statements)
+    (read in 2 statements, propagated through 3 statements)
     garbled mix of &{argv0; argv1; argv2; argv3; argv4}
   kgflags.h:550: misaligned read of addresses
-    (read in 3 statements, propagated through 3 statements)
-    garbled mix of &{argv0; argv1; argv2; argv3; argv4}
-  kgflags.h:522: misaligned read of addresses
     (read in 2 statements, propagated through 3 statements)
     garbled mix of &{argv0; argv1; argv2; argv3; argv4}

libspng/.frama-c/libspng-example.eva/warnings.log

@@ -12,14 +12,11 @@ stack: memcpy :: spng.c:948 <-
     garbled mix of &{__malloc_w_spng__malloc_l220_0;
                      __malloc_w_spng__malloc_l220_2;
                      __malloc_w_spng__malloc_l220_4}
+  spng.c:1483: imprecise merge of addresses
+    (read in 2 statements, propagated through 0 statements)
+    garbled mix of &{__malloc_w_spng__malloc_l220_0}
   spng.c:950: misaligned read of addresses
     (read in 2 statements, propagated through 0 statements)
     garbled mix of &{__malloc_w_spng__malloc_l220_0;
                      __malloc_w_spng__malloc_l220_2;
                      __malloc_w_spng__malloc_l220_4}
-  spng.c:1406: imprecise merge of addresses
-    (read in 1 statement, propagated through 0 statements)
-    garbled mix of &{__malloc_w_spng__malloc_l220_0}
-  spng.c:1483: imprecise merge of addresses
-    (read in 1 statement, propagated through 0 statements)
-    garbled mix of &{__malloc_w_spng__malloc_l220_0}

microstrain/.frama-c/microstrain_gx4_45_test.eva/warnings.log

@@ -26,7 +26,7 @@ stack: mip_3dm_cmd_ahrs_message_format :: MIPSDK/C/Examples/Linux/GX4-45/GX4_45_
        eva_main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   MIPSDK/C/Library/Source/ring_buffer.c:438: misaligned read of addresses
-    (read in 460 statements, propagated through 553 statements)
+    (read in 458 statements, propagated through 553 statements)
     garbled mix of &{__mip_interface_command_response_handler;
                      device_interface; mip_sdk_port_open_local_port_handle}
   MIPSDK/C/Library/Source/ring_buffer.c:511: misaligned read of addresses

miniz/.frama-c/miniz-example1.eva/alarms.csv

@@ -625,6 +625,8 @@ directory	file	line	function	property kind	status	property
 .	miniz_tdef.c	608	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_dict_size)
 .	miniz_tdef.c	608	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_lookahead_pos)
 .	miniz_tdef.c	608	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_lz_code_buf_dict_pos)
+.	miniz_tdef.c	609	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_pOut_buf)
+.	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pOut_buf)
 .	miniz_tdef.c	609	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_pPut_buf_func)
 .	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pPut_buf_func)
 .	miniz_tdef.c	609	tdefl_flush_block	ptr_comparison	Unknown	\pointer_comparable((void (*)())d->m_pPut_buf_func, (void (*)())0)
@@ -635,8 +637,6 @@ directory	file	line	function	property kind	status	property
 .	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pOut_buf_size)
 .	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(d->m_pOut_buf_size)
 .	miniz_tdef.c	609	tdefl_flush_block	mem_access	Unknown	\valid_read(d->m_pOut_buf_size)
-.	miniz_tdef.c	609	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_pOut_buf)
-.	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pOut_buf)
 .	miniz_tdef.c	612	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_pOutput_buf)
 .	miniz_tdef.c	612	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pOutput_buf)
 .	miniz_tdef.c	614	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_output_flush_remaining)

miniz/.frama-c/miniz-example2.eva/alarms.csv

@@ -622,6 +622,8 @@ directory	file	line	function	property kind	status	property
 .	miniz_tdef.c	608	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_dict_size)
 .	miniz_tdef.c	608	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_lookahead_pos)
 .	miniz_tdef.c	608	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_lz_code_buf_dict_pos)
+.	miniz_tdef.c	609	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_pOut_buf)
+.	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pOut_buf)
 .	miniz_tdef.c	609	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_pPut_buf_func)
 .	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pPut_buf_func)
 .	miniz_tdef.c	609	tdefl_flush_block	ptr_comparison	Unknown	\pointer_comparable((void (*)())d->m_pPut_buf_func, (void (*)())0)
@@ -632,8 +634,6 @@ directory	file	line	function	property kind	status	property
 .	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pOut_buf_size)
 .	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(d->m_pOut_buf_size)
 .	miniz_tdef.c	609	tdefl_flush_block	mem_access	Unknown	\valid_read(d->m_pOut_buf_size)
-.	miniz_tdef.c	609	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_pOut_buf)
-.	miniz_tdef.c	609	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pOut_buf)
 .	miniz_tdef.c	612	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_pOutput_buf)
 .	miniz_tdef.c	612	tdefl_flush_block	initialization	Unknown	\initialized(&d->m_pOutput_buf)
 .	miniz_tdef.c	614	tdefl_flush_block	dangling_pointer	Unknown	¬\dangling(&d->m_output_flush_remaining)