[Eva] Adds a test of the -eva-domains-function option.

tests/value/domains_function.c

+/* run.config*
+   STDOPT: #"-eva-domains-function symbolic-locations:infer+w,symbolic-locations:use+r,symbolic-locations:test_propagation-,symbolic-locations:enabled,symbolic-locations:disabled-,symbolic-locations:recursively_enabled+"
+*/
+
+#include <__fc_builtin.h>
+
+/* Tests the -eva-domains-function option that enables a domain for the given
+   functions. This test uses the symbolic locations domain to store the value
+   of the location t[i] where [i] is imprecise, from an assignment of t[i]
+   to a read of t[i].
+   If the domain is not enabled, the value of t[i] remains imprecise because
+   [i] is imprecise. If the domain is enabled, the value of the first assignemnt
+   is stored until the read. If the assignment and the read are in different
+   functions, the domain should also be enabled in all functions in between. */
+
+volatile int undet;
+int i, result, t[10];
+
+/* No interaction with the known properties about t[i]. */
+void nothing () {
+  int tmp = t[i] - t[0];
+}
+
+/* Modify the value of t[i]. */
+void kill () {
+  t[0] = undet;
+}
+
+/* The domain has write access on this function: it infers the value of t[i]. */
+void infer () {
+  t[i] = 42;
+}
+
+/* The domain has no write access on this function. */
+void no_infer () {
+  t[i] = 42;
+}
+
+/* The domain has read access on this function: it can use the value of t[i]. */
+void use () {
+  result = t[i];
+}
+
+/* The domain has no read access on this function. */
+void no_use () {
+  result = t[i];
+}
+
+/* Test the propagation of information about t[i] from function [infer]
+   to function [use]. All other combinations of functions should not be
+   precise. */
+void test_propagation () {
+  infer ();
+  no_use ();
+  Frama_C_show_each_top(result);
+  nothing ();
+  use ();
+  Frama_C_show_each_singleton(result);
+  kill ();
+  use ();
+  Frama_C_show_each_top(result);
+  no_infer ();
+  use ();
+  Frama_C_show_each_top(result);
+}
+
+/* The domain is enabled on this function. */
+void enabled () {
+  t[i] = 0;
+  result = t[i];
+}
+
+/* The domain is not enabled on this function. */
+void not_enabled () {
+  t[i] = 1;
+  result = t[i];
+  Frama_C_show_each_top(result);
+}
+
+/* The domain is disabled on this function. */
+void disabled () {
+  t[i] = 2;
+  result = t[i];
+  Frama_C_show_each_top(result);
+}
+
+/* Precise result only after [enabled], since it is the only function
+   where the domain is enabled. */
+void test () {
+  t[i] = 3;
+  result = t[i];
+  Frama_C_show_each_top(result);
+  enabled ();
+  Frama_C_show_each_singleton(result);
+  not_enabled ();
+  Frama_C_show_each_top(result);
+  disabled ();
+  Frama_C_show_each_top(result);
+}
+
+/* The domain is recursively enabled in this function and all functions called
+   from it: the results should be precise, except after [disabled] where the
+   domain is specifically disabled.*/
+void recursively_enabled () {
+  t[i] = 4;
+  result = t[i];
+  Frama_C_show_each_singleton(result);
+  enabled ();
+  Frama_C_show_each_singleton(result);
+  not_enabled ();
+  Frama_C_show_each_singleton(result);
+  disabled ();
+  Frama_C_show_each_top(result);
+}
+
+void main () {
+  for (int j = 0; j < 10; j++)
+    t[j] = undet;
+  i = Frama_C_interval(0,9);
+  test ();
+  recursively_enabled ();
+  test_propagation ();
+}

tests/value/oracle/domains_function.res.oracle

