Skip to content
Snippets Groups Projects
Commit 3c7b1e87 authored by Basile Desloges's avatar Basile Desloges
Browse files

[Eva] Handle logic coercion from singleton to set

parent f968fd06
No related branches found
No related tags found
No related merge requests found
......@@ -1162,10 +1162,13 @@ let rec eval_term ~alarm_mode env t =
ldeps = r.ldeps;
eover; eunder = under_from_over eover;
empty = r.empty }
| _ ->
| ltyp ->
if Logic_const.is_boolean_type ltyp
&& Logic_typing.is_integral_type t.term_type
then cast_to_bool r
else if Logic_utils.is_same_type ltyp t.term_type then
(* coercion from singleton to set *)
r
else
unsupported
(Format.asprintf "logic coercion %a -> %a@."
......
......@@ -129,8 +129,6 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:48:
function sigaction: precondition 'separation,separated_acts' got status valid.
[eva] FRAMAC_SHARE/libc/signal.h:248:
cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
[eva:garbled-mix:assigns] signal_h.c:48:
The specification of function sigaction
has generated a garbled mix of addresses for assigns clause *oldact.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment