sync with frama-c master

2048/.frama-c/GNUmakefile

@@ -4,7 +4,7 @@
 ### Prologue. Do not modify this block. #######################################
 -include path.mk
 FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
 # Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
@@ -37,7 +37,7 @@ TARGETS = 2048.eva
   ../2048.c \
 
 ### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
 ###############################################################################
 
 # optional, for OSCS

basic-cwe-examples/.frama-c/GNUmakefile

@@ -4,7 +4,7 @@
 ### Prologue. Do not modify this block. #######################################
 -include path.mk
 FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
 # Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
@@ -51,7 +51,7 @@ cwe416-precise.eva: EVAFLAGS += -eva-precision 1
 cwe787-precise.eva: EVAFLAGS += -eva-precision 2 -eva-no-alloc-returns-null
 
 ### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
 ###############################################################################
 
 # optional, for OSCS

bench-moerman2018/.frama-c/GNUmakefile

@@ -4,7 +4,7 @@
 ### Prologue. Do not modify this block. #######################################
 -include path.mk
 FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
 # Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
@@ -69,7 +69,7 @@ evaluate: eval_summary.txt
 all: evaluate
 
 ### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
 ###############################################################################
 
 # optional, for OSCS

cerberus/.frama-c/GNUmakefile

@@ -4,7 +4,7 @@
 ### Prologue. Do not modify this block. #######################################
 -include path.mk
 FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -scripts)/prologue.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
 # Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
@@ -432,7 +432,7 @@ unspecified_value_union_1.parse: ../unspecified_value_union_1.c
 write_union_same_prefix_visible.parse: ../write_union_same_prefix_visible.c
 
 ### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
 ###############################################################################
 
 # optional, for OSCS

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

-cheri_07_wide.c:10:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-cheri_07_wide.c:12:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+cheri_07_wide.c:10:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+cheri_07_wide.c:12:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.

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

-khmgzv-1.c:5:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-khmgzv-1.c:11:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+khmgzv-1.c:5:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+khmgzv-1.c:11:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 [eva:garbled-mix] warning: Garbled mix generated during analysis:
 {{ garbled mix of &{x} (origin: Misaligned {khmgzv-1.c:7}) }}
 {{ garbled mix of &{x} (origin: Arithmetic {khmgzv-1.c:8}) }}

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

-khmgzv-2.c:5:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+khmgzv-2.c:5:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 khmgzv-2.c:9:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
 [eva:garbled-mix] warning: Garbled mix generated during analysis:

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

-pointer_add_wrap_1.c:8:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_add_wrap_1.c:10:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_add_wrap_1.c:8:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+pointer_add_wrap_1.c:10:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.

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

-pointer_comparison_7b.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_7b.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 pointer_comparison_7b.c:6:[eva:locals-escaping] warning: locals {j} escaping the scope of a block of main through pj
 pointer_comparison_7b.c:6:[eva:locals-escaping] warning: locals {j} escaping the scope of a block of main through S___fc_stdout
-pointer_comparison_7b.c:12:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_7b.c:12:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 pointer_comparison_7b.c:14:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main

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

-pointer_comparison_7c.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_7c.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 pointer_comparison_7c.c:6:[eva:locals-escaping] warning: locals {j} escaping the scope of a block of main through pj
 pointer_comparison_7c.c:6:[eva:locals-escaping] warning: locals {j} escaping the scope of a block of main through S___fc_stdout
-pointer_comparison_7c.c:13:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_7c.c:13:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 pointer_comparison_7c.c:14:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main

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

-pointer_comparison_rel_1_auto.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_comparison_rel_1_auto.c:7:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_rel_1_auto.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_rel_1_auto.c:7:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.

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

-pointer_comparison_rel_1_global.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_comparison_rel_1_global.c:7:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_rel_1_global.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_rel_1_global.c:7:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.

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

-pointer_comparison_rel_different_type_members.c:7:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_comparison_rel_different_type_members.c:8:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_rel_different_type_members.c:7:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_rel_different_type_members.c:8:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.

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

-pointer_comparison_rel_substruct.c:7:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_comparison_rel_substruct.c:8:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_rel_substruct.c:7:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
+pointer_comparison_rel_substruct.c:8:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.

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

@@ -2,7 +2,7 @@ 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] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_offset_constant_8_malloc.c:12:[eva:garbled-mix] 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:14:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
 [eva:garbled-mix] warning: Garbled mix generated during analysis:

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

-pointer_offset_from_subtraction_1_auto.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_1_auto.c:12:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_offset_from_subtraction_1_auto.c:6:[eva:garbled-mix] 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] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 [eva:garbled-mix] warning: Garbled mix generated during analysis:
 {{ garbled mix of &{x}
   (origin: Arithmetic {pointer_offset_from_subtraction_1_auto.c:5}) }}

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

-pointer_offset_from_subtraction_1_global.c:6:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_1_global.c:12:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_offset_from_subtraction_1_global.c:6:[eva:garbled-mix] 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] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 [eva:garbled-mix] warning: Garbled mix generated during analysis:
 {{ garbled mix of &{x}
   (origin: Arithmetic {pointer_offset_from_subtraction_1_global.c:5}) }}

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

-pointer_offset_from_subtraction_2_auto.c:9:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_2_auto.c:11:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_2_auto.c:18:[eva:garbled-mix] warning: The specification of function printf_va_3 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_offset_from_subtraction_2_auto.c:9:[eva:garbled-mix] 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] 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] warning: The specification of function printf_va_3 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 [eva:garbled-mix] warning: Garbled mix generated during analysis:
 {{ garbled mix of &{x}
   (origin: Arithmetic {pointer_offset_from_subtraction_2_auto.c:5}) }}

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

-pointer_offset_from_subtraction_2_global.c:9:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_2_global.c:11:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
-pointer_offset_from_subtraction_2_global.c:18:[eva:garbled-mix] warning: The specification of function printf_va_3 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+pointer_offset_from_subtraction_2_global.c:9:[eva:garbled-mix] 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] 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] warning: The specification of function printf_va_3 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
 [eva:garbled-mix] warning: Garbled mix generated during analysis:
 {{ garbled mix of &{x}
   (origin: Arithmetic {pointer_offset_from_subtraction_2_global.c:5}) }}

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

-provenance_basic_auto_xy.c:5:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
+provenance_basic_auto_xy.c:5:[eva:garbled-mix] 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:7:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main
 [eva:garbled-mix] warning: Garbled mix generated during analysis: