[Eva] Adds test of -eva-report-red-statuses parameter.

tests/value/oracle/red_alarms.csv

+directory	file	line	function	kind	name	#contexts	status	property
+.	red_alarms.i	90	user_assertions	Property	user check	1	Invalid or unreachable	x < 0
+.	red_alarms.i	67	partitioning	Alarm	division_by_zero	1	Unknown	(int)(i - 15) ≢ 0
+.	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
+.	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
+.	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
+.	red_alarms.i	70	in_bound	Property	precondition	1	Invalid or unreachable	positive: x ≥ 0

tests/value/oracle/red_alarms.res.oracle

+[kernel] Parsing red_alarms.i (no 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
+  nondet ∈ [--..--]
+[eva] computing for function callstack <- main.
+  Called from red_alarms.i:96.
+[eva] computing for function maybe_swap <- callstack <- main.
+  Called from red_alarms.i:24.
+[eva] red_alarms.i:9: check got status valid.
+[eva] red_alarms.i:10: check got status valid.
+[eva] Recording results for maybe_swap
+[eva] Done for function maybe_swap
+[eva] computing for function maybe_swap <- callstack <- main.
+  Called from red_alarms.i:25.
+[eva:alarm] red_alarms.i:10: Warning: check got status unknown.
+[eva] Recording results for maybe_swap
+[eva] Done for function maybe_swap
+[eva] computing for function maybe_swap <- callstack <- main.
+  Called from red_alarms.i:26.
+[eva:alarm] red_alarms.i:10: Warning: check got status invalid.
+[eva] Recording results for maybe_swap
+[eva] Done for function maybe_swap
+[eva] computing for function maybe_swap <- callstack <- main.
+  Called from red_alarms.i:27.
+[eva:alarm] red_alarms.i:12: Warning: 
+  accessing uninitialized left-value. assert \initialized(p);
+[eva] Recording results for maybe_swap
+[eva] Done for function maybe_swap
+[eva] computing for function maybe_swap <- callstack <- main.
+  Called from red_alarms.i:28.
+[eva] Recording results for maybe_swap
+[eva] Done for function maybe_swap
+[eva] computing for function maybe_swap <- callstack <- main.
+  Called from red_alarms.i:29.
+[eva:alarm] red_alarms.i:13: Warning: out of bounds read. assert \valid_read(q);
+[eva] Recording results for maybe_swap
+[eva] Done for function maybe_swap
+[eva] computing for function maybe_swap <- callstack <- main.
+  Called from red_alarms.i:32.
+[eva:alarm] red_alarms.i:9: Warning: check got status unknown.
+[eva:alarm] red_alarms.i:12: Warning: out of bounds read. assert \valid_read(p);
+[eva:alarm] red_alarms.i:13: Warning: 
+  accessing uninitialized left-value. assert \initialized(q);
+[eva] Recording results for maybe_swap
+[eva] Done for function maybe_swap
+[eva] Recording results for callstack
+[eva] Done for function callstack
+[eva] computing for function partitioning <- main.
+  Called from red_alarms.i:97.
+[eva:alarm] red_alarms.i:45: Warning: 
+  accessing out of bounds index. assert i < 32;
+[eva] red_alarms.i:47: starting to merge loop iterations
+[eva:alarm] red_alarms.i:48: Warning: out of bounds write. assert \valid(p);
+[eva] red_alarms.i:52: starting to merge loop iterations
+[eva:alarm] red_alarms.i:53: Warning: 
+  accessing out of bounds index. assert i < 32;
+[eva:alarm] red_alarms.i:57: Warning: 
+  accessing out of bounds index. assert i < 32;
+[kernel] red_alarms.i:57: Warning: 
+  all target addresses were invalid. This path is assumed to be dead.
+[eva] red_alarms.i:60: starting to merge loop iterations
+[eva:alarm] red_alarms.i:61: Warning: 
+  accessing out of bounds index. assert i < 32;
+[kernel] red_alarms.i:61: Warning: 
+  all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] red_alarms.i:64: Warning: 
+  division by zero. assert (int)(i - 5) ≢ 0;
+[eva:alarm] red_alarms.i:65: Warning: 
+  division by zero. assert (int)(i - 10) ≢ 0;
+[eva:alarm] red_alarms.i:67: Warning: 
+  division by zero. assert (int)(i - 15) ≢ 0;
+[eva] Recording results for partitioning
+[eva] Done for function partitioning
+[eva] computing for function preconditions <- main.
+  Called from red_alarms.i:98.
+[eva] computing for function in_bound <- preconditions <- main.
+  Called from red_alarms.i:79.
+[eva] red_alarms.i:79: 
+  function in_bound: precondition 'positive' got status valid.
+[eva] red_alarms.i:79: 
+  function in_bound: precondition 'bounded' got status valid.
+[eva] Recording results for in_bound
+[eva] Done for function in_bound
+[eva] computing for function in_bound <- preconditions <- main.
+  Called from red_alarms.i:80.
+[eva:alarm] red_alarms.i:80: Warning: 
+  function in_bound: precondition 'positive' got status unknown.
+[eva:alarm] red_alarms.i:80: Warning: 
+  function in_bound: precondition 'bounded' got status unknown.
+[eva] Recording results for in_bound
+[eva] Done for function in_bound
+[eva] computing for function in_bound <- preconditions <- main.
+  Called from red_alarms.i:82.
+[eva:alarm] red_alarms.i:82: Warning: 
+  function in_bound: precondition 'positive' got status invalid.
+[eva] red_alarms.i:82: 
+  function in_bound: no state left, precondition 'bounded' got status valid.
+[eva] Recording results for in_bound
+[eva] Done for function in_bound
+[eva] Recording results for preconditions
+[eva] Done for function preconditions
+[eva] computing for function user_assertions <- main.
+  Called from red_alarms.i:99.
+[eva:alarm] red_alarms.i:87: Warning: check 'indeterminate' got status unknown.
+[eva] red_alarms.i:89: check 'true' got status valid.
+[eva:alarm] red_alarms.i:90: Warning: check 'false' got status invalid.
+[eva:alarm] red_alarms.i:92: Warning: check 'maybe' got status unknown.
+[eva] Recording results for user_assertions
+[eva] Done for function user_assertions
+[eva] Recording results for main
+[eva] Done for function main
+[eva] red_alarms.i:45: assertion 'Eva,index_bound' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function in_bound:
+  y ∈ [0..99]
+[eva:final-states] Values at end of function maybe_swap:
+  a ∈ {1; 42}
+  b ∈ {42}
+  c ∈ {42}
+[eva:final-states] Values at end of function callstack:
+  a ∈ {1; 42}
+  b ∈ {42}
+  c ∈ {42}
+  p ∈ {{ NULL ; &a ; &uninit }}
+  q ∈ {{ NULL ; &b ; &uninit }}
+[eva:final-states] Values at end of function partitioning:
+  t[0..31] ∈ [0..31]
+  p ∈ {{ &t + [0..128],0%4 }}
+  i ∈ [0..32]
+  r ∈ [-100..100]
+[eva:final-states] Values at end of function preconditions:
+  
+[eva:final-states] Values at end of function user_assertions:
+  x ∈ [--..--]
+[eva:final-states] Values at end of function main:
+  
+[eva] Listing red statuses in file red_alarms.csv
+[from] Computing for function in_bound
+[from] Done for function in_bound
+[from] Computing for function maybe_swap
+[from] Done for function maybe_swap
+[from] Computing for function callstack
+[from] Done for function callstack
+[from] Computing for function partitioning
+[from] Done for function partitioning
+[from] Computing for function preconditions
+[from] Done for function preconditions
+[from] Computing for function user_assertions
+[from] Done for function user_assertions
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function in_bound:
+  NO EFFECTS
+[from] Function maybe_swap:
+  a FROM nondet; p; q; b; c; uninit (and SELF)
+  b FROM nondet; p; q; a; b; c; uninit (and SELF)
+  c FROM nondet; p; q; a; b; c; uninit (and SELF)
+[from] Function callstack:
+  NO EFFECTS
+[from] Function partitioning:
+  NO EFFECTS
+[from] Function preconditions:
+  NO EFFECTS
+[from] Function user_assertions:
+  NO EFFECTS
+[from] Function main:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function in_bound:
+    y
+[inout] Inputs for function in_bound:
+    \nothing
+[inout] Out (internal) for function maybe_swap:
+    v; a; b; c
+[inout] Inputs for function maybe_swap:
+    nondet; a; b; c; uninit
+[inout] Out (internal) for function callstack:
+    a; b; c; p; tmp; tmp_0; q; tmp_1; tmp_2
+[inout] Inputs for function callstack:
+    nondet
+[inout] Out (internal) for function partitioning:
+    t[0..31]; p; i; r
+[inout] Inputs for function partitioning:
+    nondet
+[inout] Out (internal) for function preconditions:
+    \nothing
+[inout] Inputs for function preconditions:
+    nondet
+[inout] Out (internal) for function user_assertions:
+    x
+[inout] Inputs for function user_assertions:
+    nondet
+[inout] Out (internal) for function main:
+    \nothing
+[inout] Inputs for function main:
+    nondet