+[kernel] Parsing tests/value/domains_function.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  undet ∈ [--..--]
+  i ∈ {0}
+  result ∈ {0}
+  t[0..9] ∈ {0}
+[eva] tests/value/domains_function.c:117: starting to merge loop iterations
+[eva] computing for function Frama_C_interval <- main.
+  Called from tests/value/domains_function.c:119.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/domains_function.c:119: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function test <- main.
+  Called from tests/value/domains_function.c:120.
+[eva] tests/value/domains_function.c:92: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] computing for function enabled <- test <- main.
+  Called from tests/value/domains_function.c:93.
+[eva] Recording results for enabled
+[eva] Done for function enabled
+[eva] tests/value/domains_function.c:94: Frama_C_show_each_singleton: {0}
+[eva] computing for function not_enabled <- test <- main.
+  Called from tests/value/domains_function.c:95.
+[eva] tests/value/domains_function.c:77: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for not_enabled
+[eva] Done for function not_enabled
+[eva] tests/value/domains_function.c:96: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] computing for function disabled <- test <- main.
+  Called from tests/value/domains_function.c:97.
+[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:98: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for test
+[eva] Done for function test
+[eva] computing for function recursively_enabled <- main.
+  Called from tests/value/domains_function.c:121.
+[eva] tests/value/domains_function.c:107: Frama_C_show_each_singleton: {4}
+[eva] computing for function enabled <- recursively_enabled <- main.
+  Called from tests/value/domains_function.c:108.
+[eva] Recording results for enabled
+[eva] Done for function enabled
+[eva] tests/value/domains_function.c:109: Frama_C_show_each_singleton: {0}
+[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:111: Frama_C_show_each_singleton: {1}
+[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:113: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for recursively_enabled
+[eva] Done for function recursively_enabled
+[eva] computing for function test_propagation <- main.
+  Called from tests/value/domains_function.c:122.
+[eva] computing for function infer <- test_propagation <- main.
+  Called from tests/value/domains_function.c:53.
+[eva] Recording results for infer
+[eva] Done for function infer
+[eva] computing for function no_use <- test_propagation <- main.
+  Called from tests/value/domains_function.c:54.
+[eva] Recording results for no_use
+[eva] Done for function no_use
+[eva] tests/value/domains_function.c:55: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] computing for function nothing <- test_propagation <- main.
+  Called from tests/value/domains_function.c:56.
+[eva:alarm] tests/value/domains_function.c:21: Warning: 
+  signed overflow. assert -2147483648 ≤ t[i] - t[0];
+[eva:alarm] tests/value/domains_function.c:21: Warning: 
+  signed overflow. assert t[i] - t[0] ≤ 2147483647;
+[eva] Recording results for nothing
+[eva] Done for function nothing
+[eva] computing for function use <- test_propagation <- main.
+  Called from tests/value/domains_function.c:57.
+[eva] Recording results for use
+[eva] Done for function use
+[eva] tests/value/domains_function.c:58: Frama_C_show_each_singleton: {42}
+[eva] computing for function kill <- test_propagation <- main.
+  Called from tests/value/domains_function.c:59.
+[eva] Recording results for kill
+[eva] Done for function kill
+[eva] computing for function use <- test_propagation <- main.
+  Called from tests/value/domains_function.c:60.
+[eva] Recording results for use
+[eva] Done for function use
+[eva] tests/value/domains_function.c:61: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] computing for function no_infer <- test_propagation <- main.
+  Called from tests/value/domains_function.c:62.
+[eva] Recording results for no_infer
+[eva] Done for function no_infer
+[eva] tests/value/domains_function.c:63: Reusing old results for call to use
+[eva] tests/value/domains_function.c:64: 
+  Frama_C_show_each_top: [-2147483648..2147483647]
+[eva] Recording results for test_propagation
+[eva] Done for function test_propagation
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function disabled:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function enabled:
+  result ∈ {0}
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function infer:
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function kill:
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function no_infer:
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function no_use:
+  result ∈ [--..--]
+[eva:final-states] Values at end of function not_enabled:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function nothing:
+  tmp ∈ [--..--]
+[eva:final-states] Values at end of function recursively_enabled:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function test:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function use:
+  result ∈ [--..--]
+[eva:final-states] Values at end of function test_propagation:
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[eva:final-states] Values at end of function main:
+  Frama_C_entropy_source ∈ [--..--]
+  i ∈ [0..9]
+  result ∈ [--..--]
+  t[0..9] ∈ [--..--]
+[from] Computing for function disabled
+[from] Done for function disabled
+[from] Computing for function enabled
+[from] Done for function enabled
+[from] Computing for function infer
+[from] Done for function infer
+[from] Computing for function kill
+[from] Done for function kill
+[from] Computing for function no_infer
+[from] Done for function no_infer
+[from] Computing for function no_use
+[from] Done for function no_use
+[from] Computing for function not_enabled
+[from] Done for function not_enabled
+[from] Computing for function nothing
+[from] Done for function nothing
+[from] Computing for function recursively_enabled
+[from] Done for function recursively_enabled
+[from] Computing for function test
+[from] Done for function test
+[from] Computing for function use
+[from] Done for function use
+[from] Computing for function test_propagation
+[from] Done for function test_propagation
+[from] Computing for function main
+[from] Computing for function Frama_C_interval <-main
+[from] Done for function Frama_C_interval
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; min; max
+[from] Function disabled:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function enabled:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function infer:
+  t[0..9] FROM i (and SELF)
+[from] Function kill:
+  t[0] FROM undet
+[from] Function no_infer:
+  t[0..9] FROM i (and SELF)
+[from] Function no_use:
+  result FROM i; t[0..9]
+[from] Function not_enabled:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function nothing:
+  NO EFFECTS
+[from] Function recursively_enabled:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function test:
+  result FROM i; t[0..9]
+  t[0..9] FROM i (and SELF)
+[from] Function use:
+  result FROM i; t[0..9]
+[from] Function test_propagation:
+  result FROM undet; i; t[1..9]
+  t[0] FROM undet; i
+   [1..9] FROM i (and SELF)
+[from] Function main:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  i FROM Frama_C_entropy_source
+  result FROM Frama_C_entropy_source; undet; t[1..9]
+  t[0] FROM Frama_C_entropy_source; undet
+   [1..9] FROM Frama_C_entropy_source; undet (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function disabled:
+    result; t[0..9]
+[inout] Inputs for function disabled:
+    i; result; t[0..9]
+[inout] Out (internal) for function enabled:
+    result; t[0..9]
+[inout] Inputs for function enabled:
+    i; t[0..9]
+[inout] Out (internal) for function infer:
+    t[0..9]
+[inout] Inputs for function infer:
+    i
+[inout] Out (internal) for function kill:
+    t[0]
+[inout] Inputs for function kill:
+    undet
+[inout] Out (internal) for function no_infer:
+    t[0..9]
+[inout] Inputs for function no_infer:
+    i
+[inout] Out (internal) for function no_use:
+    result
+[inout] Inputs for function no_use:
+    i; t[0..9]
+[inout] Out (internal) for function not_enabled:
+    result; t[0..9]
+[inout] Inputs for function not_enabled:
+    i; result; t[0..9]
+[inout] Out (internal) for function nothing:
+    tmp
+[inout] Inputs for function nothing:
+    i; t[0..9]
+[inout] Out (internal) for function recursively_enabled:
+    result; t[0..9]
+[inout] Inputs for function recursively_enabled:
+    i; result; t[0..9]
+[inout] Out (internal) for function test:
+    result; t[0..9]
+[inout] Inputs for function test:
+    i; result; t[0..9]
+[inout] Out (internal) for function use:
+    result
+[inout] Inputs for function use:
+    i; t[0..9]
+[inout] Out (internal) for function test_propagation:
+    result; t[0..9]
+[inout] Inputs for function test_propagation:
+    undet; i; result; t[0..9]
+[inout] Out (internal) for function main:
+    Frama_C_entropy_source; i; result; t[0..9]; j
+[inout] Inputs for function main:
+    Frama_C_entropy_source; undet; i; result; t[0..9]