diff --git a/tests/value/domains_function.c b/tests/value/domains_function.c
new file mode 100644
index 0000000000000000000000000000000000000000..e81f3e8c8dca745264423d081f29bb7c163c5dbf
--- /dev/null
+++ b/tests/value/domains_function.c
@@ -0,0 +1,123 @@
+/* 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 ();
+}
diff --git a/tests/value/oracle/domains_function.res.oracle b/tests/value/oracle/domains_function.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..51ded1eb5fd5e3357568dc1f23ce53933d9e762c
--- /dev/null
+++ b/tests/value/oracle/domains_function.res.oracle
@@ -0,0 +1,272 @@
+[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]