tests/value/oracle_apron/red_alarms.csv

+directory	file	line	function	kind	name	#contexts	status	property
+.	red_alarms.i	90	user_assertions	Property	user check	1	Invalid or unreachable	x < 0
+.	red_alarms.i	67	partitioning	Alarm	division_by_zero	1	Unknown	(int)(i - 15) ≢ 0
+.	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
+.	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
+.	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
+.	red_alarms.i	70	in_bound	Property	precondition	1	Invalid or unreachable	positive: x ≥ 0

tests/value/oracle_bitwise/red_alarms.csv

+directory	file	line	function	kind	name	#contexts	status	property
+.	red_alarms.i	90	user_assertions	Property	user check	1	Invalid or unreachable	x < 0
+.	red_alarms.i	67	partitioning	Alarm	division_by_zero	1	Unknown	(int)(i - 15) ≢ 0
+.	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
+.	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
+.	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
+.	red_alarms.i	70	in_bound	Property	precondition	1	Invalid or unreachable	positive: x ≥ 0

tests/value/oracle_equality/red_alarms.csv

+directory	file	line	function	kind	name	#contexts	status	property
+.	red_alarms.i	90	user_assertions	Property	user check	1	Invalid or unreachable	x < 0
+.	red_alarms.i	67	partitioning	Alarm	division_by_zero	1	Unknown	(int)(i - 15) ≢ 0
+.	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
+.	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
+.	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
+.	red_alarms.i	70	in_bound	Property	precondition	1	Invalid or unreachable	positive: x ≥ 0

