Merge branch 'fix/eva/alternative-oracles' into 'master'

[Eva] Updates alternative test oracles

See merge request frama-c/frama-c!3134

src/plugins/value/vtests

+#!/bin/bash -eu
+
+DEFAULT_TESTS=(float value idct builtins)
+CONFIGS=(apron equality bitwise symblocs gauges octagon)
+
+ARGS=("${@-}")
+
+# has_target returns 0 if at least one of the arguments is a target
+# (i.e. not an option such as "-j 8"). If so, do not run tests
+# for all default targets, only for the specified target(s)
+has_target=0
+# sets has_target=0
+function has_target() {
+    local __has_target=1
+    for f in $@; do
+        __re="\\b$f\\b" # match argument as whole word
+        if [[ "$f" =~ \.[ci]$ || \
+            ( "$f" =~ ^[A-Za-z] && "${DEFAULT_TESTS[@]}" =~ $__re ) ]]; then
+            __has_target=0
+        fi
+    done
+    return $__has_target
+}
+
+
+if has_target ${ARGS[@]}; then
+    TESTS=("${ARGS[@]}")
+else
+    TESTS="${DEFAULT_TESTS[@]} ${ARGS[@]}"
+fi
+
+echo Testing ${TESTS[@]}
+
+for A in ${CONFIGS[@]}
+do
+    echo $A
+    ./bin/ptests.opt -config $A ${TESTS[@]}
+done

tests/float/oracle_equalities/const3.1.res.oracle → tests/float/oracle_equality/const3.1.res.oracle

-23c23
+25c25
 <   d1 ∈ [0x1.16c2000000000p-133 .. 0x1.16c3000000000p-133]
 ---
 >   d1 ∈ {0x1.16c2000000000p-133}

tests/float/oracle_equalities/dr.2.res.oracle → tests/float/oracle_equality/dr.2.res.oracle

-25c25
+27c27
 < [eva] tests/float/dr.i:26: Frama_C_show_each: {0; 1}, {0; 1}
 ---
 > [eva] tests/float/dr.i:26: Frama_C_show_each: {1}, {0; 1}
-30c30
+32c32
 <   e1 ∈ {0; 1}
 ---
 >   e1 ∈ {1}