Enables all garbled-mix messages, which have been improved.

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

-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Misaligned {pointer_copy_user_dataflow_direct_bytewise.c:5}) }}
+pointer_copy_user_dataflow_direct_bytewise.c:5:[eva:garbled-mix:write] warning: Assigning imprecise value to *dest because of misaligned read of addresses.
+stack: user_memcpy :: pointer_copy_user_dataflow_direct_bytewise.c:14 <- main
+[eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
+  pointer_copy_user_dataflow_direct_bytewise.c:5: misaligned read of addresses
+    (read 3 times, propagated 4 times) garbled mix of &{x}

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

-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Misaligned {pointer_copy_user_dataflow_indirect_bytewise.c:5}) }}
+pointer_copy_user_dataflow_indirect_bytewise.c:5:[eva:garbled-mix:write] warning: Assigning imprecise value to *dest because of misaligned read of addresses.
+stack: user_memcpy2 :: pointer_copy_user_dataflow_indirect_bytewise.c:14 <-
+       main
+[eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
+  pointer_copy_user_dataflow_indirect_bytewise.c:5: misaligned read of addresses
+    (read 3 times, propagated 4 times) garbled mix of &{x}

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

@@ -2,11 +2,8 @@ pointer_offset_constant_8_malloc.c:4:[kernel] warning: all target addresses were
 stack: main
 pointer_offset_constant_8_malloc.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-pointer_offset_constant_8_malloc.c:12:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+pointer_offset_constant_8_malloc.c:12:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 pointer_offset_constant_8_malloc.c:14:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{__malloc_main_l2}
-  (origin: Misaligned {pointer_offset_constant_8_malloc.c:13}) }}
-{{ garbled mix of &{__malloc_main_l3}
-  (origin: Misaligned {pointer_offset_constant_8_malloc.c:13}) }}

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

-pointer_offset_from_subtraction_1_auto.c:6:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_1_auto.c:12:[eva:garbled-mix:assigns] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_from_subtraction_1_auto.c:5}) }}
-{{ garbled mix of &{y}
-  (origin: Arithmetic {pointer_offset_from_subtraction_1_auto.c:5}) }}
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_from_subtraction_1_auto.c:8}) }}
-{{ garbled mix of &{y}
-  (origin: Misaligned {pointer_offset_from_subtraction_1_auto.c:10}) }}
+pointer_offset_from_subtraction_1_auto.c:5:[eva:garbled-mix:write] warning: Assigning imprecise value to offset
+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 6 times, propagated 5 times) garbled mix of &{x; y}

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

-pointer_offset_from_subtraction_1_global.c:6:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_1_global.c:12:[eva:garbled-mix:assigns] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_from_subtraction_1_global.c:5}) }}
-{{ garbled mix of &{y}
-  (origin: Arithmetic {pointer_offset_from_subtraction_1_global.c:5}) }}
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_from_subtraction_1_global.c:8}) }}
-{{ garbled mix of &{y}
-  (origin: Misaligned {pointer_offset_from_subtraction_1_global.c:10}) }}
+pointer_offset_from_subtraction_1_global.c:5:[eva:garbled-mix:write] warning: Assigning imprecise value to offset
+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 6 times, propagated 5 times) garbled mix of &{y; x}

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

-pointer_offset_from_subtraction_2_auto.c:9:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_2_auto.c:11:[eva:garbled-mix:assigns] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_2_auto.c:18:[eva:garbled-mix:assigns] warning: The specification of function printf_va_3 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_auto.c:5}) }}
-{{ garbled mix of &{y}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_auto.c:5}) }}
-{{ garbled mix of &{z}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_auto.c:8}) }}
-{{ garbled mix of &{w}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_auto.c:8}) }}
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_auto.c:14}) }}
-{{ garbled mix of &{y}
-  (origin: Misaligned {pointer_offset_from_subtraction_2_auto.c:16}) }}
+pointer_offset_from_subtraction_2_auto.c:5:[eva:garbled-mix:write] warning: Assigning imprecise value to offsetxy
+because of arithmetic operation on addresses.
+stack: main
+pointer_offset_from_subtraction_2_auto.c:8:[eva:garbled-mix:write] warning: Assigning imprecise value to offsetzw
+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 8 times, propagated 3 times) garbled mix of &{w; z; x}
+  pointer_offset_from_subtraction_2_auto.c:5: arithmetic operation on addresses
+    (read 4 times, propagated 5 times) garbled mix of &{w; z; y; x}

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

