Commit 14fd0be2 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

update (unstable?) oracles

parent 5dc54284
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
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.
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
compcertTSO-1.c:8:[eva:locals-escaping] warning: locals {a} escaping the scope of f through \result<f>
compcertTSO-1.c:8:[eva:locals-escaping] warning: locals {a} escaping the scope of g through \result<g>
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
padding_subunion_1.c:7:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
[eva:garbled-mix] 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}) }}
......
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
provenance_basic_malloc_offset+12.c:4:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
provenance_basic_malloc_offset+12.c:5:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
......
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
provenance_basic_using_intptr_t_auto_yx.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.
provenance_basic_using_intptr_t_auto_yx.c:11:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
......
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
provenance_via_io_bytewise_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.
provenance_via_io_bytewise_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.
provenance_via_io_bytewise_global.c:14:[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.
......
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment