Merge branch 'fix/eva/high-priority-precondition' into 'master'

[Eva] Fixes high priority / red status on preconditions.

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

src/plugins/eva/utils/red_statuses.ml

@@ -91,17 +91,13 @@ let add_red_ap kinstr ap =
 
 let add_red_alarm ki a = add_red_ap ki (Alarm a)
 
-let add_red_property ki ip =
-  if false then
-    add_red_ap ki (Prop ip)
-  else
-    (* Collapses preconditions-at-callsites into the precondition itself,
-       by modifying the callstack. Results in a better display *)
-    let open Property in
-    match ip with
-    | IPPropertyInstance {ii_ip=IPPredicate {ip_kind=PKRequires _} as ip'} ->
-      add_red_ap Kglobal (Prop ip')
-    | _ -> add_red_ap ki (Prop ip)
+let add_red_property ki (ip: Property.identified_property) =
+  add_red_ap ki (Prop ip);
+  (* If [ip] is an instance of a precondition [ip'], also add [ip'] itself. *)
+  match ip with
+  | IPPropertyInstance {ii_ip = IPPredicate {ip_kind = PKRequires _} as ip'} ->
+    add_red_ap Kglobal (Prop ip')
+  | _ -> ()
 
 let is_red ip =
   let kinstr = Property.get_kinstr ip in

tests/value/oracle/red_alarms.csv

@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	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	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	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

tests/value/oracle_apron/red_alarms.csv

@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	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	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	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

tests/value/oracle_bitwise/red_alarms.csv

@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	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	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	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

tests/value/oracle_equality/red_alarms.csv

@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	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	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	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

tests/value/oracle_gauges/red_alarms.csv

@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	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	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	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

tests/value/oracle_multidim/red_alarms.csv

@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	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	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	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

tests/value/oracle_octagon/red_alarms.csv

@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	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	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	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

tests/value/oracle_symblocs/red_alarms.csv

@@ -4,6 +4,7 @@ directory	file	line	function	kind	name	#contexts	status	property
 .	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	82	preconditions	Property	precondition of in_bound	1	Invalid or unreachable	positive: x ≥ 0
 .	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