-pointer_offset_from_subtraction_2_global.c:9:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_2_global.c:11:[eva:garbled-mix:assigns] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_2_global.c:18:[eva:garbled-mix:assigns] warning: The specification of function printf_va_3 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_global.c:5}) }}
-{{ garbled mix of &{y}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_global.c:5}) }}
-{{ garbled mix of &{z}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_global.c:8}) }}
-{{ garbled mix of &{w}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_global.c:8}) }}
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_from_subtraction_2_global.c:14}) }}
-{{ garbled mix of &{y}
-  (origin: Misaligned {pointer_offset_from_subtraction_2_global.c:16}) }}
+pointer_offset_from_subtraction_2_global.c:5:[eva:garbled-mix:write] warning: Assigning imprecise value to offsetxy
+because of arithmetic operation on addresses.
+stack: main
+pointer_offset_from_subtraction_2_global.c:8:[eva:garbled-mix:write] warning: Assigning imprecise value to offsetzw
+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 8 times, propagated 3 times) garbled mix of &{w; z; x}
+  pointer_offset_from_subtraction_2_global.c:5: arithmetic operation on addresses
+    (read 4 times, propagated 5 times) garbled mix of &{w; z; y; x}

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

-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{y} (origin: Arithmetic {pointer_offset_xor_auto.c:7}) }}
-{{ garbled mix of &{x} (origin: Arithmetic {pointer_offset_xor_auto.c:7}) }}
-{{ garbled mix of &{x} (origin: Arithmetic {pointer_offset_xor_auto.c:8}) }}
+pointer_offset_xor_auto.c:7:[eva:garbled-mix:write] warning: Assigning imprecise value to k because of arithmetic operation on addresses.
+stack: main
+[eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
+  pointer_offset_xor_auto.c:7: arithmetic operation on addresses
+    (read 5 times, propagated 3 times) garbled mix of &{x; y}

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

-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{y}
-  (origin: Arithmetic {pointer_offset_xor_global.c:8}) }}
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_xor_global.c:8}) }}
-{{ garbled mix of &{x}
-  (origin: Arithmetic {pointer_offset_xor_global.c:9}) }}
+pointer_offset_xor_global.c:8:[eva:garbled-mix:write] warning: Assigning imprecise value to k because of arithmetic operation on addresses.
+stack: main
+[eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
+  pointer_offset_xor_global.c:8: arithmetic operation on addresses
+    (read 5 times, propagated 3 times) garbled mix of &{x; y}

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

-provenance_basic_auto_xy.c:5:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_auto_xy.c:5:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_auto_xy.c:7:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x} (origin: Misaligned {provenance_basic_auto_xy.c:6}) }}
-{{ garbled mix of &{y} (origin: Misaligned {provenance_basic_auto_xy.c:6}) }}

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

-provenance_basic_auto_yx.c:5:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_auto_yx.c:5:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_auto_yx.c:7:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x} (origin: Misaligned {provenance_basic_auto_yx.c:6}) }}
-{{ garbled mix of &{y} (origin: Misaligned {provenance_basic_auto_yx.c:6}) }}

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

-provenance_basic_global_xy.c:5:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_global_xy.c:5:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_global_xy.c:7:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Misaligned {provenance_basic_global_xy.c:6}) }}
-{{ garbled mix of &{y}
-  (origin: Misaligned {provenance_basic_global_xy.c:6}) }}

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

-provenance_basic_global_yx.c:5:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_global_yx.c:5:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_global_yx.c:7:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Misaligned {provenance_basic_global_yx.c:6}) }}
-{{ garbled mix of &{y}
-  (origin: Misaligned {provenance_basic_global_yx.c:6}) }}

cerberus/.frama-c/provenance_basic_malloc_offset+12.eva/warnings.log

