From 097ebb6a20eecd6676ba65134067fbea89899afc Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 6 Apr 2021 17:01:58 +0200
Subject: [PATCH] [Value] adds test oracles for -config symblocs
---
tests/test_config_symblocs | 4 ++
.../oracle_symblocs/CruiseControl.res.oracle | 0
tests/value/oracle_symblocs/FP5.res.oracle | 0
tests/value/oracle_symblocs/abs.res.oracle | 0
.../value/oracle_symblocs/abs_addr.res.oracle | 0
.../absolute_pointer.res.oracle | 0
.../abstract_struct_1.res.oracle | 0
.../oracle_symblocs/access_path.res.oracle | 0
.../oracle_symblocs/add_approx.res.oracle | 0
.../value/oracle_symblocs/addition.res.oracle | 0
tests/value/oracle_symblocs/addr.0.res.oracle | 0
tests/value/oracle_symblocs/addr.1.res.oracle | 0
tests/value/oracle_symblocs/addr2.res.oracle | 0
.../oracle_symblocs/addrofstring.res.oracle | 0
.../affect_corrupt.0.res.oracle | 0
.../affect_corrupt.1.res.oracle | 0
.../value/oracle_symblocs/ai_annot.res.oracle | 0
.../value/oracle_symblocs/alias.0.res.oracle | 10 +++
.../value/oracle_symblocs/alias.1.res.oracle | 0
.../value/oracle_symblocs/alias.2.res.oracle | 0
.../value/oracle_symblocs/alias.3.res.oracle | 0
.../value/oracle_symblocs/alias.4.res.oracle | 4 ++
.../value/oracle_symblocs/alias.5.res.oracle | 4 ++
.../value/oracle_symblocs/alias.6.res.oracle | 4 ++
tests/value/oracle_symblocs/align.res.oracle | 0
.../align_char_array.res.oracle | 0
tests/value/oracle_symblocs/annot.res.oracle | 0
.../oracle_symblocs/annot_valid.res.oracle | 0
.../anonymous_field.res.oracle | 0
.../value/oracle_symblocs/any_int.res.oracle | 0
tests/value/oracle_symblocs/arch.res.oracle | 0
.../oracle_symblocs/arg_array.res.oracle | 0
.../oracle_symblocs/arith_pointer.res.oracle | 0
.../oracle_symblocs/array_access.res.oracle | 0
.../oracle_symblocs/array_array.0.res.oracle | 0
.../oracle_symblocs/array_array.1.res.oracle | 0
.../oracle_symblocs/array_array.2.res.oracle | 0
.../oracle_symblocs/array_bounds.0.res.oracle | 0
.../oracle_symblocs/array_bounds.1.res.oracle | 0
.../array_degenerating_loop.res.oracle | 0
.../array_initializer.res.oracle | 0
.../oracle_symblocs/array_loop.res.oracle | 0
.../oracle_symblocs/array_overlap.res.oracle | 0
.../oracle_symblocs/array_ptr.res.oracle | 0
.../array_zero_length.0.res.oracle | 0
.../array_zero_length.1.res.oracle | 0
.../array_zero_length.2.res.oracle | 0
.../oracle_symblocs/asm_contracts.res.oracle | 0
.../oracle_symblocs/assert_ptr.res.oracle | 0
.../assign-leaf-indirect.res.oracle | 0
.../value/oracle_symblocs/assigns.res.oracle | 0
.../oracle_symblocs/assigns_from.res.oracle | 0
.../assigns_from_direct.res.oracle | 0
.../attribute-aligned.res.oracle | 0
tests/value/oracle_symblocs/audit.res.oracle | 11 +++
.../auto_loop_unroll.0.res.oracle | 0
.../auto_loop_unroll.1.res.oracle | 0
.../oracle_symblocs/automalloc.res.oracle | 0
.../backward_add_ptr.res.oracle | 0
.../oracle_symblocs/backward_arith.res.oracle | 0
.../value/oracle_symblocs/bad_loop.res.oracle | 0
.../base_addr_offset_block_length.res.oracle | 0
.../behavior_statuses.0.res.oracle | 0
.../behavior_statuses.1.res.oracle | 0
.../oracle_symblocs/behaviors1.res.oracle | 0
.../oracle_symblocs/behaviors2.res.oracle | 0
.../oracle_symblocs/big_lib_entry.res.oracle | 0
.../value/oracle_symblocs/bigarray.res.oracle | 0
.../value/oracle_symblocs/bitfield.res.oracle | 0
.../bitfield_assign.res.oracle | 0
.../bitfield_longlong.res.oracle | 0
.../bitfield_receives_result.res.oracle | 0
.../value/oracle_symblocs/bitwise.res.oracle | 0
.../oracle_symblocs/bitwise_float.res.oracle | 0
.../bitwise_pointer.res.oracle | 8 +++
.../bitwise_reduction.res.oracle | 16 +++++
tests/value/oracle_symblocs/biz.res.oracle | 0
tests/value/oracle_symblocs/bool.res.oracle | 0
tests/value/oracle_symblocs/branch.res.oracle | 0
.../value/oracle_symblocs/branch2.res.oracle | 0
.../oracle_symblocs/broken_loop.res.oracle | 0
.../oracle_symblocs/bts0506.0.res.oracle | 0
.../oracle_symblocs/bts0506.1.res.oracle | 0
.../value/oracle_symblocs/bts0775.res.oracle | 0
.../value/oracle_symblocs/bts0858.res.oracle | 0
.../value/oracle_symblocs/bts1306.res.oracle | 0
.../buffer_overflow.0.res.oracle | 0
.../buffer_overflow.1.res.oracle | 0
tests/value/oracle_symblocs/bug.res.oracle | 0
.../value/oracle_symblocs/bug0196.res.oracle | 0
.../oracle_symblocs/bug0223.0.res.oracle | 0
.../oracle_symblocs/bug0223.1.res.oracle | 0
.../value/oracle_symblocs/bug0245.res.oracle | 0
.../value/oracle_symblocs/bug_023.res.oracle | 0
.../value/oracle_symblocs/bug_0244.res.oracle | 0
.../oracle_symblocs/builtins_split.res.oracle | 0
tests/value/oracle_symblocs/call.res.oracle | 0
tests/value/oracle_symblocs/call_2.res.oracle | 0
tests/value/oracle_symblocs/call_3.res.oracle | 0
.../oracle_symblocs/call_alias.0.res.oracle | 0
.../oracle_symblocs/call_alias.1.res.oracle | 0
.../oracle_symblocs/call_alias.2.res.oracle | 0
.../oracle_symblocs/call_deep.res.oracle | 0
.../oracle_symblocs/call_multi.res.oracle | 0
.../oracle_symblocs/call_simple.res.oracle | 0
.../oracle_symblocs/case_analysis.res.oracle | 0
tests/value/oracle_symblocs/cast.res.oracle | 0
tests/value/oracle_symblocs/cast1.res.oracle | 0
tests/value/oracle_symblocs/cast2.res.oracle | 0
.../oracle_symblocs/cast_axalto.res.oracle | 0
.../value/oracle_symblocs/cast_fun.res.oracle | 0
.../oracle_symblocs/cast_hetero.res.oracle | 0
.../oracle_symblocs/cast_return.0.res.oracle | 0
.../oracle_symblocs/cast_return.1.res.oracle | 0
.../oracle_symblocs/cert_exp35_c.res.oracle | 0
.../oracle_symblocs/changeret.res.oracle | 0
tests/value/oracle_symblocs/cmp.res.oracle | 0
.../oracle_symblocs/cmp_ptr.0.res.oracle | 0
.../oracle_symblocs/cmp_ptr.1.res.oracle | 0
.../cmp_ptr_follow_all_branches.0.res.oracle | 0
.../cmp_ptr_follow_all_branches.1.res.oracle | 0
tests/value/oracle_symblocs/cond.res.oracle | 0
.../value/oracle_symblocs/cond2.0.res.oracle | 0
.../value/oracle_symblocs/cond2.1.res.oracle | 0
.../cond_integer_cast_of_float.res.oracle | 0
.../conditional_initializer.res.oracle | 0
tests/value/oracle_symblocs/const.res.oracle | 0
tests/value/oracle_symblocs/const2.res.oracle | 0
.../oracle_symblocs/const_syntax.res.oracle | 0
.../oracle_symblocs/const_typedef.res.oracle | 0
.../constarraystructlibentry.res.oracle | 0
.../oracle_symblocs/context_free.res.oracle | 0
.../context_free_simple.res.oracle | 0
.../oracle_symblocs/context_width.res.oracle | 0
.../value/oracle_symblocs/control.res.oracle | 0
.../oracle_symblocs/conversion.res.oracle | 0
.../oracle_symblocs/copy_paste.res.oracle | 0
...copy_paste_hidden_by_dummy_cast.res.oracle | 0
.../oracle_symblocs/copy_stdin.res.oracle | 0
.../value/oracle_symblocs/dangling.res.oracle | 0
.../oracle_symblocs/dataflow_order.res.oracle | 0
.../oracle_symblocs/dead_code.res.oracle | 0
.../oracle_symblocs/dead_code2.res.oracle | 0
.../oracle_symblocs/dead_inout.res.oracle | 0
.../oracle_symblocs/dead_statuses.res.oracle | 0
.../deep_conditionals.res.oracle | 0
.../oracle_symblocs/degeneration2.res.oracle | 0
tests/value/oracle_symblocs/deps.0.res.oracle | 0
tests/value/oracle_symblocs/deps.1.res.oracle | 0
tests/value/oracle_symblocs/deps.2.res.oracle | 0
.../oracle_symblocs/deps_addr.res.oracle | 0
.../oracle_symblocs/deps_compose.res.oracle | 0
.../oracle_symblocs/deps_local.res.oracle | 0
.../oracle_symblocs/deps_mixed.res.oracle | 0
.../deps_unitialized_locals.res.oracle | 0
tests/value/oracle_symblocs/deref.res.oracle | 0
.../oracle_symblocs/descending.res.oracle | 0
.../disjoint_status.res.oracle | 0
tests/value/oracle_symblocs/div.0.res.oracle | 0
tests/value/oracle_symblocs/div.1.res.oracle | 0
.../oracle_symblocs/div_strange.res.oracle | 0
tests/value/oracle_symblocs/divneg.res.oracle | 0
.../value/oracle_symblocs/domains.res.oracle | 0
.../domains_function.res.oracle | 38 ++++++++++
.../oracle_symblocs/downcast.0.res.oracle | 0
.../oracle_symblocs/downcast.1.res.oracle | 0
.../oracle_symblocs/downcast.2.res.oracle | 0
.../oracle_symblocs/downcast.3.res.oracle | 0
.../oracle_symblocs/downcast.4.res.oracle | 0
tests/value/oracle_symblocs/dur.res.oracle | 0
.../oracle_symblocs/empty_base.0.res.oracle | 0
.../oracle_symblocs/empty_base.1.res.oracle | 0
.../oracle_symblocs/empty_struct.0.res.oracle | 0
.../oracle_symblocs/empty_struct.1.res.oracle | 0
.../oracle_symblocs/empty_struct.2.res.oracle | 0
.../oracle_symblocs/empty_struct.3.res.oracle | 0
.../oracle_symblocs/empty_struct.4.res.oracle | 0
.../oracle_symblocs/empty_struct.5.res.oracle | 0
.../oracle_symblocs/empty_struct.6.res.oracle | 0
.../oracle_symblocs/empty_struct2.res.oracle | 0
.../oracle_symblocs/empty_union.res.oracle | 0
.../value/oracle_symblocs/endian.0.res.oracle | 0
.../value/oracle_symblocs/endian.1.res.oracle | 0
tests/value/oracle_symblocs/enum.res.oracle | 0
tests/value/oracle_symblocs/enum2.res.oracle | 0
.../value/oracle_symblocs/equality.res.oracle | 0
.../oracle_symblocs/eval_separated.res.oracle | 0
.../oracle_symblocs/exit_paths.res.oracle | 0
tests/value/oracle_symblocs/extern.res.oracle | 0
tests/value/oracle_symblocs/f1.res.oracle | 0
tests/value/oracle_symblocs/f2.res.oracle | 0
tests/value/oracle_symblocs/false.res.oracle | 0
.../oracle_symblocs/fam_sizeof.res.oracle | 0
.../oracle_symblocs/find_ivaltop.res.oracle | 0
.../value/oracle_symblocs/folding.res.oracle | 0
.../oracle_symblocs/for_loops.0.res.oracle | 0
.../oracle_symblocs/for_loops.1.res.oracle | 0
.../oracle_symblocs/for_loops.2.res.oracle | 0
.../oracle_symblocs/for_loops.3.res.oracle | 0
tests/value/oracle_symblocs/forall.res.oracle | 0
tests/value/oracle_symblocs/fptr.0.res.oracle | 0
tests/value/oracle_symblocs/fptr.1.res.oracle | 0
tests/value/oracle_symblocs/from1.res.oracle | 0
.../oracle_symblocs/from_call.0.res.oracle | 0
.../oracle_symblocs/from_call.1.res.oracle | 0
.../oracle_symblocs/from_global.res.oracle | 0
.../value/oracle_symblocs/from_ind.res.oracle | 0
.../oracle_symblocs/from_pb.0.res.oracle | 0
.../oracle_symblocs/from_pb.1.res.oracle | 0
.../oracle_symblocs/from_pb.2.res.oracle | 0
.../oracle_symblocs/from_pb.3.res.oracle | 0
.../oracle_symblocs/from_pb.4.res.oracle | 0
.../oracle_symblocs/from_pb.5.res.oracle | 0
.../oracle_symblocs/from_pb.6.res.oracle | 0
.../oracle_symblocs/from_pb.7.res.oracle | 0
.../oracle_symblocs/from_ptr.0.res.oracle | 0
.../oracle_symblocs/from_ptr.1.res.oracle | 0
.../oracle_symblocs/from_ptr2.res.oracle | 0
.../oracle_symblocs/from_res_2.res.oracle | 0
.../oracle_symblocs/from_termin.res.oracle | 0
.../oracle_symblocs/fun_ptr.0.res.oracle | 0
.../oracle_symblocs/fun_ptr.1.res.oracle | 0
.../function_return_serial_casts.res.oracle | 0
tests/value/oracle_symblocs/g1.res.oracle | 0
.../oracle_symblocs/garbled_init.res.oracle | 0
tests/value/oracle_symblocs/gauges.res.oracle | 0
tests/value/oracle_symblocs/ghost.res.oracle | 0
.../oracle_symblocs/global_bug.res.oracle | 0
tests/value/oracle_symblocs/goto.res.oracle | 0
.../hierarchical_convergence.res.oracle | 0
tests/value/oracle_symblocs/if.0.res.oracle | 0
tests/value/oracle_symblocs/if.1.res.oracle | 0
tests/value/oracle_symblocs/if2.res.oracle | 0
tests/value/oracle_symblocs/ilevel.res.oracle | 0
.../value/oracle_symblocs/implies.res.oracle | 0
.../imprecise_invalid_write.res.oracle | 0
.../incompatible_states.res.oracle | 7 ++
.../incorrect_reduce_expr.res.oracle | 0
tests/value/oracle_symblocs/ineq.res.oracle | 0
.../value/oracle_symblocs/infinite.res.oracle | 0
tests/value/oracle_symblocs/init.0.res.oracle | 0
tests/value/oracle_symblocs/init.1.res.oracle | 0
.../init_const_guard.res.oracle | 0
.../oracle_symblocs/initialized.res.oracle | 0
.../initialized_copy.0.res.oracle | 0
.../initialized_copy.1.res.oracle | 0
.../value/oracle_symblocs/inout.0.res.oracle | 0
.../value/oracle_symblocs/inout.1.res.oracle | 0
.../value/oracle_symblocs/inout.2.res.oracle | 0
.../value/oracle_symblocs/inout.3.res.oracle | 0
.../value/oracle_symblocs/inout.4.res.oracle | 0
.../oracle_symblocs/inout_diff.res.oracle | 0
.../oracle_symblocs/inout_formals.res.oracle | 0
.../inout_on_alarms.res.oracle | 0
.../oracle_symblocs/inout_proto.res.oracle | 0
tests/value/oracle_symblocs/input.res.oracle | 0
.../value/oracle_symblocs/integers.res.oracle | 0
.../value/oracle_symblocs/interpol.res.oracle | 0
.../interpreter-mode-syracuse.res.oracle | 0
.../invalid_loc_return.res.oracle | 0
.../invalid_lval_arg.res.oracle | 0
.../invalid_pointer.0.res.oracle | 0
.../invalid_pointer.1.res.oracle | 0
.../oracle_symblocs/inversion.res.oracle | 0
.../oracle_symblocs/inversion2.res.oracle | 0
.../value/oracle_symblocs/jacques.res.oracle | 0
.../join_misaligned.res.oracle | 0
tests/value/oracle_symblocs/label.res.oracle | 0
tests/value/oracle_symblocs/lazy.0.res.oracle | 0
tests/value/oracle_symblocs/lazy.1.res.oracle | 0
tests/value/oracle_symblocs/leaf.res.oracle | 0
tests/value/oracle_symblocs/leaf2.res.oracle | 0
.../oracle_symblocs/leaf_spec.0.res.oracle | 0
.../oracle_symblocs/leaf_spec.1.res.oracle | 0
.../value/oracle_symblocs/library.res.oracle | 5 ++
.../library_precond.res.oracle | 0
tests/value/oracle_symblocs/limits.res.oracle | 0
tests/value/oracle_symblocs/local.res.oracle | 0
.../oracle_symblocs/local_cleanup.res.oracle | 0
.../oracle_symblocs/local_slevel.res.oracle | 0
.../local_variables.res.oracle | 0
tests/value/oracle_symblocs/lock.res.oracle | 0
tests/value/oracle_symblocs/logic.res.oracle | 0
.../oracle_symblocs/logic_ptr_cast.res.oracle | 0
.../oracle_symblocs/logicdeps.res.oracle | 0
tests/value/oracle_symblocs/long.res.oracle | 0
.../oracle_symblocs/long_const.0.res.oracle | 0
.../oracle_symblocs/long_const.1.res.oracle | 0
tests/value/oracle_symblocs/loop.res.oracle | 0
tests/value/oracle_symblocs/loop1.res.oracle | 0
tests/value/oracle_symblocs/loop2.res.oracle | 0
tests/value/oracle_symblocs/loop3.res.oracle | 0
.../oracle_symblocs/loop_array.res.oracle | 0
.../oracle_symblocs/loop_join.res.oracle | 0
.../oracle_symblocs/loop_long.res.oracle | 0
.../oracle_symblocs/loop_no_var.res.oracle | 0
.../oracle_symblocs/loop_simple.res.oracle | 0
.../oracle_symblocs/loop_test.0.res.oracle | 0
.../oracle_symblocs/loop_test.1.res.oracle | 0
.../oracle_symblocs/loop_wvar.0.res.oracle | 0
.../oracle_symblocs/loop_wvar.1.res.oracle | 0
.../oracle_symblocs/loop_wvar.2.res.oracle | 0
.../oracle_symblocs/loop_wvar.3.res.oracle | 0
.../oracle_symblocs/loopfun.0.res.oracle | 0
.../oracle_symblocs/loopfun.1.res.oracle | 0
.../value/oracle_symblocs/loopinv.res.oracle | 0
.../value/oracle_symblocs/machdep.res.oracle | 0
.../oracle_symblocs/max_pointed.res.oracle | 0
.../value/oracle_symblocs/memexec.res.oracle | 0
.../oracle_symblocs/merge_bits.res.oracle | 0
.../oracle_symblocs/mini_pointrer.res.oracle | 0
.../misaligned_tabs.res.oracle | 0
.../oracle_symblocs/mixed_val.res.oracle | 0
.../value/oracle_symblocs/modifies.res.oracle | 0
tests/value/oracle_symblocs/modulo.res.oracle | 0
.../oracle_symblocs/multi_access.res.oracle | 0
.../narrow_behaviors.res.oracle | 0
.../nested_struct_init.res.oracle | 0
.../oracle_symblocs/no_results.res.oracle | 0
.../non_iso_initializer.res.oracle | 0
.../oracle_symblocs/non_natural.res.oracle | 52 ++++++++++++++
tests/value/oracle_symblocs/nonlin.res.oracle | 0
.../value/oracle_symblocs/noreturn.res.oracle | 0
tests/value/oracle_symblocs/not.res.oracle | 0
.../not_ct_array_arg.res.oracle | 0
.../oracle_symblocs/null_lt_valid.res.oracle | 0
.../value/oracle_symblocs/octagons.res.oracle | 0
.../offset_misaligned.res.oracle | 0
.../oracle_symblocs/offset_neg.res.oracle | 0
.../oracle_symblocs/offset_top.res.oracle | 0
.../oracle_symblocs/offsetmap.0.res.oracle | 4 ++
.../oracle_symblocs/offsetmap.1.res.oracle | 4 ++
.../value/oracle_symblocs/origin.0.res.oracle | 0
.../value/oracle_symblocs/origin.1.res.oracle | 0
.../oracle_symblocs/output_leafs.res.oracle | 0
.../oracle_symblocs/overflow.0.res.oracle | 0
.../oracle_symblocs/overflow.1.res.oracle | 0
.../overflow_cast_float_int.res.oracle | 0
tests/value/oracle_symblocs/packed.res.oracle | 0
.../partitioning-annots.0.res.oracle | 0
.../partitioning-annots.1.res.oracle | 0
.../partitioning-annots.2.res.oracle | 0
.../partitioning-annots.3.res.oracle | 0
.../partitioning-annots.4.res.oracle | 0
.../partitioning-annots.5.res.oracle | 0
.../partitioning-annots.6.res.oracle | 0
tests/value/oracle_symblocs/pb.res.oracle | 0
tests/value/oracle_symblocs/period.res.oracle | 0
tests/value/oracle_symblocs/plevel.res.oracle | 4 ++
.../value/oracle_symblocs/pointer.res.oracle | 0
.../oracle_symblocs/pointer2.0.res.oracle | 0
.../oracle_symblocs/pointer2.1.res.oracle | 0
.../value/oracle_symblocs/pointer3.res.oracle | 0
.../value/oracle_symblocs/pointer4.res.oracle | 0
.../oracle_symblocs/pointer_arg.res.oracle | 0
.../oracle_symblocs/pointer_comp.res.oracle | 0
.../pointer_comparison.0.res.oracle | 0
.../pointer_comparison.1.res.oracle | 0
.../pointer_int_cast.res.oracle | 0
.../oracle_symblocs/pointer_loop.res.oracle | 0
.../oracle_symblocs/postcond_leaf.res.oracle | 0
.../oracle_symblocs/postcondition.res.oracle | 0
tests/value/oracle_symblocs/pragma.res.oracle | 0
.../precise_locations.res.oracle | 0
.../value/oracle_symblocs/precond.res.oracle | 0
.../oracle_symblocs/precond2.0.res.oracle | 0
.../oracle_symblocs/precond2.1.res.oracle | 0
.../propagate_bottom.res.oracle | 0
.../oracle_symblocs/protomain.res.oracle | 0
.../ptr_call_object.res.oracle | 0
.../oracle_symblocs/ptr_relation.0.res.oracle | 4 ++
.../oracle_symblocs/ptr_relation.1.res.oracle | 0
.../oracle_symblocs/ptr_relation.2.res.oracle | 0
.../value/oracle_symblocs/pure_exp.res.oracle | 0
.../qualified_arrays.res.oracle | 0
tests/value/oracle_symblocs/raz.res.oracle | 0
.../oracle_symblocs/reading_null.res.oracle | 0
tests/value/oracle_symblocs/rec.res.oracle | 0
.../value/oracle_symblocs/recol.0.res.oracle | 0
.../value/oracle_symblocs/recol.1.res.oracle | 0
.../oracle_symblocs/recursion.0.res.oracle | 0
.../oracle_symblocs/recursion.1.res.oracle | 0
.../oracle_symblocs/recursion2.res.oracle | 0
.../reduce_by_valid.res.oracle | 0
.../oracle_symblocs/reduce_formals.res.oracle | 0
.../oracle_symblocs/reduce_index.res.oracle | 0
.../oracle_symblocs/reduce_valid.res.oracle | 0
.../redundant_alarms.res.oracle | 41 +++++++++++
.../reevaluate_alarms.res.oracle | 0
.../relation_reduction.res.oracle | 0
.../oracle_symblocs/relation_shift.res.oracle | 0
.../oracle_symblocs/relations.res.oracle | 0
.../oracle_symblocs/relations2.res.oracle | 2 +
.../relations_difficult.res.oracle | 0
.../replace_by_show_each.res.oracle | 0
.../value/oracle_symblocs/resolve.res.oracle | 0
tests/value/oracle_symblocs/return.res.oracle | 0
.../oracle_symblocs/semaphore.res.oracle | 0
.../oracle_symblocs/separated.res.oracle | 0
.../value/oracle_symblocs/shift.0.res.oracle | 0
.../value/oracle_symblocs/shift.1.res.oracle | 0
.../oracle_symblocs/shift_big.res.oracle | 0
.../oracle_symblocs/shift_neg.0.res.oracle | 0
.../oracle_symblocs/shift_neg.1.res.oracle | 0
.../sign_of_bitfiled_int.0.res.oracle | 0
.../sign_of_bitfiled_int.1.res.oracle | 0
.../oracle_symblocs/simple_packed.res.oracle | 0
.../oracle_symblocs/simple_path.res.oracle | 0
.../oracle_symblocs/simplify_cfg.0.res.oracle | 0
.../oracle_symblocs/simplify_cfg.1.res.oracle | 0
tests/value/oracle_symblocs/sizeof.res.oracle | 0
.../oracle_symblocs/slevel_return.res.oracle | 0
.../value/oracle_symblocs/slevelex.res.oracle | 0
.../small_conditionals.res.oracle | 0
.../value/oracle_symblocs/sort4.0.res.oracle | 0
.../value/oracle_symblocs/sort4.1.res.oracle | 0
.../value/oracle_symblocs/sort4.2.res.oracle | 0
.../oracle_symblocs/split_return.0.res.oracle | 0
.../oracle_symblocs/split_return.1.res.oracle | 0
.../oracle_symblocs/split_return.2.res.oracle | 0
.../oracle_symblocs/split_return.3.res.oracle | 0
.../oracle_symblocs/split_return.4.res.oracle | 0
.../statement_contract.res.oracle | 0
tests/value/oracle_symblocs/static.res.oracle | 0
.../value/oracle_symblocs/strange.res.oracle | 0
.../value/oracle_symblocs/strings.res.oracle | 0
.../oracle_symblocs/strings_cond.res.oracle | 0
tests/value/oracle_symblocs/struct.res.oracle | 0
.../value/oracle_symblocs/struct2.res.oracle | 27 +++++++
.../value/oracle_symblocs/struct3.res.oracle | 0
.../oracle_symblocs/struct_array.res.oracle | 0
.../oracle_symblocs/struct_call.0.res.oracle | 0
.../oracle_symblocs/struct_call.1.res.oracle | 0
.../oracle_symblocs/struct_deps.res.oracle | 0
.../oracle_symblocs/struct_incl.res.oracle | 0
.../oracle_symblocs/struct_p_call.res.oracle | 0
.../value/oracle_symblocs/strucval.res.oracle | 0
tests/value/oracle_symblocs/subset.res.oracle | 0
.../oracle_symblocs/summary.0.res.oracle | 0
.../oracle_symblocs/summary.1.res.oracle | 0
.../oracle_symblocs/summary.2.res.oracle | 0
.../oracle_symblocs/summary.3.res.oracle | 0
.../oracle_symblocs/summary.4.res.oracle | 0
.../value/oracle_symblocs/switch.0.res.oracle | 0
.../value/oracle_symblocs/switch.1.res.oracle | 0
.../value/oracle_symblocs/switch2.res.oracle | 0
.../oracle_symblocs/switch_cast.res.oracle | 0
.../oracle_symblocs/symbolic_locs.res.oracle | 71 +++++++++++++++++++
tests/value/oracle_symblocs/tab.res.oracle | 0
tests/value/oracle_symblocs/tab1.res.oracle | 0
.../oracle_symblocs/termination.res.oracle | 0
tests/value/oracle_symblocs/test.0.res.oracle | 4 ++
tests/value/oracle_symblocs/test.1.res.oracle | 0
.../oracle_symblocs/test_arith.res.oracle | 0
.../oracle_symblocs/threat_array.res.oracle | 0
.../oracle_symblocs/threat_if.res.oracle | 0
.../threat_redundant.res.oracle | 0
.../oracle_symblocs/tricky_logic.res.oracle | 0
.../typedef_function.res.oracle | 0
tests/value/oracle_symblocs/typeof.res.oracle | 0
.../ulongvslonglong.0.res.oracle | 0
.../ulongvslonglong.1.res.oracle | 0
.../undef_behavior_bts1059.res.oracle | 0
.../oracle_symblocs/undef_fct.res.oracle | 0
.../undefined_sequence.0.res.oracle | 0
.../undefined_sequence.1.res.oracle | 0
.../undefined_sequence2.res.oracle | 0
tests/value/oracle_symblocs/uninit.res.oracle | 0
.../uninit_callstack.res.oracle | 0
.../uninitialized_gnubody.res.oracle | 0
.../unknown_sizeof.0.res.oracle | 0
.../unknown_sizeof.1.res.oracle | 0
tests/value/oracle_symblocs/unop.res.oracle | 0
tests/value/oracle_symblocs/unroll.res.oracle | 0
.../oracle_symblocs/unroll_simple.res.oracle | 0
.../unsigned_overflow.res.oracle | 0
.../oracle_symblocs/use_spec.0.res.oracle | 0
.../oracle_symblocs/use_spec.1.res.oracle | 0
.../user_assertion_uninit_var.res.oracle | 0
tests/value/oracle_symblocs/usp.res.oracle | 0
.../oracle_symblocs/va_list.0.res.oracle | 0
.../oracle_symblocs/va_list.1.res.oracle | 0
.../oracle_symblocs/va_list2.0.res.oracle | 0
.../oracle_symblocs/va_list2.1.res.oracle | 0
tests/value/oracle_symblocs/val6.0.res.oracle | 0
tests/value/oracle_symblocs/val6.1.res.oracle | 0
.../value/oracle_symblocs/val_if.0.res.oracle | 0
.../value/oracle_symblocs/val_if.1.res.oracle | 0
.../value/oracle_symblocs/val_if.2.res.oracle | 0
.../oracle_symblocs/val_ptr.0.res.oracle | 0
.../oracle_symblocs/val_ptr.1.res.oracle | 0
.../oracle_symblocs/val_ptr.2.res.oracle | 0
.../oracle_symblocs/val_ptr.3.res.oracle | 0
.../oracle_symblocs/video_detect.res.oracle | 0
.../value/oracle_symblocs/volatile.res.oracle | 0
.../oracle_symblocs/volatile2.res.oracle | 0
.../oracle_symblocs/volatilestruct.res.oracle | 0
.../oracle_symblocs/wide_string.res.oracle | 0
.../widen_non_constant.res.oracle | 0
.../widen_on_non_monotonic.res.oracle | 0
.../oracle_symblocs/widen_overflow.res.oracle | 0
.../widening_thresholds.res.oracle | 0
.../oracle_symblocs/with_comment.res.oracle | 0
.../zerolengtharrays.res.oracle | 0
504 files changed, 324 insertions(+)
create mode 100644 tests/value/oracle_symblocs/CruiseControl.res.oracle
create mode 100644 tests/value/oracle_symblocs/FP5.res.oracle
create mode 100644 tests/value/oracle_symblocs/abs.res.oracle
create mode 100644 tests/value/oracle_symblocs/abs_addr.res.oracle
create mode 100644 tests/value/oracle_symblocs/absolute_pointer.res.oracle
create mode 100644 tests/value/oracle_symblocs/abstract_struct_1.res.oracle
create mode 100644 tests/value/oracle_symblocs/access_path.res.oracle
create mode 100644 tests/value/oracle_symblocs/add_approx.res.oracle
create mode 100644 tests/value/oracle_symblocs/addition.res.oracle
create mode 100644 tests/value/oracle_symblocs/addr.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/addr.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/addr2.res.oracle
create mode 100644 tests/value/oracle_symblocs/addrofstring.res.oracle
create mode 100644 tests/value/oracle_symblocs/affect_corrupt.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/affect_corrupt.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/ai_annot.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.5.res.oracle
create mode 100644 tests/value/oracle_symblocs/alias.6.res.oracle
create mode 100644 tests/value/oracle_symblocs/align.res.oracle
create mode 100644 tests/value/oracle_symblocs/align_char_array.res.oracle
create mode 100644 tests/value/oracle_symblocs/annot.res.oracle
create mode 100644 tests/value/oracle_symblocs/annot_valid.res.oracle
create mode 100644 tests/value/oracle_symblocs/anonymous_field.res.oracle
create mode 100644 tests/value/oracle_symblocs/any_int.res.oracle
create mode 100644 tests/value/oracle_symblocs/arch.res.oracle
create mode 100644 tests/value/oracle_symblocs/arg_array.res.oracle
create mode 100644 tests/value/oracle_symblocs/arith_pointer.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_access.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_array.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_array.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_array.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_bounds.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_bounds.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_degenerating_loop.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_initializer.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_loop.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_overlap.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_ptr.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_zero_length.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_zero_length.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/array_zero_length.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/asm_contracts.res.oracle
create mode 100644 tests/value/oracle_symblocs/assert_ptr.res.oracle
create mode 100644 tests/value/oracle_symblocs/assign-leaf-indirect.res.oracle
create mode 100644 tests/value/oracle_symblocs/assigns.res.oracle
create mode 100644 tests/value/oracle_symblocs/assigns_from.res.oracle
create mode 100644 tests/value/oracle_symblocs/assigns_from_direct.res.oracle
create mode 100644 tests/value/oracle_symblocs/attribute-aligned.res.oracle
create mode 100644 tests/value/oracle_symblocs/audit.res.oracle
create mode 100644 tests/value/oracle_symblocs/auto_loop_unroll.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/auto_loop_unroll.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/automalloc.res.oracle
create mode 100644 tests/value/oracle_symblocs/backward_add_ptr.res.oracle
create mode 100644 tests/value/oracle_symblocs/backward_arith.res.oracle
create mode 100644 tests/value/oracle_symblocs/bad_loop.res.oracle
create mode 100644 tests/value/oracle_symblocs/base_addr_offset_block_length.res.oracle
create mode 100644 tests/value/oracle_symblocs/behavior_statuses.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/behavior_statuses.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/behaviors1.res.oracle
create mode 100644 tests/value/oracle_symblocs/behaviors2.res.oracle
create mode 100644 tests/value/oracle_symblocs/big_lib_entry.res.oracle
create mode 100644 tests/value/oracle_symblocs/bigarray.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitfield.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitfield_assign.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitfield_longlong.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitfield_receives_result.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitwise.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitwise_float.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitwise_pointer.res.oracle
create mode 100644 tests/value/oracle_symblocs/bitwise_reduction.res.oracle
create mode 100644 tests/value/oracle_symblocs/biz.res.oracle
create mode 100644 tests/value/oracle_symblocs/bool.res.oracle
create mode 100644 tests/value/oracle_symblocs/branch.res.oracle
create mode 100644 tests/value/oracle_symblocs/branch2.res.oracle
create mode 100644 tests/value/oracle_symblocs/broken_loop.res.oracle
create mode 100644 tests/value/oracle_symblocs/bts0506.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/bts0506.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/bts0775.res.oracle
create mode 100644 tests/value/oracle_symblocs/bts0858.res.oracle
create mode 100644 tests/value/oracle_symblocs/bts1306.res.oracle
create mode 100644 tests/value/oracle_symblocs/buffer_overflow.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/buffer_overflow.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/bug.res.oracle
create mode 100644 tests/value/oracle_symblocs/bug0196.res.oracle
create mode 100644 tests/value/oracle_symblocs/bug0223.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/bug0223.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/bug0245.res.oracle
create mode 100644 tests/value/oracle_symblocs/bug_023.res.oracle
create mode 100644 tests/value/oracle_symblocs/bug_0244.res.oracle
create mode 100644 tests/value/oracle_symblocs/builtins_split.res.oracle
create mode 100644 tests/value/oracle_symblocs/call.res.oracle
create mode 100644 tests/value/oracle_symblocs/call_2.res.oracle
create mode 100644 tests/value/oracle_symblocs/call_3.res.oracle
create mode 100644 tests/value/oracle_symblocs/call_alias.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/call_alias.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/call_alias.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/call_deep.res.oracle
create mode 100644 tests/value/oracle_symblocs/call_multi.res.oracle
create mode 100644 tests/value/oracle_symblocs/call_simple.res.oracle
create mode 100644 tests/value/oracle_symblocs/case_analysis.res.oracle
create mode 100644 tests/value/oracle_symblocs/cast.res.oracle
create mode 100644 tests/value/oracle_symblocs/cast1.res.oracle
create mode 100644 tests/value/oracle_symblocs/cast2.res.oracle
create mode 100644 tests/value/oracle_symblocs/cast_axalto.res.oracle
create mode 100644 tests/value/oracle_symblocs/cast_fun.res.oracle
create mode 100644 tests/value/oracle_symblocs/cast_hetero.res.oracle
create mode 100644 tests/value/oracle_symblocs/cast_return.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/cast_return.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/cert_exp35_c.res.oracle
create mode 100644 tests/value/oracle_symblocs/changeret.res.oracle
create mode 100644 tests/value/oracle_symblocs/cmp.res.oracle
create mode 100644 tests/value/oracle_symblocs/cmp_ptr.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/cmp_ptr.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/cmp_ptr_follow_all_branches.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/cmp_ptr_follow_all_branches.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/cond.res.oracle
create mode 100644 tests/value/oracle_symblocs/cond2.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/cond2.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/cond_integer_cast_of_float.res.oracle
create mode 100644 tests/value/oracle_symblocs/conditional_initializer.res.oracle
create mode 100644 tests/value/oracle_symblocs/const.res.oracle
create mode 100644 tests/value/oracle_symblocs/const2.res.oracle
create mode 100644 tests/value/oracle_symblocs/const_syntax.res.oracle
create mode 100644 tests/value/oracle_symblocs/const_typedef.res.oracle
create mode 100644 tests/value/oracle_symblocs/constarraystructlibentry.res.oracle
create mode 100644 tests/value/oracle_symblocs/context_free.res.oracle
create mode 100644 tests/value/oracle_symblocs/context_free_simple.res.oracle
create mode 100644 tests/value/oracle_symblocs/context_width.res.oracle
create mode 100644 tests/value/oracle_symblocs/control.res.oracle
create mode 100644 tests/value/oracle_symblocs/conversion.res.oracle
create mode 100644 tests/value/oracle_symblocs/copy_paste.res.oracle
create mode 100644 tests/value/oracle_symblocs/copy_paste_hidden_by_dummy_cast.res.oracle
create mode 100644 tests/value/oracle_symblocs/copy_stdin.res.oracle
create mode 100644 tests/value/oracle_symblocs/dangling.res.oracle
create mode 100644 tests/value/oracle_symblocs/dataflow_order.res.oracle
create mode 100644 tests/value/oracle_symblocs/dead_code.res.oracle
create mode 100644 tests/value/oracle_symblocs/dead_code2.res.oracle
create mode 100644 tests/value/oracle_symblocs/dead_inout.res.oracle
create mode 100644 tests/value/oracle_symblocs/dead_statuses.res.oracle
create mode 100644 tests/value/oracle_symblocs/deep_conditionals.res.oracle
create mode 100644 tests/value/oracle_symblocs/degeneration2.res.oracle
create mode 100644 tests/value/oracle_symblocs/deps.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/deps.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/deps.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/deps_addr.res.oracle
create mode 100644 tests/value/oracle_symblocs/deps_compose.res.oracle
create mode 100644 tests/value/oracle_symblocs/deps_local.res.oracle
create mode 100644 tests/value/oracle_symblocs/deps_mixed.res.oracle
create mode 100644 tests/value/oracle_symblocs/deps_unitialized_locals.res.oracle
create mode 100644 tests/value/oracle_symblocs/deref.res.oracle
create mode 100644 tests/value/oracle_symblocs/descending.res.oracle
create mode 100644 tests/value/oracle_symblocs/disjoint_status.res.oracle
create mode 100644 tests/value/oracle_symblocs/div.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/div.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/div_strange.res.oracle
create mode 100644 tests/value/oracle_symblocs/divneg.res.oracle
create mode 100644 tests/value/oracle_symblocs/domains.res.oracle
create mode 100644 tests/value/oracle_symblocs/domains_function.res.oracle
create mode 100644 tests/value/oracle_symblocs/downcast.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/downcast.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/downcast.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/downcast.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/downcast.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/dur.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_base.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_base.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_struct.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_struct.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_struct.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_struct.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_struct.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_struct.5.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_struct.6.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_struct2.res.oracle
create mode 100644 tests/value/oracle_symblocs/empty_union.res.oracle
create mode 100644 tests/value/oracle_symblocs/endian.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/endian.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/enum.res.oracle
create mode 100644 tests/value/oracle_symblocs/enum2.res.oracle
create mode 100644 tests/value/oracle_symblocs/equality.res.oracle
create mode 100644 tests/value/oracle_symblocs/eval_separated.res.oracle
create mode 100644 tests/value/oracle_symblocs/exit_paths.res.oracle
create mode 100644 tests/value/oracle_symblocs/extern.res.oracle
create mode 100644 tests/value/oracle_symblocs/f1.res.oracle
create mode 100644 tests/value/oracle_symblocs/f2.res.oracle
create mode 100644 tests/value/oracle_symblocs/false.res.oracle
create mode 100644 tests/value/oracle_symblocs/fam_sizeof.res.oracle
create mode 100644 tests/value/oracle_symblocs/find_ivaltop.res.oracle
create mode 100644 tests/value/oracle_symblocs/folding.res.oracle
create mode 100644 tests/value/oracle_symblocs/for_loops.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/for_loops.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/for_loops.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/for_loops.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/forall.res.oracle
create mode 100644 tests/value/oracle_symblocs/fptr.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/fptr.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/from1.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_call.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_call.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_global.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_ind.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_pb.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_pb.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_pb.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_pb.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_pb.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_pb.5.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_pb.6.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_pb.7.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_ptr.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_ptr.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_ptr2.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_res_2.res.oracle
create mode 100644 tests/value/oracle_symblocs/from_termin.res.oracle
create mode 100644 tests/value/oracle_symblocs/fun_ptr.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/fun_ptr.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/function_return_serial_casts.res.oracle
create mode 100644 tests/value/oracle_symblocs/g1.res.oracle
create mode 100644 tests/value/oracle_symblocs/garbled_init.res.oracle
create mode 100644 tests/value/oracle_symblocs/gauges.res.oracle
create mode 100644 tests/value/oracle_symblocs/ghost.res.oracle
create mode 100644 tests/value/oracle_symblocs/global_bug.res.oracle
create mode 100644 tests/value/oracle_symblocs/goto.res.oracle
create mode 100644 tests/value/oracle_symblocs/hierarchical_convergence.res.oracle
create mode 100644 tests/value/oracle_symblocs/if.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/if.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/if2.res.oracle
create mode 100644 tests/value/oracle_symblocs/ilevel.res.oracle
create mode 100644 tests/value/oracle_symblocs/implies.res.oracle
create mode 100644 tests/value/oracle_symblocs/imprecise_invalid_write.res.oracle
create mode 100644 tests/value/oracle_symblocs/incompatible_states.res.oracle
create mode 100644 tests/value/oracle_symblocs/incorrect_reduce_expr.res.oracle
create mode 100644 tests/value/oracle_symblocs/ineq.res.oracle
create mode 100644 tests/value/oracle_symblocs/infinite.res.oracle
create mode 100644 tests/value/oracle_symblocs/init.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/init.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/init_const_guard.res.oracle
create mode 100644 tests/value/oracle_symblocs/initialized.res.oracle
create mode 100644 tests/value/oracle_symblocs/initialized_copy.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/initialized_copy.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout_diff.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout_formals.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout_on_alarms.res.oracle
create mode 100644 tests/value/oracle_symblocs/inout_proto.res.oracle
create mode 100644 tests/value/oracle_symblocs/input.res.oracle
create mode 100644 tests/value/oracle_symblocs/integers.res.oracle
create mode 100644 tests/value/oracle_symblocs/interpol.res.oracle
create mode 100644 tests/value/oracle_symblocs/interpreter-mode-syracuse.res.oracle
create mode 100644 tests/value/oracle_symblocs/invalid_loc_return.res.oracle
create mode 100644 tests/value/oracle_symblocs/invalid_lval_arg.res.oracle
create mode 100644 tests/value/oracle_symblocs/invalid_pointer.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/invalid_pointer.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/inversion.res.oracle
create mode 100644 tests/value/oracle_symblocs/inversion2.res.oracle
create mode 100644 tests/value/oracle_symblocs/jacques.res.oracle
create mode 100644 tests/value/oracle_symblocs/join_misaligned.res.oracle
create mode 100644 tests/value/oracle_symblocs/label.res.oracle
create mode 100644 tests/value/oracle_symblocs/lazy.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/lazy.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/leaf.res.oracle
create mode 100644 tests/value/oracle_symblocs/leaf2.res.oracle
create mode 100644 tests/value/oracle_symblocs/leaf_spec.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/leaf_spec.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/library.res.oracle
create mode 100644 tests/value/oracle_symblocs/library_precond.res.oracle
create mode 100644 tests/value/oracle_symblocs/limits.res.oracle
create mode 100644 tests/value/oracle_symblocs/local.res.oracle
create mode 100644 tests/value/oracle_symblocs/local_cleanup.res.oracle
create mode 100644 tests/value/oracle_symblocs/local_slevel.res.oracle
create mode 100644 tests/value/oracle_symblocs/local_variables.res.oracle
create mode 100644 tests/value/oracle_symblocs/lock.res.oracle
create mode 100644 tests/value/oracle_symblocs/logic.res.oracle
create mode 100644 tests/value/oracle_symblocs/logic_ptr_cast.res.oracle
create mode 100644 tests/value/oracle_symblocs/logicdeps.res.oracle
create mode 100644 tests/value/oracle_symblocs/long.res.oracle
create mode 100644 tests/value/oracle_symblocs/long_const.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/long_const.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop1.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop2.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop3.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_array.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_join.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_long.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_no_var.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_simple.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_test.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_test.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_wvar.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_wvar.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_wvar.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/loop_wvar.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/loopfun.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/loopfun.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/loopinv.res.oracle
create mode 100644 tests/value/oracle_symblocs/machdep.res.oracle
create mode 100644 tests/value/oracle_symblocs/max_pointed.res.oracle
create mode 100644 tests/value/oracle_symblocs/memexec.res.oracle
create mode 100644 tests/value/oracle_symblocs/merge_bits.res.oracle
create mode 100644 tests/value/oracle_symblocs/mini_pointrer.res.oracle
create mode 100644 tests/value/oracle_symblocs/misaligned_tabs.res.oracle
create mode 100644 tests/value/oracle_symblocs/mixed_val.res.oracle
create mode 100644 tests/value/oracle_symblocs/modifies.res.oracle
create mode 100644 tests/value/oracle_symblocs/modulo.res.oracle
create mode 100644 tests/value/oracle_symblocs/multi_access.res.oracle
create mode 100644 tests/value/oracle_symblocs/narrow_behaviors.res.oracle
create mode 100644 tests/value/oracle_symblocs/nested_struct_init.res.oracle
create mode 100644 tests/value/oracle_symblocs/no_results.res.oracle
create mode 100644 tests/value/oracle_symblocs/non_iso_initializer.res.oracle
create mode 100644 tests/value/oracle_symblocs/non_natural.res.oracle
create mode 100644 tests/value/oracle_symblocs/nonlin.res.oracle
create mode 100644 tests/value/oracle_symblocs/noreturn.res.oracle
create mode 100644 tests/value/oracle_symblocs/not.res.oracle
create mode 100644 tests/value/oracle_symblocs/not_ct_array_arg.res.oracle
create mode 100644 tests/value/oracle_symblocs/null_lt_valid.res.oracle
create mode 100644 tests/value/oracle_symblocs/octagons.res.oracle
create mode 100644 tests/value/oracle_symblocs/offset_misaligned.res.oracle
create mode 100644 tests/value/oracle_symblocs/offset_neg.res.oracle
create mode 100644 tests/value/oracle_symblocs/offset_top.res.oracle
create mode 100644 tests/value/oracle_symblocs/offsetmap.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/offsetmap.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/origin.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/origin.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/output_leafs.res.oracle
create mode 100644 tests/value/oracle_symblocs/overflow.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/overflow.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/overflow_cast_float_int.res.oracle
create mode 100644 tests/value/oracle_symblocs/packed.res.oracle
create mode 100644 tests/value/oracle_symblocs/partitioning-annots.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/partitioning-annots.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/partitioning-annots.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/partitioning-annots.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/partitioning-annots.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/partitioning-annots.5.res.oracle
create mode 100644 tests/value/oracle_symblocs/partitioning-annots.6.res.oracle
create mode 100644 tests/value/oracle_symblocs/pb.res.oracle
create mode 100644 tests/value/oracle_symblocs/period.res.oracle
create mode 100644 tests/value/oracle_symblocs/plevel.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer2.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer2.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer3.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer4.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer_arg.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer_comp.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer_comparison.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer_comparison.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer_int_cast.res.oracle
create mode 100644 tests/value/oracle_symblocs/pointer_loop.res.oracle
create mode 100644 tests/value/oracle_symblocs/postcond_leaf.res.oracle
create mode 100644 tests/value/oracle_symblocs/postcondition.res.oracle
create mode 100644 tests/value/oracle_symblocs/pragma.res.oracle
create mode 100644 tests/value/oracle_symblocs/precise_locations.res.oracle
create mode 100644 tests/value/oracle_symblocs/precond.res.oracle
create mode 100644 tests/value/oracle_symblocs/precond2.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/precond2.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/propagate_bottom.res.oracle
create mode 100644 tests/value/oracle_symblocs/protomain.res.oracle
create mode 100644 tests/value/oracle_symblocs/ptr_call_object.res.oracle
create mode 100644 tests/value/oracle_symblocs/ptr_relation.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/ptr_relation.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/ptr_relation.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/pure_exp.res.oracle
create mode 100644 tests/value/oracle_symblocs/qualified_arrays.res.oracle
create mode 100644 tests/value/oracle_symblocs/raz.res.oracle
create mode 100644 tests/value/oracle_symblocs/reading_null.res.oracle
create mode 100644 tests/value/oracle_symblocs/rec.res.oracle
create mode 100644 tests/value/oracle_symblocs/recol.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/recol.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/recursion.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/recursion.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/recursion2.res.oracle
create mode 100644 tests/value/oracle_symblocs/reduce_by_valid.res.oracle
create mode 100644 tests/value/oracle_symblocs/reduce_formals.res.oracle
create mode 100644 tests/value/oracle_symblocs/reduce_index.res.oracle
create mode 100644 tests/value/oracle_symblocs/reduce_valid.res.oracle
create mode 100644 tests/value/oracle_symblocs/redundant_alarms.res.oracle
create mode 100644 tests/value/oracle_symblocs/reevaluate_alarms.res.oracle
create mode 100644 tests/value/oracle_symblocs/relation_reduction.res.oracle
create mode 100644 tests/value/oracle_symblocs/relation_shift.res.oracle
create mode 100644 tests/value/oracle_symblocs/relations.res.oracle
create mode 100644 tests/value/oracle_symblocs/relations2.res.oracle
create mode 100644 tests/value/oracle_symblocs/relations_difficult.res.oracle
create mode 100644 tests/value/oracle_symblocs/replace_by_show_each.res.oracle
create mode 100644 tests/value/oracle_symblocs/resolve.res.oracle
create mode 100644 tests/value/oracle_symblocs/return.res.oracle
create mode 100644 tests/value/oracle_symblocs/semaphore.res.oracle
create mode 100644 tests/value/oracle_symblocs/separated.res.oracle
create mode 100644 tests/value/oracle_symblocs/shift.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/shift.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/shift_big.res.oracle
create mode 100644 tests/value/oracle_symblocs/shift_neg.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/shift_neg.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/sign_of_bitfiled_int.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/sign_of_bitfiled_int.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/simple_packed.res.oracle
create mode 100644 tests/value/oracle_symblocs/simple_path.res.oracle
create mode 100644 tests/value/oracle_symblocs/simplify_cfg.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/simplify_cfg.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/sizeof.res.oracle
create mode 100644 tests/value/oracle_symblocs/slevel_return.res.oracle
create mode 100644 tests/value/oracle_symblocs/slevelex.res.oracle
create mode 100644 tests/value/oracle_symblocs/small_conditionals.res.oracle
create mode 100644 tests/value/oracle_symblocs/sort4.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/sort4.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/sort4.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/split_return.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/split_return.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/split_return.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/split_return.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/split_return.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/statement_contract.res.oracle
create mode 100644 tests/value/oracle_symblocs/static.res.oracle
create mode 100644 tests/value/oracle_symblocs/strange.res.oracle
create mode 100644 tests/value/oracle_symblocs/strings.res.oracle
create mode 100644 tests/value/oracle_symblocs/strings_cond.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct2.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct3.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct_array.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct_call.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct_call.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct_deps.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct_incl.res.oracle
create mode 100644 tests/value/oracle_symblocs/struct_p_call.res.oracle
create mode 100644 tests/value/oracle_symblocs/strucval.res.oracle
create mode 100644 tests/value/oracle_symblocs/subset.res.oracle
create mode 100644 tests/value/oracle_symblocs/summary.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/summary.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/summary.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/summary.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/summary.4.res.oracle
create mode 100644 tests/value/oracle_symblocs/switch.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/switch.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/switch2.res.oracle
create mode 100644 tests/value/oracle_symblocs/switch_cast.res.oracle
create mode 100644 tests/value/oracle_symblocs/symbolic_locs.res.oracle
create mode 100644 tests/value/oracle_symblocs/tab.res.oracle
create mode 100644 tests/value/oracle_symblocs/tab1.res.oracle
create mode 100644 tests/value/oracle_symblocs/termination.res.oracle
create mode 100644 tests/value/oracle_symblocs/test.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/test.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/test_arith.res.oracle
create mode 100644 tests/value/oracle_symblocs/threat_array.res.oracle
create mode 100644 tests/value/oracle_symblocs/threat_if.res.oracle
create mode 100644 tests/value/oracle_symblocs/threat_redundant.res.oracle
create mode 100644 tests/value/oracle_symblocs/tricky_logic.res.oracle
create mode 100644 tests/value/oracle_symblocs/typedef_function.res.oracle
create mode 100644 tests/value/oracle_symblocs/typeof.res.oracle
create mode 100644 tests/value/oracle_symblocs/ulongvslonglong.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/ulongvslonglong.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/undef_behavior_bts1059.res.oracle
create mode 100644 tests/value/oracle_symblocs/undef_fct.res.oracle
create mode 100644 tests/value/oracle_symblocs/undefined_sequence.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/undefined_sequence.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/undefined_sequence2.res.oracle
create mode 100644 tests/value/oracle_symblocs/uninit.res.oracle
create mode 100644 tests/value/oracle_symblocs/uninit_callstack.res.oracle
create mode 100644 tests/value/oracle_symblocs/uninitialized_gnubody.res.oracle
create mode 100644 tests/value/oracle_symblocs/unknown_sizeof.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/unknown_sizeof.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/unop.res.oracle
create mode 100644 tests/value/oracle_symblocs/unroll.res.oracle
create mode 100644 tests/value/oracle_symblocs/unroll_simple.res.oracle
create mode 100644 tests/value/oracle_symblocs/unsigned_overflow.res.oracle
create mode 100644 tests/value/oracle_symblocs/use_spec.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/use_spec.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/user_assertion_uninit_var.res.oracle
create mode 100644 tests/value/oracle_symblocs/usp.res.oracle
create mode 100644 tests/value/oracle_symblocs/va_list.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/va_list.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/va_list2.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/va_list2.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/val6.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/val6.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/val_if.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/val_if.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/val_if.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/val_ptr.0.res.oracle
create mode 100644 tests/value/oracle_symblocs/val_ptr.1.res.oracle
create mode 100644 tests/value/oracle_symblocs/val_ptr.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/val_ptr.3.res.oracle
create mode 100644 tests/value/oracle_symblocs/video_detect.res.oracle
create mode 100644 tests/value/oracle_symblocs/volatile.res.oracle
create mode 100644 tests/value/oracle_symblocs/volatile2.res.oracle
create mode 100644 tests/value/oracle_symblocs/volatilestruct.res.oracle
create mode 100644 tests/value/oracle_symblocs/wide_string.res.oracle
create mode 100644 tests/value/oracle_symblocs/widen_non_constant.res.oracle
create mode 100644 tests/value/oracle_symblocs/widen_on_non_monotonic.res.oracle
create mode 100644 tests/value/oracle_symblocs/widen_overflow.res.oracle
create mode 100644 tests/value/oracle_symblocs/widening_thresholds.res.oracle
create mode 100644 tests/value/oracle_symblocs/with_comment.res.oracle
create mode 100644 tests/value/oracle_symblocs/zerolengtharrays.res.oracle
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index b4a58bcd9f8..d25a43c5eb7 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,3 +1,7 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains symbolic-locations
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+
+# Compare the result with the oracle of the default config.
+FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
+
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/oracle_symblocs/CruiseControl.res.oracle b/tests/value/oracle_symblocs/CruiseControl.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/FP5.res.oracle b/tests/value/oracle_symblocs/FP5.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/abs.res.oracle b/tests/value/oracle_symblocs/abs.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/abs_addr.res.oracle b/tests/value/oracle_symblocs/abs_addr.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/absolute_pointer.res.oracle b/tests/value/oracle_symblocs/absolute_pointer.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/abstract_struct_1.res.oracle b/tests/value/oracle_symblocs/abstract_struct_1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/access_path.res.oracle b/tests/value/oracle_symblocs/access_path.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/add_approx.res.oracle b/tests/value/oracle_symblocs/add_approx.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/addition.res.oracle b/tests/value/oracle_symblocs/addition.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/addr.0.res.oracle b/tests/value/oracle_symblocs/addr.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/addr.1.res.oracle b/tests/value/oracle_symblocs/addr.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/addr2.res.oracle b/tests/value/oracle_symblocs/addr2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/addrofstring.res.oracle b/tests/value/oracle_symblocs/addrofstring.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/affect_corrupt.0.res.oracle b/tests/value/oracle_symblocs/affect_corrupt.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/affect_corrupt.1.res.oracle b/tests/value/oracle_symblocs/affect_corrupt.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ai_annot.res.oracle b/tests/value/oracle_symblocs/ai_annot.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/alias.0.res.oracle b/tests/value/oracle_symblocs/alias.0.res.oracle
new file mode 100644
index 00000000000..c234ab23c2e
--- /dev/null
+++ b/tests/value/oracle_symblocs/alias.0.res.oracle
@@ -0,0 +1,10 @@
+103,104c103,104
+< t ∈ {1; 2; 4}
+< u ∈ {2; 3; 4; 5}
+---
+> t ∈ {4}
+> u ∈ {5}
+110c110
+< t2 ∈ {0; 3; 6}
+---
+> t2 ∈ {6}
diff --git a/tests/value/oracle_symblocs/alias.1.res.oracle b/tests/value/oracle_symblocs/alias.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/alias.2.res.oracle b/tests/value/oracle_symblocs/alias.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/alias.3.res.oracle b/tests/value/oracle_symblocs/alias.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/alias.4.res.oracle b/tests/value/oracle_symblocs/alias.4.res.oracle
new file mode 100644
index 00000000000..f45634e31c8
--- /dev/null
+++ b/tests/value/oracle_symblocs/alias.4.res.oracle
@@ -0,0 +1,4 @@
+81c81
+< y ∈ {0; 3; 77}
+---
+> y ∈ {77}
diff --git a/tests/value/oracle_symblocs/alias.5.res.oracle b/tests/value/oracle_symblocs/alias.5.res.oracle
new file mode 100644
index 00000000000..10edd6543c8
--- /dev/null
+++ b/tests/value/oracle_symblocs/alias.5.res.oracle
@@ -0,0 +1,4 @@
+170c170
+< y ∈ {0; 3; 77}
+---
+> y ∈ {77}
diff --git a/tests/value/oracle_symblocs/alias.6.res.oracle b/tests/value/oracle_symblocs/alias.6.res.oracle
new file mode 100644
index 00000000000..a7dfd303175
--- /dev/null
+++ b/tests/value/oracle_symblocs/alias.6.res.oracle
@@ -0,0 +1,4 @@
+86c86
+< x ∈ {0; 4; 33}
+---
+> x ∈ {33}
diff --git a/tests/value/oracle_symblocs/align.res.oracle b/tests/value/oracle_symblocs/align.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/align_char_array.res.oracle b/tests/value/oracle_symblocs/align_char_array.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/annot.res.oracle b/tests/value/oracle_symblocs/annot.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/annot_valid.res.oracle b/tests/value/oracle_symblocs/annot_valid.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/anonymous_field.res.oracle b/tests/value/oracle_symblocs/anonymous_field.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/any_int.res.oracle b/tests/value/oracle_symblocs/any_int.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/arch.res.oracle b/tests/value/oracle_symblocs/arch.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/arg_array.res.oracle b/tests/value/oracle_symblocs/arg_array.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/arith_pointer.res.oracle b/tests/value/oracle_symblocs/arith_pointer.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_access.res.oracle b/tests/value/oracle_symblocs/array_access.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_array.0.res.oracle b/tests/value/oracle_symblocs/array_array.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_array.1.res.oracle b/tests/value/oracle_symblocs/array_array.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_array.2.res.oracle b/tests/value/oracle_symblocs/array_array.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_bounds.0.res.oracle b/tests/value/oracle_symblocs/array_bounds.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_bounds.1.res.oracle b/tests/value/oracle_symblocs/array_bounds.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_degenerating_loop.res.oracle b/tests/value/oracle_symblocs/array_degenerating_loop.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_initializer.res.oracle b/tests/value/oracle_symblocs/array_initializer.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_loop.res.oracle b/tests/value/oracle_symblocs/array_loop.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_overlap.res.oracle b/tests/value/oracle_symblocs/array_overlap.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_ptr.res.oracle b/tests/value/oracle_symblocs/array_ptr.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_zero_length.0.res.oracle b/tests/value/oracle_symblocs/array_zero_length.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_zero_length.1.res.oracle b/tests/value/oracle_symblocs/array_zero_length.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/array_zero_length.2.res.oracle b/tests/value/oracle_symblocs/array_zero_length.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/asm_contracts.res.oracle b/tests/value/oracle_symblocs/asm_contracts.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/assert_ptr.res.oracle b/tests/value/oracle_symblocs/assert_ptr.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/assign-leaf-indirect.res.oracle b/tests/value/oracle_symblocs/assign-leaf-indirect.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/assigns.res.oracle b/tests/value/oracle_symblocs/assigns.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/assigns_from.res.oracle b/tests/value/oracle_symblocs/assigns_from.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/assigns_from_direct.res.oracle b/tests/value/oracle_symblocs/assigns_from_direct.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/attribute-aligned.res.oracle b/tests/value/oracle_symblocs/attribute-aligned.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/audit.res.oracle b/tests/value/oracle_symblocs/audit.res.oracle
new file mode 100644
index 00000000000..9ff41db2488
--- /dev/null
+++ b/tests/value/oracle_symblocs/audit.res.oracle
@@ -0,0 +1,11 @@
+1,8d0
+< [kernel:audit] Warning:
+< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101
+< [kernel:audit] Warning:
+< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list)
+< [kernel:audit] Warning:
+< missing files:
+< tests/value/non_existing_file.h
+< [kernel] Audit: sources list written to: tests/value/result/audit-out.json
+34d25
+< [kernel] Wrote: tests/value/result/audit-out.json
diff --git a/tests/value/oracle_symblocs/auto_loop_unroll.0.res.oracle b/tests/value/oracle_symblocs/auto_loop_unroll.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/auto_loop_unroll.1.res.oracle b/tests/value/oracle_symblocs/auto_loop_unroll.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/automalloc.res.oracle b/tests/value/oracle_symblocs/automalloc.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/backward_add_ptr.res.oracle b/tests/value/oracle_symblocs/backward_add_ptr.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/backward_arith.res.oracle b/tests/value/oracle_symblocs/backward_arith.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bad_loop.res.oracle b/tests/value/oracle_symblocs/bad_loop.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/base_addr_offset_block_length.res.oracle b/tests/value/oracle_symblocs/base_addr_offset_block_length.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/behavior_statuses.0.res.oracle b/tests/value/oracle_symblocs/behavior_statuses.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/behavior_statuses.1.res.oracle b/tests/value/oracle_symblocs/behavior_statuses.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/behaviors1.res.oracle b/tests/value/oracle_symblocs/behaviors1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/behaviors2.res.oracle b/tests/value/oracle_symblocs/behaviors2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/big_lib_entry.res.oracle b/tests/value/oracle_symblocs/big_lib_entry.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bigarray.res.oracle b/tests/value/oracle_symblocs/bigarray.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bitfield.res.oracle b/tests/value/oracle_symblocs/bitfield.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bitfield_assign.res.oracle b/tests/value/oracle_symblocs/bitfield_assign.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bitfield_longlong.res.oracle b/tests/value/oracle_symblocs/bitfield_longlong.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bitfield_receives_result.res.oracle b/tests/value/oracle_symblocs/bitfield_receives_result.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bitwise.res.oracle b/tests/value/oracle_symblocs/bitwise.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bitwise_float.res.oracle b/tests/value/oracle_symblocs/bitwise_float.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bitwise_pointer.res.oracle b/tests/value/oracle_symblocs/bitwise_pointer.res.oracle
new file mode 100644
index 00000000000..f04f7077977
--- /dev/null
+++ b/tests/value/oracle_symblocs/bitwise_pointer.res.oracle
@@ -0,0 +1,8 @@
+62c62
+< x ∈ [0..9]
+---
+> x ∈ {5}
+75c75
+< x1 ∈ [0..9]
+---
+> x1 ∈ {5}
diff --git a/tests/value/oracle_symblocs/bitwise_reduction.res.oracle b/tests/value/oracle_symblocs/bitwise_reduction.res.oracle
new file mode 100644
index 00000000000..13596efae1b
--- /dev/null
+++ b/tests/value/oracle_symblocs/bitwise_reduction.res.oracle
@@ -0,0 +1,16 @@
+20c20
+< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+---
+> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+23c23
+< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+---
+> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+30c30
+< {{ &t + {0; 4} }}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+---
+> {{ &t + {0; 4} }}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+33c33
+< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+---
+> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
diff --git a/tests/value/oracle_symblocs/biz.res.oracle b/tests/value/oracle_symblocs/biz.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bool.res.oracle b/tests/value/oracle_symblocs/bool.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/branch.res.oracle b/tests/value/oracle_symblocs/branch.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/branch2.res.oracle b/tests/value/oracle_symblocs/branch2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/broken_loop.res.oracle b/tests/value/oracle_symblocs/broken_loop.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bts0506.0.res.oracle b/tests/value/oracle_symblocs/bts0506.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bts0506.1.res.oracle b/tests/value/oracle_symblocs/bts0506.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bts0775.res.oracle b/tests/value/oracle_symblocs/bts0775.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bts0858.res.oracle b/tests/value/oracle_symblocs/bts0858.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bts1306.res.oracle b/tests/value/oracle_symblocs/bts1306.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/buffer_overflow.0.res.oracle b/tests/value/oracle_symblocs/buffer_overflow.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/buffer_overflow.1.res.oracle b/tests/value/oracle_symblocs/buffer_overflow.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bug.res.oracle b/tests/value/oracle_symblocs/bug.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bug0196.res.oracle b/tests/value/oracle_symblocs/bug0196.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bug0223.0.res.oracle b/tests/value/oracle_symblocs/bug0223.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bug0223.1.res.oracle b/tests/value/oracle_symblocs/bug0223.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bug0245.res.oracle b/tests/value/oracle_symblocs/bug0245.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bug_023.res.oracle b/tests/value/oracle_symblocs/bug_023.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/bug_0244.res.oracle b/tests/value/oracle_symblocs/bug_0244.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/builtins_split.res.oracle b/tests/value/oracle_symblocs/builtins_split.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call.res.oracle b/tests/value/oracle_symblocs/call.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call_2.res.oracle b/tests/value/oracle_symblocs/call_2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call_3.res.oracle b/tests/value/oracle_symblocs/call_3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call_alias.0.res.oracle b/tests/value/oracle_symblocs/call_alias.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call_alias.1.res.oracle b/tests/value/oracle_symblocs/call_alias.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call_alias.2.res.oracle b/tests/value/oracle_symblocs/call_alias.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call_deep.res.oracle b/tests/value/oracle_symblocs/call_deep.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call_multi.res.oracle b/tests/value/oracle_symblocs/call_multi.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/call_simple.res.oracle b/tests/value/oracle_symblocs/call_simple.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/case_analysis.res.oracle b/tests/value/oracle_symblocs/case_analysis.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cast.res.oracle b/tests/value/oracle_symblocs/cast.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cast1.res.oracle b/tests/value/oracle_symblocs/cast1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cast2.res.oracle b/tests/value/oracle_symblocs/cast2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cast_axalto.res.oracle b/tests/value/oracle_symblocs/cast_axalto.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cast_fun.res.oracle b/tests/value/oracle_symblocs/cast_fun.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cast_hetero.res.oracle b/tests/value/oracle_symblocs/cast_hetero.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cast_return.0.res.oracle b/tests/value/oracle_symblocs/cast_return.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cast_return.1.res.oracle b/tests/value/oracle_symblocs/cast_return.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cert_exp35_c.res.oracle b/tests/value/oracle_symblocs/cert_exp35_c.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/changeret.res.oracle b/tests/value/oracle_symblocs/changeret.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cmp.res.oracle b/tests/value/oracle_symblocs/cmp.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cmp_ptr.0.res.oracle b/tests/value/oracle_symblocs/cmp_ptr.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cmp_ptr.1.res.oracle b/tests/value/oracle_symblocs/cmp_ptr.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cmp_ptr_follow_all_branches.0.res.oracle b/tests/value/oracle_symblocs/cmp_ptr_follow_all_branches.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cmp_ptr_follow_all_branches.1.res.oracle b/tests/value/oracle_symblocs/cmp_ptr_follow_all_branches.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cond.res.oracle b/tests/value/oracle_symblocs/cond.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cond2.0.res.oracle b/tests/value/oracle_symblocs/cond2.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cond2.1.res.oracle b/tests/value/oracle_symblocs/cond2.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/cond_integer_cast_of_float.res.oracle b/tests/value/oracle_symblocs/cond_integer_cast_of_float.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/conditional_initializer.res.oracle b/tests/value/oracle_symblocs/conditional_initializer.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/const.res.oracle b/tests/value/oracle_symblocs/const.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/const2.res.oracle b/tests/value/oracle_symblocs/const2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/const_syntax.res.oracle b/tests/value/oracle_symblocs/const_syntax.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/const_typedef.res.oracle b/tests/value/oracle_symblocs/const_typedef.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/constarraystructlibentry.res.oracle b/tests/value/oracle_symblocs/constarraystructlibentry.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/context_free.res.oracle b/tests/value/oracle_symblocs/context_free.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/context_free_simple.res.oracle b/tests/value/oracle_symblocs/context_free_simple.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/context_width.res.oracle b/tests/value/oracle_symblocs/context_width.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/control.res.oracle b/tests/value/oracle_symblocs/control.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/conversion.res.oracle b/tests/value/oracle_symblocs/conversion.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/copy_paste.res.oracle b/tests/value/oracle_symblocs/copy_paste.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/copy_paste_hidden_by_dummy_cast.res.oracle b/tests/value/oracle_symblocs/copy_paste_hidden_by_dummy_cast.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/copy_stdin.res.oracle b/tests/value/oracle_symblocs/copy_stdin.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/dangling.res.oracle b/tests/value/oracle_symblocs/dangling.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/dataflow_order.res.oracle b/tests/value/oracle_symblocs/dataflow_order.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/dead_code.res.oracle b/tests/value/oracle_symblocs/dead_code.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/dead_code2.res.oracle b/tests/value/oracle_symblocs/dead_code2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/dead_inout.res.oracle b/tests/value/oracle_symblocs/dead_inout.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/dead_statuses.res.oracle b/tests/value/oracle_symblocs/dead_statuses.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deep_conditionals.res.oracle b/tests/value/oracle_symblocs/deep_conditionals.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/degeneration2.res.oracle b/tests/value/oracle_symblocs/degeneration2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deps.0.res.oracle b/tests/value/oracle_symblocs/deps.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deps.1.res.oracle b/tests/value/oracle_symblocs/deps.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deps.2.res.oracle b/tests/value/oracle_symblocs/deps.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deps_addr.res.oracle b/tests/value/oracle_symblocs/deps_addr.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deps_compose.res.oracle b/tests/value/oracle_symblocs/deps_compose.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deps_local.res.oracle b/tests/value/oracle_symblocs/deps_local.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deps_mixed.res.oracle b/tests/value/oracle_symblocs/deps_mixed.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deps_unitialized_locals.res.oracle b/tests/value/oracle_symblocs/deps_unitialized_locals.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/deref.res.oracle b/tests/value/oracle_symblocs/deref.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/descending.res.oracle b/tests/value/oracle_symblocs/descending.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/disjoint_status.res.oracle b/tests/value/oracle_symblocs/disjoint_status.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/div.0.res.oracle b/tests/value/oracle_symblocs/div.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/div.1.res.oracle b/tests/value/oracle_symblocs/div.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/div_strange.res.oracle b/tests/value/oracle_symblocs/div_strange.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/divneg.res.oracle b/tests/value/oracle_symblocs/divneg.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/domains.res.oracle b/tests/value/oracle_symblocs/domains.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/domains_function.res.oracle b/tests/value/oracle_symblocs/domains_function.res.oracle
new file mode 100644
index 00000000000..8027660c48a
--- /dev/null
+++ b/tests/value/oracle_symblocs/domains_function.res.oracle
@@ -0,0 +1,38 @@
+19,20c19
+< [eva] tests/value/domains_function.c:92:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:92: Frama_C_show_each_top: {3}
+28,29c27
+< [eva] tests/value/domains_function.c:77:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
+32,33c30
+< [eva] tests/value/domains_function.c:96:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:96: Frama_C_show_each_top: {1}
+52,56c49,50
+< [eva] computing for function not_enabled <- recursively_enabled <- main.
+< Called from tests/value/domains_function.c:110.
+< [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
+< [eva] Recording results for not_enabled
+< [eva] Done for function not_enabled
+---
+> [eva] tests/value/domains_function.c:110:
+> Reusing old results for call to not_enabled
+58,63c52,53
+< [eva] computing for function disabled <- recursively_enabled <- main.
+< Called from tests/value/domains_function.c:112.
+< [eva] tests/value/domains_function.c:84:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+< [eva] Recording results for disabled
+< [eva] Done for function disabled
+---
+> [eva] tests/value/domains_function.c:112:
+> Reusing old results for call to disabled
+130c120
+< result ∈ [--..--]
+---
+> result ∈ {1}
diff --git a/tests/value/oracle_symblocs/downcast.0.res.oracle b/tests/value/oracle_symblocs/downcast.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/downcast.1.res.oracle b/tests/value/oracle_symblocs/downcast.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/downcast.2.res.oracle b/tests/value/oracle_symblocs/downcast.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/downcast.3.res.oracle b/tests/value/oracle_symblocs/downcast.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/downcast.4.res.oracle b/tests/value/oracle_symblocs/downcast.4.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/dur.res.oracle b/tests/value/oracle_symblocs/dur.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_base.0.res.oracle b/tests/value/oracle_symblocs/empty_base.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_base.1.res.oracle b/tests/value/oracle_symblocs/empty_base.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_struct.0.res.oracle b/tests/value/oracle_symblocs/empty_struct.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_struct.1.res.oracle b/tests/value/oracle_symblocs/empty_struct.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_struct.2.res.oracle b/tests/value/oracle_symblocs/empty_struct.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_struct.3.res.oracle b/tests/value/oracle_symblocs/empty_struct.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_struct.4.res.oracle b/tests/value/oracle_symblocs/empty_struct.4.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_struct.5.res.oracle b/tests/value/oracle_symblocs/empty_struct.5.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_struct.6.res.oracle b/tests/value/oracle_symblocs/empty_struct.6.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_struct2.res.oracle b/tests/value/oracle_symblocs/empty_struct2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/empty_union.res.oracle b/tests/value/oracle_symblocs/empty_union.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/endian.0.res.oracle b/tests/value/oracle_symblocs/endian.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/endian.1.res.oracle b/tests/value/oracle_symblocs/endian.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/enum.res.oracle b/tests/value/oracle_symblocs/enum.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/enum2.res.oracle b/tests/value/oracle_symblocs/enum2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/equality.res.oracle b/tests/value/oracle_symblocs/equality.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/eval_separated.res.oracle b/tests/value/oracle_symblocs/eval_separated.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/exit_paths.res.oracle b/tests/value/oracle_symblocs/exit_paths.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/extern.res.oracle b/tests/value/oracle_symblocs/extern.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/f1.res.oracle b/tests/value/oracle_symblocs/f1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/f2.res.oracle b/tests/value/oracle_symblocs/f2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/false.res.oracle b/tests/value/oracle_symblocs/false.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/fam_sizeof.res.oracle b/tests/value/oracle_symblocs/fam_sizeof.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/find_ivaltop.res.oracle b/tests/value/oracle_symblocs/find_ivaltop.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/folding.res.oracle b/tests/value/oracle_symblocs/folding.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/for_loops.0.res.oracle b/tests/value/oracle_symblocs/for_loops.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/for_loops.1.res.oracle b/tests/value/oracle_symblocs/for_loops.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/for_loops.2.res.oracle b/tests/value/oracle_symblocs/for_loops.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/for_loops.3.res.oracle b/tests/value/oracle_symblocs/for_loops.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/forall.res.oracle b/tests/value/oracle_symblocs/forall.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/fptr.0.res.oracle b/tests/value/oracle_symblocs/fptr.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/fptr.1.res.oracle b/tests/value/oracle_symblocs/fptr.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from1.res.oracle b/tests/value/oracle_symblocs/from1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_call.0.res.oracle b/tests/value/oracle_symblocs/from_call.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_call.1.res.oracle b/tests/value/oracle_symblocs/from_call.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_global.res.oracle b/tests/value/oracle_symblocs/from_global.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_ind.res.oracle b/tests/value/oracle_symblocs/from_ind.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_pb.0.res.oracle b/tests/value/oracle_symblocs/from_pb.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_pb.1.res.oracle b/tests/value/oracle_symblocs/from_pb.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_pb.2.res.oracle b/tests/value/oracle_symblocs/from_pb.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_pb.3.res.oracle b/tests/value/oracle_symblocs/from_pb.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_pb.4.res.oracle b/tests/value/oracle_symblocs/from_pb.4.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_pb.5.res.oracle b/tests/value/oracle_symblocs/from_pb.5.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_pb.6.res.oracle b/tests/value/oracle_symblocs/from_pb.6.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_pb.7.res.oracle b/tests/value/oracle_symblocs/from_pb.7.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_ptr.0.res.oracle b/tests/value/oracle_symblocs/from_ptr.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_ptr.1.res.oracle b/tests/value/oracle_symblocs/from_ptr.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_ptr2.res.oracle b/tests/value/oracle_symblocs/from_ptr2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_res_2.res.oracle b/tests/value/oracle_symblocs/from_res_2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/from_termin.res.oracle b/tests/value/oracle_symblocs/from_termin.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/fun_ptr.0.res.oracle b/tests/value/oracle_symblocs/fun_ptr.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/fun_ptr.1.res.oracle b/tests/value/oracle_symblocs/fun_ptr.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/function_return_serial_casts.res.oracle b/tests/value/oracle_symblocs/function_return_serial_casts.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/g1.res.oracle b/tests/value/oracle_symblocs/g1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/garbled_init.res.oracle b/tests/value/oracle_symblocs/garbled_init.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/gauges.res.oracle b/tests/value/oracle_symblocs/gauges.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ghost.res.oracle b/tests/value/oracle_symblocs/ghost.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/global_bug.res.oracle b/tests/value/oracle_symblocs/global_bug.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/goto.res.oracle b/tests/value/oracle_symblocs/goto.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/hierarchical_convergence.res.oracle b/tests/value/oracle_symblocs/hierarchical_convergence.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/if.0.res.oracle b/tests/value/oracle_symblocs/if.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/if.1.res.oracle b/tests/value/oracle_symblocs/if.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/if2.res.oracle b/tests/value/oracle_symblocs/if2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ilevel.res.oracle b/tests/value/oracle_symblocs/ilevel.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/implies.res.oracle b/tests/value/oracle_symblocs/implies.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/imprecise_invalid_write.res.oracle b/tests/value/oracle_symblocs/imprecise_invalid_write.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/incompatible_states.res.oracle b/tests/value/oracle_symblocs/incompatible_states.res.oracle
new file mode 100644
index 00000000000..f25e47594b3
--- /dev/null
+++ b/tests/value/oracle_symblocs/incompatible_states.res.oracle
@@ -0,0 +1,7 @@
+41,42d40
+< [eva:alarm] tests/value/incompatible_states.c:53: Warning:
+< division by zero. assert t[i] ≢ 0;
+49c47
+< [scope:rm_asserts] removing 2 assertion(s)
+---
+> [scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/value/oracle_symblocs/incorrect_reduce_expr.res.oracle b/tests/value/oracle_symblocs/incorrect_reduce_expr.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ineq.res.oracle b/tests/value/oracle_symblocs/ineq.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/infinite.res.oracle b/tests/value/oracle_symblocs/infinite.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/init.0.res.oracle b/tests/value/oracle_symblocs/init.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/init.1.res.oracle b/tests/value/oracle_symblocs/init.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/init_const_guard.res.oracle b/tests/value/oracle_symblocs/init_const_guard.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/initialized.res.oracle b/tests/value/oracle_symblocs/initialized.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/initialized_copy.0.res.oracle b/tests/value/oracle_symblocs/initialized_copy.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/initialized_copy.1.res.oracle b/tests/value/oracle_symblocs/initialized_copy.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout.0.res.oracle b/tests/value/oracle_symblocs/inout.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout.1.res.oracle b/tests/value/oracle_symblocs/inout.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout.2.res.oracle b/tests/value/oracle_symblocs/inout.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout.3.res.oracle b/tests/value/oracle_symblocs/inout.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout.4.res.oracle b/tests/value/oracle_symblocs/inout.4.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout_diff.res.oracle b/tests/value/oracle_symblocs/inout_diff.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout_formals.res.oracle b/tests/value/oracle_symblocs/inout_formals.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout_on_alarms.res.oracle b/tests/value/oracle_symblocs/inout_on_alarms.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inout_proto.res.oracle b/tests/value/oracle_symblocs/inout_proto.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/input.res.oracle b/tests/value/oracle_symblocs/input.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/integers.res.oracle b/tests/value/oracle_symblocs/integers.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/interpol.res.oracle b/tests/value/oracle_symblocs/interpol.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/interpreter-mode-syracuse.res.oracle b/tests/value/oracle_symblocs/interpreter-mode-syracuse.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/invalid_loc_return.res.oracle b/tests/value/oracle_symblocs/invalid_loc_return.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/invalid_lval_arg.res.oracle b/tests/value/oracle_symblocs/invalid_lval_arg.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/invalid_pointer.0.res.oracle b/tests/value/oracle_symblocs/invalid_pointer.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/invalid_pointer.1.res.oracle b/tests/value/oracle_symblocs/invalid_pointer.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inversion.res.oracle b/tests/value/oracle_symblocs/inversion.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/inversion2.res.oracle b/tests/value/oracle_symblocs/inversion2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/jacques.res.oracle b/tests/value/oracle_symblocs/jacques.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/join_misaligned.res.oracle b/tests/value/oracle_symblocs/join_misaligned.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/label.res.oracle b/tests/value/oracle_symblocs/label.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/lazy.0.res.oracle b/tests/value/oracle_symblocs/lazy.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/lazy.1.res.oracle b/tests/value/oracle_symblocs/lazy.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/leaf.res.oracle b/tests/value/oracle_symblocs/leaf.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/leaf2.res.oracle b/tests/value/oracle_symblocs/leaf2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/leaf_spec.0.res.oracle b/tests/value/oracle_symblocs/leaf_spec.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/leaf_spec.1.res.oracle b/tests/value/oracle_symblocs/leaf_spec.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/library.res.oracle b/tests/value/oracle_symblocs/library.res.oracle
new file mode 100644
index 00000000000..263da140a44
--- /dev/null
+++ b/tests/value/oracle_symblocs/library.res.oracle
@@ -0,0 +1,5 @@
+129,132d128
+< [eva:alarm] tests/value/library.i:44: Warning:
+< non-finite float value. assert \is_finite(*pf);
+< [eva:alarm] tests/value/library.i:44: Warning:
+< non-finite float value. assert \is_finite(\add_float(*pf, *pf));
diff --git a/tests/value/oracle_symblocs/library_precond.res.oracle b/tests/value/oracle_symblocs/library_precond.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/limits.res.oracle b/tests/value/oracle_symblocs/limits.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/local.res.oracle b/tests/value/oracle_symblocs/local.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/local_cleanup.res.oracle b/tests/value/oracle_symblocs/local_cleanup.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/local_slevel.res.oracle b/tests/value/oracle_symblocs/local_slevel.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/local_variables.res.oracle b/tests/value/oracle_symblocs/local_variables.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/lock.res.oracle b/tests/value/oracle_symblocs/lock.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/logic.res.oracle b/tests/value/oracle_symblocs/logic.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/logic_ptr_cast.res.oracle b/tests/value/oracle_symblocs/logic_ptr_cast.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/logicdeps.res.oracle b/tests/value/oracle_symblocs/logicdeps.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/long.res.oracle b/tests/value/oracle_symblocs/long.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/long_const.0.res.oracle b/tests/value/oracle_symblocs/long_const.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/long_const.1.res.oracle b/tests/value/oracle_symblocs/long_const.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop.res.oracle b/tests/value/oracle_symblocs/loop.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop1.res.oracle b/tests/value/oracle_symblocs/loop1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop2.res.oracle b/tests/value/oracle_symblocs/loop2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop3.res.oracle b/tests/value/oracle_symblocs/loop3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_array.res.oracle b/tests/value/oracle_symblocs/loop_array.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_join.res.oracle b/tests/value/oracle_symblocs/loop_join.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_long.res.oracle b/tests/value/oracle_symblocs/loop_long.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_no_var.res.oracle b/tests/value/oracle_symblocs/loop_no_var.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_simple.res.oracle b/tests/value/oracle_symblocs/loop_simple.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_test.0.res.oracle b/tests/value/oracle_symblocs/loop_test.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_test.1.res.oracle b/tests/value/oracle_symblocs/loop_test.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_wvar.0.res.oracle b/tests/value/oracle_symblocs/loop_wvar.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_wvar.1.res.oracle b/tests/value/oracle_symblocs/loop_wvar.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_wvar.2.res.oracle b/tests/value/oracle_symblocs/loop_wvar.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loop_wvar.3.res.oracle b/tests/value/oracle_symblocs/loop_wvar.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loopfun.0.res.oracle b/tests/value/oracle_symblocs/loopfun.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loopfun.1.res.oracle b/tests/value/oracle_symblocs/loopfun.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/loopinv.res.oracle b/tests/value/oracle_symblocs/loopinv.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/machdep.res.oracle b/tests/value/oracle_symblocs/machdep.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/max_pointed.res.oracle b/tests/value/oracle_symblocs/max_pointed.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/memexec.res.oracle b/tests/value/oracle_symblocs/memexec.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/merge_bits.res.oracle b/tests/value/oracle_symblocs/merge_bits.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/mini_pointrer.res.oracle b/tests/value/oracle_symblocs/mini_pointrer.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/misaligned_tabs.res.oracle b/tests/value/oracle_symblocs/misaligned_tabs.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/mixed_val.res.oracle b/tests/value/oracle_symblocs/mixed_val.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/modifies.res.oracle b/tests/value/oracle_symblocs/modifies.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/modulo.res.oracle b/tests/value/oracle_symblocs/modulo.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/multi_access.res.oracle b/tests/value/oracle_symblocs/multi_access.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/narrow_behaviors.res.oracle b/tests/value/oracle_symblocs/narrow_behaviors.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/nested_struct_init.res.oracle b/tests/value/oracle_symblocs/nested_struct_init.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/no_results.res.oracle b/tests/value/oracle_symblocs/no_results.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/non_iso_initializer.res.oracle b/tests/value/oracle_symblocs/non_iso_initializer.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/non_natural.res.oracle b/tests/value/oracle_symblocs/non_natural.res.oracle
new file mode 100644
index 00000000000..5bb2115c807
--- /dev/null
+++ b/tests/value/oracle_symblocs/non_natural.res.oracle
@@ -0,0 +1,52 @@
+58a59,60
+> [kernel] tests/value/non_natural.i:30:
+> more than 200(12500) elements to enumerate. Approximating.
+65a68,71
+> [kernel] tests/value/non_natural.i:23:
+> more than 200(12501) elements to enumerate. Approximating.
+> [kernel] tests/value/non_natural.i:23:
+> more than 200(12500) elements to enumerate. Approximating.
+70a77,80
+> [kernel] tests/value/non_natural.i:24:
+> more than 200(12501) elements to enumerate. Approximating.
+> [kernel] tests/value/non_natural.i:24:
+> more than 200(12500) elements to enumerate. Approximating.
+78a89,90
+> [kernel] tests/value/non_natural.i:25:
+> more than 200(12500) elements to enumerate. Approximating.
+86a99,100
+> [kernel] tests/value/non_natural.i:26:
+> more than 200(12500) elements to enumerate. Approximating.
+94a109,110
+> [kernel] tests/value/non_natural.i:27:
+> more than 200(12500) elements to enumerate. Approximating.
+102a119,120
+> [kernel] tests/value/non_natural.i:28:
+> more than 200(12500) elements to enumerate. Approximating.
+110a129,130
+> [kernel] tests/value/non_natural.i:29:
+> more than 200(12500) elements to enumerate. Approximating.
+127,146d146
+< [kernel] tests/value/non_natural.i:23:
+< more than 200(12501) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:23:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:24:
+< more than 200(12501) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:24:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:25:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:26:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:27:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:28:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:29:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:30:
+< more than 200(12500) elements to enumerate. Approximating.
+199a200,201
+> [kernel] tests/value/non_natural.i:39:
+> more than 200(12500) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_symblocs/nonlin.res.oracle b/tests/value/oracle_symblocs/nonlin.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/noreturn.res.oracle b/tests/value/oracle_symblocs/noreturn.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/not.res.oracle b/tests/value/oracle_symblocs/not.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/not_ct_array_arg.res.oracle b/tests/value/oracle_symblocs/not_ct_array_arg.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/null_lt_valid.res.oracle b/tests/value/oracle_symblocs/null_lt_valid.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/octagons.res.oracle b/tests/value/oracle_symblocs/octagons.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/offset_misaligned.res.oracle b/tests/value/oracle_symblocs/offset_misaligned.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/offset_neg.res.oracle b/tests/value/oracle_symblocs/offset_neg.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/offset_top.res.oracle b/tests/value/oracle_symblocs/offset_top.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/offsetmap.0.res.oracle b/tests/value/oracle_symblocs/offsetmap.0.res.oracle
new file mode 100644
index 00000000000..6bebb89e738
--- /dev/null
+++ b/tests/value/oracle_symblocs/offsetmap.0.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
diff --git a/tests/value/oracle_symblocs/offsetmap.1.res.oracle b/tests/value/oracle_symblocs/offsetmap.1.res.oracle
new file mode 100644
index 00000000000..6bebb89e738
--- /dev/null
+++ b/tests/value/oracle_symblocs/offsetmap.1.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
diff --git a/tests/value/oracle_symblocs/origin.0.res.oracle b/tests/value/oracle_symblocs/origin.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/origin.1.res.oracle b/tests/value/oracle_symblocs/origin.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/output_leafs.res.oracle b/tests/value/oracle_symblocs/output_leafs.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/overflow.0.res.oracle b/tests/value/oracle_symblocs/overflow.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/overflow.1.res.oracle b/tests/value/oracle_symblocs/overflow.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/overflow_cast_float_int.res.oracle b/tests/value/oracle_symblocs/overflow_cast_float_int.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/packed.res.oracle b/tests/value/oracle_symblocs/packed.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/partitioning-annots.0.res.oracle b/tests/value/oracle_symblocs/partitioning-annots.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/partitioning-annots.1.res.oracle b/tests/value/oracle_symblocs/partitioning-annots.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/partitioning-annots.2.res.oracle b/tests/value/oracle_symblocs/partitioning-annots.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/partitioning-annots.3.res.oracle b/tests/value/oracle_symblocs/partitioning-annots.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/partitioning-annots.4.res.oracle b/tests/value/oracle_symblocs/partitioning-annots.4.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/partitioning-annots.5.res.oracle b/tests/value/oracle_symblocs/partitioning-annots.5.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/partitioning-annots.6.res.oracle b/tests/value/oracle_symblocs/partitioning-annots.6.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pb.res.oracle b/tests/value/oracle_symblocs/pb.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/period.res.oracle b/tests/value/oracle_symblocs/period.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/plevel.res.oracle b/tests/value/oracle_symblocs/plevel.res.oracle
new file mode 100644
index 00000000000..d19a038f2cb
--- /dev/null
+++ b/tests/value/oracle_symblocs/plevel.res.oracle
@@ -0,0 +1,4 @@
+12d11
+< [eva] Recording results for main
+14a14
+> [eva] Recording results for main
diff --git a/tests/value/oracle_symblocs/pointer.res.oracle b/tests/value/oracle_symblocs/pointer.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer2.0.res.oracle b/tests/value/oracle_symblocs/pointer2.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer2.1.res.oracle b/tests/value/oracle_symblocs/pointer2.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer3.res.oracle b/tests/value/oracle_symblocs/pointer3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer4.res.oracle b/tests/value/oracle_symblocs/pointer4.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer_arg.res.oracle b/tests/value/oracle_symblocs/pointer_arg.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer_comp.res.oracle b/tests/value/oracle_symblocs/pointer_comp.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer_comparison.0.res.oracle b/tests/value/oracle_symblocs/pointer_comparison.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer_comparison.1.res.oracle b/tests/value/oracle_symblocs/pointer_comparison.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer_int_cast.res.oracle b/tests/value/oracle_symblocs/pointer_int_cast.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pointer_loop.res.oracle b/tests/value/oracle_symblocs/pointer_loop.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/postcond_leaf.res.oracle b/tests/value/oracle_symblocs/postcond_leaf.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/postcondition.res.oracle b/tests/value/oracle_symblocs/postcondition.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pragma.res.oracle b/tests/value/oracle_symblocs/pragma.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/precise_locations.res.oracle b/tests/value/oracle_symblocs/precise_locations.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/precond.res.oracle b/tests/value/oracle_symblocs/precond.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/precond2.0.res.oracle b/tests/value/oracle_symblocs/precond2.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/precond2.1.res.oracle b/tests/value/oracle_symblocs/precond2.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/propagate_bottom.res.oracle b/tests/value/oracle_symblocs/propagate_bottom.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/protomain.res.oracle b/tests/value/oracle_symblocs/protomain.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ptr_call_object.res.oracle b/tests/value/oracle_symblocs/ptr_call_object.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ptr_relation.0.res.oracle b/tests/value/oracle_symblocs/ptr_relation.0.res.oracle
new file mode 100644
index 00000000000..0ae744ec7d6
--- /dev/null
+++ b/tests/value/oracle_symblocs/ptr_relation.0.res.oracle
@@ -0,0 +1,4 @@
+23c23
+< i ∈ {0; 77; 333}
+---
+> i ∈ {77}
diff --git a/tests/value/oracle_symblocs/ptr_relation.1.res.oracle b/tests/value/oracle_symblocs/ptr_relation.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ptr_relation.2.res.oracle b/tests/value/oracle_symblocs/ptr_relation.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/pure_exp.res.oracle b/tests/value/oracle_symblocs/pure_exp.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/qualified_arrays.res.oracle b/tests/value/oracle_symblocs/qualified_arrays.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/raz.res.oracle b/tests/value/oracle_symblocs/raz.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/reading_null.res.oracle b/tests/value/oracle_symblocs/reading_null.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/rec.res.oracle b/tests/value/oracle_symblocs/rec.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/recol.0.res.oracle b/tests/value/oracle_symblocs/recol.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/recol.1.res.oracle b/tests/value/oracle_symblocs/recol.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/recursion.0.res.oracle b/tests/value/oracle_symblocs/recursion.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/recursion.1.res.oracle b/tests/value/oracle_symblocs/recursion.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/recursion2.res.oracle b/tests/value/oracle_symblocs/recursion2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/reduce_by_valid.res.oracle b/tests/value/oracle_symblocs/reduce_by_valid.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/reduce_formals.res.oracle b/tests/value/oracle_symblocs/reduce_formals.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/reduce_index.res.oracle b/tests/value/oracle_symblocs/reduce_index.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/reduce_valid.res.oracle b/tests/value/oracle_symblocs/reduce_valid.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/redundant_alarms.res.oracle b/tests/value/oracle_symblocs/redundant_alarms.res.oracle
new file mode 100644
index 00000000000..e407fdc210c
--- /dev/null
+++ b/tests/value/oracle_symblocs/redundant_alarms.res.oracle
@@ -0,0 +1,41 @@
+10,13d9
+< [eva:alarm] tests/value/redundant_alarms.c:11: Warning:
+< accessing uninitialized left-value. assert \initialized(p);
+< [eva:alarm] tests/value/redundant_alarms.c:12: Warning:
+< accessing uninitialized left-value. assert \initialized(p);
+24,27d19
+< [eva:alarm] tests/value/redundant_alarms.c:21: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[i]);
+< [eva:alarm] tests/value/redundant_alarms.c:22: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[i]);
+38,41d29
+< [eva:alarm] tests/value/redundant_alarms.c:32: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[j]);
+< [eva:alarm] tests/value/redundant_alarms.c:33: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[i]);
+63,69d50
+< [scope:rm_asserts] removing 3 assertion(s)
+< [scope:rm_asserts] tests/value/redundant_alarms.c:12:
+< removing redundant assert Eva: initialization: \initialized(p);
+< [scope:rm_asserts] tests/value/redundant_alarms.c:32:
+< removing redundant assert Eva: initialization: \initialized(&t[j]);
+< [scope:rm_asserts] tests/value/redundant_alarms.c:33:
+< removing redundant assert Eva: initialization: \initialized(&t[i]);
+108d88
+< /*@ assert Eva: initialization: \initialized(p); */
+110d89
+< /*@ assert Eva: initialization: \initialized(p); */
+127d105
+< /*@ assert Eva: initialization: \initialized(&t[i]); */
+129d106
+< /*@ assert Eva: initialization: \initialized(&t[i]); */
+142d118
+< /*@ assert Eva: initialization: \initialized(&t[j]); */
+144d119
+< /*@ assert Eva: initialization: \initialized(&t[i]); */
+196a172
+> int z;
+199,201d174
+< *p = 1;
+< int z = *p + 1;
+< int w = *p + 2;
diff --git a/tests/value/oracle_symblocs/reevaluate_alarms.res.oracle b/tests/value/oracle_symblocs/reevaluate_alarms.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/relation_reduction.res.oracle b/tests/value/oracle_symblocs/relation_reduction.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/relation_shift.res.oracle b/tests/value/oracle_symblocs/relation_shift.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/relations.res.oracle b/tests/value/oracle_symblocs/relations.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/relations2.res.oracle b/tests/value/oracle_symblocs/relations2.res.oracle
new file mode 100644
index 00000000000..51123dbb845
--- /dev/null
+++ b/tests/value/oracle_symblocs/relations2.res.oracle
@@ -0,0 +1,2 @@
+133d132
+< [eva] tests/value/relations2.i:57: Frama_C_show_each_NO2:
diff --git a/tests/value/oracle_symblocs/relations_difficult.res.oracle b/tests/value/oracle_symblocs/relations_difficult.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/replace_by_show_each.res.oracle b/tests/value/oracle_symblocs/replace_by_show_each.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/resolve.res.oracle b/tests/value/oracle_symblocs/resolve.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/return.res.oracle b/tests/value/oracle_symblocs/return.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/semaphore.res.oracle b/tests/value/oracle_symblocs/semaphore.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/separated.res.oracle b/tests/value/oracle_symblocs/separated.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/shift.0.res.oracle b/tests/value/oracle_symblocs/shift.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/shift.1.res.oracle b/tests/value/oracle_symblocs/shift.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/shift_big.res.oracle b/tests/value/oracle_symblocs/shift_big.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/shift_neg.0.res.oracle b/tests/value/oracle_symblocs/shift_neg.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/shift_neg.1.res.oracle b/tests/value/oracle_symblocs/shift_neg.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/sign_of_bitfiled_int.0.res.oracle b/tests/value/oracle_symblocs/sign_of_bitfiled_int.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/sign_of_bitfiled_int.1.res.oracle b/tests/value/oracle_symblocs/sign_of_bitfiled_int.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/simple_packed.res.oracle b/tests/value/oracle_symblocs/simple_packed.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/simple_path.res.oracle b/tests/value/oracle_symblocs/simple_path.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/simplify_cfg.0.res.oracle b/tests/value/oracle_symblocs/simplify_cfg.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/simplify_cfg.1.res.oracle b/tests/value/oracle_symblocs/simplify_cfg.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/sizeof.res.oracle b/tests/value/oracle_symblocs/sizeof.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/slevel_return.res.oracle b/tests/value/oracle_symblocs/slevel_return.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/slevelex.res.oracle b/tests/value/oracle_symblocs/slevelex.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/small_conditionals.res.oracle b/tests/value/oracle_symblocs/small_conditionals.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/sort4.0.res.oracle b/tests/value/oracle_symblocs/sort4.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/sort4.1.res.oracle b/tests/value/oracle_symblocs/sort4.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/sort4.2.res.oracle b/tests/value/oracle_symblocs/sort4.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/split_return.0.res.oracle b/tests/value/oracle_symblocs/split_return.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/split_return.1.res.oracle b/tests/value/oracle_symblocs/split_return.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/split_return.2.res.oracle b/tests/value/oracle_symblocs/split_return.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/split_return.3.res.oracle b/tests/value/oracle_symblocs/split_return.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/split_return.4.res.oracle b/tests/value/oracle_symblocs/split_return.4.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/statement_contract.res.oracle b/tests/value/oracle_symblocs/statement_contract.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/static.res.oracle b/tests/value/oracle_symblocs/static.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/strange.res.oracle b/tests/value/oracle_symblocs/strange.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/strings.res.oracle b/tests/value/oracle_symblocs/strings.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/strings_cond.res.oracle b/tests/value/oracle_symblocs/strings_cond.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/struct.res.oracle b/tests/value/oracle_symblocs/struct.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/struct2.res.oracle b/tests/value/oracle_symblocs/struct2.res.oracle
new file mode 100644
index 00000000000..a2e06e1f458
--- /dev/null
+++ b/tests/value/oracle_symblocs/struct2.res.oracle
@@ -0,0 +1,27 @@
+55a56,57
+> [kernel] tests/value/struct2.i:78: Warning:
+> all target addresses were invalid. This path is assumed to be dead.
+59,60d60
+< accessing out of bounds index. assert 0 ≤ (int)(tab2[i] + j);
+< [eva:alarm] tests/value/struct2.i:82: Warning:
+83,84d82
+< accessing out of bounds index. assert (int)(i + j) < 2;
+< [eva:alarm] tests/value/struct2.i:185: Warning:
+106c104
+< [scope:rm_asserts] removing 2 assertion(s)
+---
+> [scope:rm_asserts] removing 1 assertion(s)
+144,145c142
+< tab4[0] ∈ {0; 2}
+< [1] ∈ {0}
+---
+> tab4[0..1] ∈ {0}
+148c145,146
+< tab6[0..1] ∈ {0; 2}
+---
+> tab6[0] ∈ {0}
+> [1] ∈ {2}
+219c217
+< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
+---
+> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
diff --git a/tests/value/oracle_symblocs/struct3.res.oracle b/tests/value/oracle_symblocs/struct3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/struct_array.res.oracle b/tests/value/oracle_symblocs/struct_array.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/struct_call.0.res.oracle b/tests/value/oracle_symblocs/struct_call.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/struct_call.1.res.oracle b/tests/value/oracle_symblocs/struct_call.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/struct_deps.res.oracle b/tests/value/oracle_symblocs/struct_deps.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/struct_incl.res.oracle b/tests/value/oracle_symblocs/struct_incl.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/struct_p_call.res.oracle b/tests/value/oracle_symblocs/struct_p_call.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/strucval.res.oracle b/tests/value/oracle_symblocs/strucval.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/subset.res.oracle b/tests/value/oracle_symblocs/subset.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/summary.0.res.oracle b/tests/value/oracle_symblocs/summary.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/summary.1.res.oracle b/tests/value/oracle_symblocs/summary.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/summary.2.res.oracle b/tests/value/oracle_symblocs/summary.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/summary.3.res.oracle b/tests/value/oracle_symblocs/summary.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/summary.4.res.oracle b/tests/value/oracle_symblocs/summary.4.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/switch.0.res.oracle b/tests/value/oracle_symblocs/switch.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/switch.1.res.oracle b/tests/value/oracle_symblocs/switch.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/switch2.res.oracle b/tests/value/oracle_symblocs/switch2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/switch_cast.res.oracle b/tests/value/oracle_symblocs/switch_cast.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/symbolic_locs.res.oracle b/tests/value/oracle_symblocs/symbolic_locs.res.oracle
new file mode 100644
index 00000000000..6f9fd51c1da
--- /dev/null
+++ b/tests/value/oracle_symblocs/symbolic_locs.res.oracle
@@ -0,0 +1,71 @@
+20a21,26
+> # Symbolic locations domain:
+> V: {[ t[i] -> {4} ]}
+> Z: {[ t[i] -> t[0..8]; i ]}
+> I: {[ t -> {t[i]}
+> i -> {t[i]} ]}
+> S: {[ i -> {t[i]} ]}
+31a38,42
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+48a60,65
+> # Symbolic locations domain:
+> V: {[ t[i] -> {4} ]}
+> Z: {[ t[i] -> t[0..8]; i ]}
+> I: {[ t -> {t[i]}
+> i -> {t[i]} ]}
+> S: {[ i -> {t[i]} ]}
+59a77,81
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+79a102,108
+> # Symbolic locations domain:
+> V: {[ t[i] -> {{ &x }} ]}
+> Z: {[ t[i] -> t[0..8]; i ]}
+> I: {[ t -> {t[i]}
+> i -> {t[i]} ]}
+> S: {[ i -> {t[i]}
+> x -> {t[i]} ]}
+92a122,126
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+108a143,148
+> # Symbolic locations domain:
+> V: {[ t[i] -> {1} ]}
+> Z: {[ t[i] -> t[0..8]; i ]}
+> I: {[ t -> {t[i]}
+> i -> {t[i]} ]}
+> S: {[ i -> {t[i]} ]}
+117a158,162
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+134a180,184
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
+141,143c191
+< [eva:alarm] tests/value/symbolic_locs.i:111: Warning:
+< signed overflow. assert *p + 1 ≤ 2147483647;
+< [eva] tests/value/symbolic_locs.i:113: Frama_C_show_each: [0..2147483647]
+---
+> [eva] tests/value/symbolic_locs.i:113: Frama_C_show_each: [10001..2147483647]
+152a201,205
+> # Symbolic locations domain:
+> V: {[ ]}
+> Z: {[ ]}
+> I: {[ ]}
+> S: {[ ]}
diff --git a/tests/value/oracle_symblocs/tab.res.oracle b/tests/value/oracle_symblocs/tab.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/tab1.res.oracle b/tests/value/oracle_symblocs/tab1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/termination.res.oracle b/tests/value/oracle_symblocs/termination.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/test.0.res.oracle b/tests/value/oracle_symblocs/test.0.res.oracle
new file mode 100644
index 00000000000..272fc4fdee9
--- /dev/null
+++ b/tests/value/oracle_symblocs/test.0.res.oracle
@@ -0,0 +1,4 @@
+31c31
+< tmp ∈ [--..--] or UNINITIALIZED
+---
+> tmp ∈ [-2147483647..2147483647] or UNINITIALIZED
diff --git a/tests/value/oracle_symblocs/test.1.res.oracle b/tests/value/oracle_symblocs/test.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/test_arith.res.oracle b/tests/value/oracle_symblocs/test_arith.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/threat_array.res.oracle b/tests/value/oracle_symblocs/threat_array.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/threat_if.res.oracle b/tests/value/oracle_symblocs/threat_if.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/threat_redundant.res.oracle b/tests/value/oracle_symblocs/threat_redundant.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/tricky_logic.res.oracle b/tests/value/oracle_symblocs/tricky_logic.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/typedef_function.res.oracle b/tests/value/oracle_symblocs/typedef_function.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/typeof.res.oracle b/tests/value/oracle_symblocs/typeof.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ulongvslonglong.0.res.oracle b/tests/value/oracle_symblocs/ulongvslonglong.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/ulongvslonglong.1.res.oracle b/tests/value/oracle_symblocs/ulongvslonglong.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/undef_behavior_bts1059.res.oracle b/tests/value/oracle_symblocs/undef_behavior_bts1059.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/undef_fct.res.oracle b/tests/value/oracle_symblocs/undef_fct.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/undefined_sequence.0.res.oracle b/tests/value/oracle_symblocs/undefined_sequence.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/undefined_sequence.1.res.oracle b/tests/value/oracle_symblocs/undefined_sequence.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/undefined_sequence2.res.oracle b/tests/value/oracle_symblocs/undefined_sequence2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/uninit.res.oracle b/tests/value/oracle_symblocs/uninit.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/uninit_callstack.res.oracle b/tests/value/oracle_symblocs/uninit_callstack.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/uninitialized_gnubody.res.oracle b/tests/value/oracle_symblocs/uninitialized_gnubody.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/unknown_sizeof.0.res.oracle b/tests/value/oracle_symblocs/unknown_sizeof.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/unknown_sizeof.1.res.oracle b/tests/value/oracle_symblocs/unknown_sizeof.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/unop.res.oracle b/tests/value/oracle_symblocs/unop.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/unroll.res.oracle b/tests/value/oracle_symblocs/unroll.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/unroll_simple.res.oracle b/tests/value/oracle_symblocs/unroll_simple.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/unsigned_overflow.res.oracle b/tests/value/oracle_symblocs/unsigned_overflow.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/use_spec.0.res.oracle b/tests/value/oracle_symblocs/use_spec.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/use_spec.1.res.oracle b/tests/value/oracle_symblocs/use_spec.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/user_assertion_uninit_var.res.oracle b/tests/value/oracle_symblocs/user_assertion_uninit_var.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/usp.res.oracle b/tests/value/oracle_symblocs/usp.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/va_list.0.res.oracle b/tests/value/oracle_symblocs/va_list.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/va_list.1.res.oracle b/tests/value/oracle_symblocs/va_list.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/va_list2.0.res.oracle b/tests/value/oracle_symblocs/va_list2.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/va_list2.1.res.oracle b/tests/value/oracle_symblocs/va_list2.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val6.0.res.oracle b/tests/value/oracle_symblocs/val6.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val6.1.res.oracle b/tests/value/oracle_symblocs/val6.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val_if.0.res.oracle b/tests/value/oracle_symblocs/val_if.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val_if.1.res.oracle b/tests/value/oracle_symblocs/val_if.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val_if.2.res.oracle b/tests/value/oracle_symblocs/val_if.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val_ptr.0.res.oracle b/tests/value/oracle_symblocs/val_ptr.0.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val_ptr.1.res.oracle b/tests/value/oracle_symblocs/val_ptr.1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val_ptr.2.res.oracle b/tests/value/oracle_symblocs/val_ptr.2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/val_ptr.3.res.oracle b/tests/value/oracle_symblocs/val_ptr.3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/video_detect.res.oracle b/tests/value/oracle_symblocs/video_detect.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/volatile.res.oracle b/tests/value/oracle_symblocs/volatile.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/volatile2.res.oracle b/tests/value/oracle_symblocs/volatile2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/volatilestruct.res.oracle b/tests/value/oracle_symblocs/volatilestruct.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/wide_string.res.oracle b/tests/value/oracle_symblocs/wide_string.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/widen_non_constant.res.oracle b/tests/value/oracle_symblocs/widen_non_constant.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/widen_on_non_monotonic.res.oracle b/tests/value/oracle_symblocs/widen_on_non_monotonic.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/widen_overflow.res.oracle b/tests/value/oracle_symblocs/widen_overflow.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/widening_thresholds.res.oracle b/tests/value/oracle_symblocs/widening_thresholds.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/with_comment.res.oracle b/tests/value/oracle_symblocs/with_comment.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/oracle_symblocs/zerolengtharrays.res.oracle b/tests/value/oracle_symblocs/zerolengtharrays.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab