Merge branch 'sync/master' into 'master'

synchronize with frama-c master

See merge request !52

basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast

 /* Generated by Frama-C */
+#include "errno.h"
 #include "stdlib.h"
 size_t volatile _rand;
 size_t random_size_t(void)

basic-cwe-examples/.frama-c/cwe190-unsigned.parse/framac.ast

 /* Generated by Frama-C */
+#include "errno.h"
 #include "stdlib.h"
 long volatile _rand;
 long random_long(void)

basic-cwe-examples/.frama-c/cwe190.parse/framac.ast

 /* Generated by Frama-C */
+#include "errno.h"
 #include "stdlib.h"
 size_t volatile _rand;
 size_t random_size_t(void)

basic-cwe-examples/.frama-c/cwe761-precise.eva/alarms.csv

 directory	file	line	function	property kind	status	property
 .	cwe761.c	24	contains_char	precondition of free	Invalid or unreachable	freeable: p ≡ \null ∨ \freeable(p)
-FRAMAC_SHARE/libc	stdlib.h	405	free	precondition	Invalid or unreachable	freeable: p ≡ \null ∨ \freeable(p)
+FRAMAC_SHARE/libc	stdlib.h	406	free	precondition	Invalid or unreachable	freeable: p ≡ \null ∨ \freeable(p)

basic-cwe-examples/.frama-c/cwe761.eva/alarms.csv

@@ -2,4 +2,4 @@ directory	file	line	function	property kind	status	property
 .	cwe761.c	21	contains_char	initialization	Unknown	\initialized(str)
 .	cwe761.c	24	contains_char	precondition of free	Unknown	freeable: p ≡ \null ∨ \freeable(p)
 .	cwe761.c	32	contains_char	precondition of free	Unknown	freeable: p ≡ \null ∨ \freeable(p)
-FRAMAC_SHARE/libc	stdlib.h	405	free	precondition	Unknown	freeable: p ≡ \null ∨ \freeable(p)
+FRAMAC_SHARE/libc	stdlib.h	406	free	precondition	Unknown	freeable: p ≡ \null ∨ \freeable(p)

basic-cwe-examples/.frama-c/cwe761.parse/framac.ast

 /* Generated by Frama-C */
+#include "errno.h"
 #include "stdlib.h"
 #include "string.h"
 #include "strings.h"

basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast

 /* Generated by Frama-C */
+#include "errno.h"
 #include "stdlib.h"
 #include "string.h"
 #include "strings.h"

basic-cwe-examples/.frama-c/cwe787.parse/framac.ast

 /* Generated by Frama-C */
+#include "errno.h"
 #include "stdlib.h"
 #include "string.h"
 #include "strings.h"

c-testsuite/.frama-c/00040.parse/framac.ast

 /* Generated by Frama-C */
+#include "errno.h"
 #include "stdlib.h"
 int N;
 int *t;

c-utils/.frama-c/ex_stringlib.eva/warnings.log

@@ -2,5 +2,5 @@ src/stringlib.c:314:[eva:garbled-mix:assigns] warning: The specification of func
 has generated a garbled mix of addresses for assigns clause \result.
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   src/stringlib.c:314: assigns clause on addresses
-    (read 18 times, propagated 12 times)
+    (read in 4 statements, propagated through 5 statements)
     garbled mix of &{__realloc_s_append_alt_l383}

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

@@ -4,4 +4,5 @@ besson_blazy_wilkie_Fig_2.c:14:[eva:garbled-mix:write] warning: Assigning imprec
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   besson_blazy_wilkie_Fig_2.c:14: arithmetic operation on addresses
-    (read 3 times, propagated 1 times) garbled mix of &{__malloc_main_l11}
+    (read in 1 statement, propagated through 1 statement)
+    garbled mix of &{__malloc_main_l11}

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

@@ -2,4 +2,5 @@ cheri_06_mask.c:11:[eva:garbled-mix:write] warning: Assigning imprecise value to
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   cheri_06_mask.c:11: arithmetic operation on addresses
-    (read 6 times, propagated 4 times) garbled mix of &{x}
+    (read in 4 statements, propagated through 4 statements)
+    garbled mix of &{x}

cerberus/.frama-c/khmgzv-1.eva/warnings.log

@@ -5,4 +5,5 @@ khmgzv-1.c:8:[eva:garbled-mix:write] warning: Assigning imprecise value to a bec
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   khmgzv-1.c:8: arithmetic operation on addresses
-    (read 4 times, propagated 2 times) garbled mix of &{x}
+    (read in 2 statements, propagated through 2 statements)
+    garbled mix of &{x}

cerberus/.frama-c/klw-itp14-1.eva/warnings.log

@@ -5,4 +5,5 @@ because of misaligned read of addresses.
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   klw-itp14-1.c:4: misaligned read of addresses
-    (read 3 times, propagated 4 times) garbled mix of &{s}
+    (read in 1 statement, propagated through 1 statement) garbled mix of &
+    {s}

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

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

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

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

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

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

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

@@ -5,4 +5,5 @@ pointer_copy_user_ctrlflow_bitwise.c:17:[kernel] warning: all target addresses w
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   pointer_copy_user_ctrlflow_bitwise.c:10: arithmetic operation on addresses
-    (read 8234 times, propagated 4116 times) garbled mix of &{x}
+    (read in 1 statement, propagated through 1 statement) garbled mix of &
+    {x}

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

@@ -6,4 +6,5 @@ pointer_copy_user_ctrlflow_bytewise.c:278:[kernel] warning: all target addresses
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   pointer_copy_user_ctrlflow_bytewise.c:267: misaligned read of addresses
-    (read 1024 times, propagated 4 times) garbled mix of &{x}
+    (read in 1 statement, propagated through 1 statement) garbled mix of &
+    {x}

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

@@ -6,4 +6,5 @@ pointer_copy_user_ctrlflow_bytewise_abbrev.c:25:[kernel] warning: all target add
 stack: main
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
   pointer_copy_user_ctrlflow_bytewise_abbrev.c:14: misaligned read of addresses
-    (read 16 times, propagated 4 times) garbled mix of &{x}
+    (read in 1 statement, propagated through 1 statement) garbled mix of &
+    {x}