@@ -2,11 +2,8 @@ provenance_basic_malloc_offset+12.c:4:[kernel] warning: all target addresses wer
 stack: main
 provenance_basic_malloc_offset+12.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-provenance_basic_malloc_offset+12.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_malloc_offset+12.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_malloc_offset+12.c:11:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{__malloc_main_l2}
-  (origin: Misaligned {provenance_basic_malloc_offset+12.c:10}) }}
-{{ garbled mix of &{__malloc_main_l3}
-  (origin: Misaligned {provenance_basic_malloc_offset+12.c:10}) }}

cerberus/.frama-c/provenance_basic_malloc_offset+2.eva/warnings.log

@@ -2,11 +2,8 @@ provenance_basic_malloc_offset+2.c:4:[kernel] warning: all target addresses were
 stack: main
 provenance_basic_malloc_offset+2.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-provenance_basic_malloc_offset+2.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_malloc_offset+2.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_malloc_offset+2.c:11:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{__malloc_main_l2}
-  (origin: Misaligned {provenance_basic_malloc_offset+2.c:10}) }}
-{{ garbled mix of &{__malloc_main_l3}
-  (origin: Misaligned {provenance_basic_malloc_offset+2.c:10}) }}

cerberus/.frama-c/provenance_basic_malloc_offset+4.eva/warnings.log

@@ -2,11 +2,8 @@ provenance_basic_malloc_offset+4.c:4:[kernel] warning: all target addresses were
 stack: main
 provenance_basic_malloc_offset+4.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-provenance_basic_malloc_offset+4.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_malloc_offset+4.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_malloc_offset+4.c:11:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{__malloc_main_l2}
-  (origin: Misaligned {provenance_basic_malloc_offset+4.c:10}) }}
-{{ garbled mix of &{__malloc_main_l3}
-  (origin: Misaligned {provenance_basic_malloc_offset+4.c:10}) }}

cerberus/.frama-c/provenance_basic_malloc_offset+8.eva/warnings.log

@@ -2,11 +2,8 @@ provenance_basic_malloc_offset+8.c:4:[kernel] warning: all target addresses were
 stack: main
 provenance_basic_malloc_offset+8.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-provenance_basic_malloc_offset+8.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_malloc_offset+8.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_malloc_offset+8.c:11:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{__malloc_main_l2}
-  (origin: Misaligned {provenance_basic_malloc_offset+8.c:10}) }}
-{{ garbled mix of &{__malloc_main_l3}
-  (origin: Misaligned {provenance_basic_malloc_offset+8.c:10}) }}

cerberus/.frama-c/provenance_basic_malloc_offset-4.eva/warnings.log

@@ -2,11 +2,8 @@ provenance_basic_malloc_offset-4.c:4:[kernel] warning: all target addresses were
 stack: main
 provenance_basic_malloc_offset-4.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-provenance_basic_malloc_offset-4.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_malloc_offset-4.c:8:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_malloc_offset-4.c:11:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{__malloc_main_l2}
-  (origin: Misaligned {provenance_basic_malloc_offset-4.c:10}) }}
-{{ garbled mix of &{__malloc_main_l3}
-  (origin: Misaligned {provenance_basic_malloc_offset-4.c:10}) }}

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

-provenance_basic_mixed_auto.c:6:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_mixed_auto.c:6:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_mixed_auto.c:12:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Misaligned {provenance_basic_mixed_auto.c:11}) }}
-{{ garbled mix of &{y}
-  (origin: Misaligned {provenance_basic_mixed_auto.c:11}) }}

cerberus/.frama-c/provenance_basic_mixed_auto_offset+4.eva/warnings.log

-provenance_basic_mixed_auto_offset+4.c:6:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_mixed_auto_offset+4.c:6:[eva:garbled-mix:assigns] warning: The specification of function printf_va_1
+has generated a garbled mix of addresses
+for assigns clause __fc_stdout->__fc_FILE_data.
 provenance_basic_mixed_auto_offset+4.c:12:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
-[eva:garbled-mix:summary] warning: Garbled mix generated during analysis:
-{{ garbled mix of &{x}
-  (origin: Misaligned {provenance_basic_mixed_auto_offset+4.c:11}) }}
-{{ garbled mix of &{y}
-  (origin: Misaligned {provenance_basic_mixed_auto_offset+4.c:11}) }}