CN: bugfix: conversion of bools in cLogicalFuns

rems-project · Aug 31, 2023 · 0c7bcf5 · 0c7bcf5
1 parent 3d97c28
commit 0c7bcf5
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/backend/cn/cLogicalFuns.ml b/backend/cn/cLogicalFuns.ml
@@ -194,7 +194,11 @@ let rec symb_exec_mu_pexpr var_map pexpr =
  | None -> fail {loc; msg = Generic (Pp.item "expr from C syntax: non-constant type"
  (IT.pp ct_it))}
  in
- do_wrapI loc ct x
+ begin match ct with
+ | Sctypes.Integer Sctypes.IntegerTypes.Bool ->
+ return (IT.ite_ (IT.eq_ (x, IT.int_ 0), IT.int_ 0, IT.int_ 1))
+ | _ -> do_wrapI loc ct x
+ end
  | M_PEwrapI (act, pe) ->
  let@ x = symb_exec_mu_pexpr var_map pe in
  do_wrapI loc act.ct x