tests/value/oracle_gauges/red_alarms.csv

+directory	file	line	function	kind	name	#contexts	status	property
+.	red_alarms.i	90	user_assertions	Property	user check	1	Invalid or unreachable	x < 0
+.	red_alarms.i	67	partitioning	Alarm	division_by_zero	1	Unknown	(int)(i - 15) ≢ 0
+.	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
+.	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
+.	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
+.	red_alarms.i	70	in_bound	Property	precondition	1	Invalid or unreachable	positive: x ≥ 0

tests/value/oracle_gauges/red_alarms.res.oracle

+55d54
+< [eva:alarm] red_alarms.i:48: Warning: out of bounds write. assert \valid(p);

tests/value/oracle_multidim/red_alarms.csv

+directory	file	line	function	kind	name	#contexts	status	property
+.	red_alarms.i	90	user_assertions	Property	user check	1	Invalid or unreachable	x < 0
+.	red_alarms.i	67	partitioning	Alarm	division_by_zero	1	Unknown	(int)(i - 15) ≢ 0
+.	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
+.	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
+.	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
+.	red_alarms.i	70	in_bound	Property	precondition	1	Invalid or unreachable	positive: x ≥ 0

tests/value/oracle_octagon/red_alarms.csv

+directory	file	line	function	kind	name	#contexts	status	property
+.	red_alarms.i	90	user_assertions	Property	user check	1	Invalid or unreachable	x < 0
+.	red_alarms.i	67	partitioning	Alarm	division_by_zero	1	Unknown	(int)(i - 15) ≢ 0
+.	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
+.	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
+.	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
+.	red_alarms.i	70	in_bound	Property	precondition	1	Invalid or unreachable	positive: x ≥ 0

tests/value/oracle_symblocs/red_alarms.csv

+directory	file	line	function	kind	name	#contexts	status	property
+.	red_alarms.i	90	user_assertions	Property	user check	1	Invalid or unreachable	x < 0
+.	red_alarms.i	67	partitioning	Alarm	division_by_zero	1	Unknown	(int)(i - 15) ≢ 0
+.	red_alarms.i	45	partitioning	Alarm	index_bound	1	Invalid or unreachable	i < 32
+.	red_alarms.i	57	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	13	maybe_swap	Alarm	mem_access	1	Unknown	\valid_read(q)
+.	red_alarms.i	12	maybe_swap	Alarm	initialization	2	Unknown	\initialized(p)
+.	red_alarms.i	61	partitioning	Alarm	index_bound	1	Unknown	i < 32
+.	red_alarms.i	10	maybe_swap	Property	user check	1	Unknown	*p ≢ *q
+.	red_alarms.i	70	in_bound	Property	precondition	1	Invalid or unreachable	positive: x ≥ 0

tests/value/red_alarms.i

+/* run.config*
+   LOG: @PTEST_NAME@.csv
+   STDOPT: +"-eva-report-red-statuses ./@PTEST_NAME@.csv"
+*/
+
+volatile int nondet;
+
+void maybe_swap (int *p, int *q) {
+  //@ check p != q;
+  //@ check *p != *q;
+  if (nondet) {
+    int v = *p;
+    *p = *q;
+    *q = *p;
+  }
+}
+
+/* Red statuses depending on call contexts. */
+void callstack (void) {
+  int a = 1;
+  int b = 42;
+  int c = 42;
+  int uninit;
+  maybe_swap(&a, &b);
+  maybe_swap(&a, &b);
+  maybe_swap(&b, &c); // In [swap], the second assertion should be red.
+  maybe_swap(&uninit, &a); // In [swap], alarm \initialized(*p) should be red.
+  maybe_swap(&uninit, &b);
+  maybe_swap(&a, 0); // In [swap], alarm \valid_read(q) should be red.
+  int *p = nondet ? &a : (nondet ? &uninit : 0);
+  int *q = nondet ? &b : (nondet ? &uninit : 0);
+  maybe_swap(p, q); // This should not create other red alarms.
+}
+
+/* Red statuses depending on partitioning. */
+void partitioning (void) {
+  int t[32];
+  int *p = &t[0];
+  int i, r;
+  //@ loop unroll 32;
+  for (i = 0; i < 32; i++) {
+    t[i] = i; // No alarm.
+  }
+  if (nondet)
+    r = t[i]; // Invalid alarm: red status.
+  p = &t[0];
+  for (i = 0; i < 32; i++) {
+    *p = i; // False alarm — so no red status.
+    p++;
+  }
+  //@ loop unroll 0;
+  for (i = 0; i <= 32 && nondet; i++) {
+    t[i] = i; // True alarm, but no red status without partitioning.
+  }
+  //@ loop unroll 32;
+  for (i = 0; i <= 32 && nondet; i++) {
+    t[i] = i; // Alarm with a red status thanks to the loop unrolling.
+  }
+  //@ dynamic_split i == 32;
+  for (i = 0; i <= 32 && nondet; i++) {
+    t[i] = i; // Alarm with a red status thanks to the dynamic split.
+  }
+  if (i != 5)
+    r = 100 / (i - 5); // False alarm — so no red status.
+  r = 100 / (i - 10); // True alarm with no red status.
+  //@ split i;
+  r = 100 / (i - 15); // Alarm with red status thanks to the split.
+}
+
+/*@ requires positive: x >= 0;
+    requires bounded: x < 100;
+    assigns \nothing; */
+void in_bound (int x) {
+  int y = x;
+  return;
+}
+
+void preconditions (void) {
+  in_bound(42);
+  in_bound(nondet);
+  if (nondet)
+    in_bound(-1); // First precondition has red status.
+}
+
+void user_assertions (void) {
+  int x;
+  //@ check indeterminate: x > 0;
+  x = 1;
+  //@ check true: x > 0;
+  //@ check false: x < 0;
+  x = nondet;
+  //@ check maybe: x > 0;
+}
+
+void main (void) {
+  callstack();
+  partitioning();
+  preconditions();
+  user_assertions();
+}