diff --git a/Changelog b/Changelog
index bad19ae33373814899a64110da3d758235cedaa3..032638655591d1acf520615275efbd6427fa30fb 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,7 @@
Open Source Release <next-release>
###############################################################################
+o! Kernel [2024-10-08] introduce logic type Lboolean and constants
- Kernel [2024-10-08] Asm contracts can now have \initialized ensures.
See option -asm-contracts-ensure-init
- Kernel [2024-10-08] Option for converting stmt contracts into
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 01d7509c06f6d75a7962b12a604c1143980ea032..0f6962782bb6c79f9826c286a8854241a31b69a8 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -872,7 +872,7 @@ tabs:
type_spec(tname):
| INTEGER { LTinteger }
| REAL { LTreal }
-| BOOLEAN { LTnamed (Utf8_logic.boolean,[]) }
+| BOOLEAN { LTboolean }
| VOID { LTvoid }
| BOOL { LTint IBool }
| CHAR { LTint IChar } /** [char] */
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index bf6365d482160ef3b8c0a7e327339f2f1f251cd5..6ca4bb04ff2e040ada195bd7831da60332a784f7 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -53,9 +53,6 @@ let init =
(*
let tvar v = new_identified_term (tvar v) in
*)
- let boolean =
- { lt_name=Utf8_logic.boolean; lt_params=[]; lt_def=None; lt_attr=[] }
- in
let set =
{ lt_name = "set"; lt_params=["elem"]; lt_def=None; lt_attr=[] }
in
@@ -72,7 +69,7 @@ let init =
{lt_name = "rounding_mode"; lt_params = []; lt_def = None; lt_attr=[]}
in
List.iter (fun x -> Logic_env.add_builtin_logic_type x.lt_name x)
- [ boolean; set; typetag; sign; float_format; rounding_mode ];
+ [ set; typetag; sign; float_format; rounding_mode ];
(* constructors *)
List.iter
(fun (typename, constrs) ->
@@ -88,15 +85,13 @@ let init =
constrs
in
typename.lt_def <- Some (LTsum l))
- [ boolean, ["\\true"; "\\false"];
- sign , [ "\\Positive"; "\\Negative"] ;
+ [ sign , [ "\\Positive"; "\\Negative"] ;
float_format, [ "\\Single"; "\\Double"; "\\Quad" ] ;
rounding_mode, [ "\\Up"; "\\Down"; "\\ToZero"; "\\NearestAway";
"\\NearestEven" ];
];
(* logic types used by the builtins *)
let a_name, a_type = polymorphic_type "a" in
- let boolean = Ltype(boolean,[]) in
let sign = Ltype(sign,[]) in
let float_format = Ltype(float_format,[]) in
let rounding_mode = Ltype(rounding_mode,[]) in
@@ -255,7 +250,7 @@ let init =
"f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\numof", [], ["min",Linteger;
"max", Linteger;
- "f",(Larrow ([Linteger],boolean))], Linteger ;
+ "f",(Larrow ([Linteger],Lboolean))], Linteger ;
(* for floats special values *)
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 73e7cc4ab67e78b6eb11eea45262069a2b113aae..d9ef2e8af3dbe3d4647d98a37ef8194e996c5508 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -1834,7 +1834,7 @@ let pp_profiles fmt li =
let logic_info_of_logic_var lv =
let rec extract_tparams tparams = function
- | Ctype _ | Linteger | Lreal -> tparams
+ | Ctype _ | Linteger | Lreal | Lboolean -> tparams
| Ltype (_,l) -> List.fold_left extract_tparams tparams l
| Lvar s -> Datatype.String.Set.add s tparams
| Larrow (l,t) ->
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 3c0114a58533f3b45b7a984e8b074a9ac779c6e0..9f8f661f037cec928cc29ad8791e4cc0f7bebf63 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1334,6 +1334,7 @@ and location = Filepath.position * Filepath.position
(** {1 Abstract syntax trees for annotations} *)
and logic_constant =
+ | Boolean of bool
| Integer of Integer.t * string option
(** Integer constant with a textual representation. *)
| LStr of string (** String constant. *)
@@ -1356,6 +1357,7 @@ and logic_type =
| Ltype of logic_type_info * logic_type list
(** an user-defined logic type with its parameters *)
| Lvar of string (** a type variable. *)
+ | Lboolean (** booleans *)
| Linteger (** mathematical integers, {i i.e.} Z *)
| Lreal (** mathematical reals, {i i.e.} R *)
| Larrow of logic_type list * logic_type (** (n-ary) function type *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index fc7d05c72804a2d36f0dbf0c858ef8de51dd3097..c018fc00b8bbc864177b46e20ed6d725d8bef91c 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2358,6 +2358,8 @@ class cil_printer () = object (self)
(* ******************************************************************* *)
method logic_constant fmt = function
+ | Boolean true -> self#pp_acsl_keyword fmt "\\true"
+ | Boolean false -> self#pp_acsl_keyword fmt "\\false"
| Integer(_, Some s) when print_as_source s ->
fprintf fmt "%s" s (* Always print the text if there is one, unless
we want to print it as hexa *)
@@ -2389,6 +2391,11 @@ class cil_printer () = object (self)
in
function
| Ctype typ -> self#typ name fmt typ
+ | Lboolean ->
+ let res =
+ if Kernel.Unicode.get () then Utf8_logic.boolean else "boolean"
+ in
+ Format.fprintf fmt "%s%t" res pname
| Linteger ->
let res =
if Kernel.Unicode.get () then Utf8_logic.integer else "integer"
@@ -2399,11 +2406,6 @@ class cil_printer () = object (self)
if Kernel.Unicode.get () then Utf8_logic.real else "real"
in
Format.fprintf fmt "%s%t" res pname
- | Ltype ({ lt_name = name},[]) when name = Utf8_logic.boolean ->
- let res =
- if Kernel.Unicode.get () then Utf8_logic.boolean else "boolean"
- in
- Format.fprintf fmt "%s%t" res pname
| Ltype (s,l) ->
fprintf fmt "%a%a%t" self#logic_type_info s
((* the space avoids the issue of list<list<int>> where the double >
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 4a1ae03abc0409845ad9d794b96efe4fc24b9f85..42fa14470042a00252b7a68dcb34e978d891cb62 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -596,6 +596,8 @@ and pp_if_loc_known prefix suffix fmt loc =
else ()
and pp_logic_constant fmt = function
+ | Boolean b ->
+ Format.fprintf fmt "Boolean(%B)" b
| Integer(integer,string_option) ->
Format.fprintf fmt "Integer(%a,%a)" pp_integer integer (pp_option pp_string) string_option
| LStr(string) -> Format.fprintf fmt "LStr(%a)" pp_string string
@@ -616,6 +618,7 @@ and pp_logic_type fmt = function
| Ltype(logic_type_info,logic_type_list) ->
Format.fprintf fmt "Ltype(%a,%a)" pp_logic_type_info logic_type_info (pp_list pp_logic_type) logic_type_list
| Lvar(string) -> Format.fprintf fmt "Lvar(%a)" pp_string string
+ | Lboolean -> Format.fprintf fmt "Lboolean"
| Linteger -> Format.fprintf fmt "Linteger"
| Lreal -> Format.fprintf fmt "Lreal"
| Larrow(logic_type_list,logic_type) ->
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 91bbf80e966b1defd19735cf112733140c021122..0c27e9c2ffd78fe1342086291d75fa66b6dc50d5 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -49,6 +49,10 @@ let rec print_logic_type name fmt typ =
in
print_logic_type (Some pname) fmt t
| LTvoid -> fprintf fmt "void%t" pname
+ | LTboolean ->
+ fprintf fmt "%s%t"
+ (if Kernel.Unicode.get () then Utf8_logic.boolean else "boolean")
+ pname
| LTinteger ->
fprintf fmt "%s%t"
(if Kernel.Unicode.get () then Utf8_logic.integer else "integer")
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index d82c70ccfe7300dc85d897a1f3f695b63b77c876..2b92a40cc21072e33bb363188d14f88d90620172 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -545,7 +545,7 @@ and is_same_logic_constant c c' env =
| `Same ei'' -> Cil_datatype.Enumitem.equal ei' ei''
| `Not_present -> false)
| LEnum _, _ | _, LEnum _ -> false
- | (Integer _ | LStr _ | LWStr _ | LChr _ | LReal _), _ ->
+ | (Boolean _ | Integer _ | LStr _ | LWStr _ | LChr _ | LReal _), _ ->
Cil_datatype.Logic_constant.equal c c'
and is_same_term t t' env =
@@ -763,12 +763,14 @@ and is_same_logic_type t t' env =
is_matching_logic_type_info t t' env &&
is_same_list is_same_logic_type prms prms' env
| Lvar s, Lvar s' -> is_matching_logic_type_var s s' env
+ | Lboolean, Lboolean -> true
| Linteger, Linteger -> true
| Lreal, Lreal -> true
| Larrow(args,rt), Larrow(args', rt') ->
is_same_list is_same_logic_type args args' env &&
is_same_logic_type rt rt' env
- | (Ctype _ | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _),_ -> false
+ | (Ctype _ | Ltype _ | Lvar _ | Linteger | Lboolean | Lreal | Larrow _),_ ->
+ false
and is_same_inductive_case (_,labs,tprms,p) (_,labs',tprms',p') env =
let res, env =
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index c9bbec26a5ed4b8928e81fd5983d43aec41f70d3..4a175d3957548c18a985bf514fb8e6aa75c12a3c 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -75,7 +75,7 @@ let is_non_null_expr e =
let is_integral_logic_const = function
| Integer _ | LEnum _ | LChr _ -> true
- | LStr _ | LWStr _ | LReal _ -> false
+ | LStr _ | LWStr _ | LReal _ | Boolean _ -> false
let possible_value_of_integral_logic_const = function
| Integer(i,_) -> Some i
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index f67e99e886011622d09f9db98c0e3b4b27d0bc69..d0ae997cb8a69a18b72a22113e9c7577ecd8353a 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1508,7 +1508,7 @@ and childrenLogicType vis ty =
Ctype t ->
let t' = visitCilType vis t in
if t != t' then Ctype t' else ty
- | Linteger | Lreal -> ty
+ | Lboolean | Linteger | Lreal -> ty
| Ltype (s,l) ->
let s' = doVisitCil vis (Visitor_behavior.Get.logic_type_info vis#behavior)
vis#vlogic_type_info_use alphabetabeta s in
@@ -3276,9 +3276,8 @@ let isIntegralOrPointerType t =
let rec isLogicBooleanType t =
match t with
| Ctype ty -> isIntegralType ty
- | Linteger -> true
- | Ltype ({lt_name = name} as tdef,_) ->
- name = Utf8_logic.boolean ||
+ | Lboolean | Linteger -> true
+ | Ltype (tdef,_) ->
( is_unrollable_ltdef tdef && isLogicBooleanType (unroll_ltdef t))
| Lreal | Lvar _ | Larrow _ -> false
@@ -3289,14 +3288,15 @@ let isBoolType typ = match unrollType typ with
let rec isLogicPureBooleanType t =
match t with
| Ctype t -> isBoolType t
- | Ltype ({lt_name = name} as def,_) ->
- name = Utf8_logic.boolean ||
+ | Lboolean -> true
+ | Ltype (def,_) ->
(is_unrollable_ltdef def && isLogicPureBooleanType (unroll_ltdef t))
| _ -> false
let rec isLogicIntegralType t =
match t with
| Ctype t -> isIntegralType t
+ | Lboolean -> false
| Linteger -> true
| Lreal -> false
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
@@ -3311,6 +3311,7 @@ let isFloatingType t =
let isLogicFloatType t =
match t with
| Ctype t -> isFloatingType t
+ | Lboolean -> false
| Linteger -> false
| Lreal -> false
| Lvar _ | Ltype _ | Larrow _ -> false
@@ -3318,6 +3319,7 @@ let isLogicFloatType t =
let rec isLogicRealOrFloatType t =
match t with
| Ctype t -> isFloatingType t
+ | Lboolean -> false
| Linteger -> false
| Lreal -> true
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
@@ -3327,6 +3329,7 @@ let rec isLogicRealOrFloatType t =
let rec isLogicRealType t =
match t with
| Ctype _ -> false
+ | Lboolean -> false
| Linteger -> false
| Lreal -> true
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
@@ -3350,7 +3353,7 @@ let rec isLogicArithmeticType t =
| Linteger | Lreal -> true
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
isLogicArithmeticType (unroll_ltdef ty)
- | Lvar _ | Ltype _ | Larrow _ -> false
+ | Lboolean | Lvar _ | Ltype _ | Larrow _ -> false
let isFunctionType t =
match unrollTypeSkel t with
@@ -3541,7 +3544,7 @@ let rec typeOfTermLval = function
Kernel.fatal ~current:true
"typeOfTermLval: Mem on a non-pointer"
end
- | Linteger | Lreal ->
+ | Lboolean | Linteger | Lreal ->
Kernel.fatal ~current:true "typeOfTermLval: Mem on a logic type"
| Ltype (s,_) as ty when is_unrollable_ltdef s ->
type_of_pointed (unroll_ltdef ty)
@@ -3565,7 +3568,7 @@ and typeTermOffset basetyp =
let rec putAttributes = function
| Ctype typ ->
Ctype (typeAddAttributes contagious typ)
- | Linteger | Lreal ->
+ | Lboolean | Linteger | Lreal ->
Kernel.fatal ~current:true
"typeTermOffset: Attribute on a logic type"
| Ltype (s,_) as ty when is_unrollable_ltdef s ->
@@ -3596,7 +3599,8 @@ and typeTermOffset basetyp =
Kernel.fatal ~current:true
"typeTermOffset: Index on a non-array"
end
- | Linteger | Lreal -> Kernel.fatal ~current:true "typeTermOffset: Index on a logic type"
+ | Lboolean | Linteger | Lreal ->
+ Kernel.fatal ~current:true "typeTermOffset: Index on a logic type"
| Ltype (s,_) as ty when is_unrollable_ltdef s ->
elt_type (unroll_ltdef ty)
| Ltype (s,_) ->
@@ -3617,7 +3621,8 @@ and typeTermOffset basetyp =
blendAttributes baseAttrs fieldType
| _ -> Kernel.fatal ~current:true "typeTermOffset: Field on a non-compound"
end
- | Linteger | Lreal -> Kernel.fatal ~current:true "typeTermOffset: Field on a logic type"
+ | Lboolean | Linteger | Lreal ->
+ Kernel.fatal ~current:true "typeTermOffset: Field on a logic type"
| Ltype (s,_) as ty when is_unrollable_ltdef s ->
elt_type (unroll_ltdef ty)
| Ltype (s,_) ->
@@ -3640,7 +3645,7 @@ let isVolatileType typ_lval = typeHasAttributeMemoryBlock "volatile" typ_lval
let rec isVolatileLogicType = function
| Ctype typ -> isVolatileType typ
- | Linteger | Lreal | Lvar _ | Larrow _ -> false
+ | Lboolean | Linteger | Lreal | Lvar _ | Larrow _ -> false
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
isVolatileLogicType (unroll_ltdef ty)
| Ltype _ -> false
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index 20033aed2b0d8163ee290341ce9999f11a086dab..019ba5281b355651fc34a1e369254b592f68b9c1 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -47,6 +47,7 @@ open Cil_types
(* Types *)
let voidType = TVoid([])
+let boolType = TInt(IBool,[])
let intType = TInt(IInt,[])
let uintType = TInt(IUInt,[])
let shortType = TInt(IShort, [])
@@ -192,4 +193,3 @@ let make_logic_type name = {
lt_def = None ;
lt_attr = [] ;
}
-
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index 1c3c1cf27bacc1952bc76db8f87a4b71cdede787..e08071f1b3c93e67fdb8562ac0e3c1615d1d4641 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -48,6 +48,10 @@ open Cil_types
(** void *)
val voidType: typ
+(** bool
+ @since Frama-C+dev *)
+val boolType: typ
+
(** int
@since Frama-C+dev *)
val intType: typ
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 4ab4e41617b53d0a053fc0ce373f21f436e2449e..65c8fe4fdb064a6164a459542b3b91f0267d9f5b 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1405,12 +1405,13 @@ end
let rec compare_logic_type config v1 v2 =
let rank = function
- | Linteger -> 0
- | Lreal -> 1
- | Ctype _ -> 2
- | Lvar _ -> 3
- | Ltype _ -> 4
- | Larrow _ -> 5
+ | Lboolean -> 0
+ | Linteger -> 1
+ | Lreal -> 2
+ | Ctype _ -> 3
+ | Lvar _ -> 4
+ | Ltype _ -> 5
+ | Larrow _ -> 6
in
let v1 = if config.unroll then !punrollLogicType v1 else v1 in
let v2 = if config.unroll then !punrollLogicType v2 else v2 in
@@ -1426,6 +1427,7 @@ let rec compare_logic_type config v1 v2 =
if c <> 0 then c
else compare_list (compare_logic_type config) ts1 ts2
| Lvar x1, Lvar x2 -> Datatype.String.compare x1 x2
+ | Lboolean, Lboolean -> 0
| Linteger, Linteger -> 0
| Lreal, Lreal -> 0
| Larrow(l1, t1), Larrow(l2, t2) ->
@@ -1434,8 +1436,9 @@ let rec compare_logic_type config v1 v2 =
| _ -> assert false
let rec hash_logic_type config = function
- | Linteger -> 0
- | Lreal -> 1
+ | Lboolean -> 0
+ | Linteger -> 1
+ | Lreal -> 2
| Ctype ty -> hash_type config ty
| Ltype({ lt_def = Some (LTsyn t)},_) when config.unroll ->
hash_logic_type config t
@@ -1593,19 +1596,21 @@ let compare_logic_real r1 r2 =
String.compare r1.r_literal r2.r_literal
let compare_logic_constant c1 c2 = match c1,c2 with
+ | Boolean b1, Boolean b2 -> compare b1 b2
| Integer (i1,_), Integer(i2,_) -> Integer.compare i1 i2
| LStr s1, LStr s2 -> Datatype.String.compare s1 s2
| LWStr s1, LWStr s2 -> compare_list Datatype.Int64.compare s1 s2
| LChr c1, LChr c2 -> Datatype.Char.compare c1 c2
| LReal r1, LReal r2 -> compare_logic_real r1 r2
| LEnum e1, LEnum e2 -> Enumitem.compare e1 e2
+ | Boolean _,(Integer _ | LStr _|LWStr _ |LChr _|LReal _|LEnum _) -> 1
| Integer _,(LStr _|LWStr _ |LChr _|LReal _|LEnum _) -> 1
| LStr _ ,(LWStr _ |LChr _|LReal _|LEnum _) -> 1
| LWStr _ ,(LChr _|LReal _|LEnum _) -> 1
| LChr _,(LReal _|LEnum _) -> 1
| LReal _,LEnum _ -> 1
- | (LStr _|LWStr _ |LChr _|LReal _|LEnum _),
- (Integer _|LStr _|LWStr _ |LChr _|LReal _) -> -1
+ | (Integer _ |LStr _|LWStr _ |LChr _|LReal _|LEnum _),
+ (Boolean _ |Integer _|LStr _|LWStr _ |LChr _|LReal _) -> -1
let rec compare_term t1 t2 =
let r1 = rank_term t1.term_node in
@@ -1813,6 +1818,7 @@ let hash_logic_constant = function
| LStr s -> Datatype.String.hash s
| LWStr l -> hash_list Datatype.Int64.hash l
| LChr c -> Datatype.Char.hash c
+ | Boolean b -> Datatype.Bool.hash b
| Integer(n, _) -> Integer.hash n
| LReal r ->
if is_exact_float r then Datatype.Float.hash r.r_lower
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 91f440b76c33bc75741e383ad78c2e3e3e5b25ce..8452b091dd8aabc50fdee5e26a46b88c73891b47 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -149,7 +149,7 @@ let rec instantiate subst = function
(* This is an application of type parameters:
no need to recursively substitute in the resulting type. *)
(try List.assoc v subst with Not_found -> ty)
- | Ctype _ | Linteger | Lreal as ty -> ty
+ | Ctype _ | Linteger | Lreal | Lboolean as ty -> ty
let is_unrollable_ltdef = function
| {lt_def=Some (LTsyn _)} -> true
@@ -166,12 +166,12 @@ let rec unroll_ltdef = function
unroll_ltdef (instantiate subst ty)
| Ltype ({lt_def= None},_)
| Ltype ({lt_def= Some (LTsum _)},_)
- | Linteger | Lreal | Lvar _ | Larrow _ | Ctype _ as ty -> ty
+ | Linteger | Lboolean | Lreal | Lvar _ | Larrow _ | Ctype _ as ty -> ty
let rec isLogicCType f = function
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
isLogicCType f (unroll_ltdef ty)
- | Ltype _ | Linteger | Lreal | Lvar _ | Larrow _ -> false
+ | Ltype _ | Linteger | Lboolean | Lreal | Lvar _ | Larrow _ -> false
| Ctype cty -> f cty
let rec is_list_type = function
@@ -238,13 +238,11 @@ let make_arrow_type args rt =
| _ -> Larrow(List.map (fun x -> x.lv_type) args, rt)
let rec is_boolean_type = function
- | Ltype ({ lt_name = s }, []) when s = Utf8_logic.boolean -> true
+ | Lboolean -> true
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
is_boolean_type (unroll_ltdef ty)
| _ -> false
-let boolean_type = Ltype ({ lt_name = Utf8_logic.boolean ; lt_params = [] ; lt_def = None; lt_attr = [] } , [])
-
(** {2 Offsets} *)
let rec lastTermOffset (off: term_offset) : term_offset =
@@ -279,6 +277,9 @@ let trange ?(loc=Cil_datatype.Location.unknown) (low,high) =
term ~loc (Trange(low,high))
(Ltype(Logic_env.find_logic_type "set",[Linteger]))
+let tboolean ?(loc=Cil_datatype.Location.unknown) b =
+ term ~loc (TConst (Boolean b)) Lboolean
+
(** An integer constant (of type integer). *)
let tinteger ?(loc=Cil_datatype.Location.unknown) i =
term ~loc (TConst (Integer (Integer.of_int i,None))) Linteger
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index bf69aa11aca30c3702f2d35c3b6154f7ade35f01..d5b6b3e495976d6eefd085fa85a3d83d4d9fe358 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -289,9 +289,6 @@ val make_arrow_type: logic_var list -> logic_type -> logic_type
(** @return true if the argument is the boolean type. *)
val is_boolean_type: logic_type -> bool
-(** @since Sodium-20150201 *)
-val boolean_type: logic_type
-
(* ************************************************************************** *)
(** {1 Logic Terms} *)
(* ************************************************************************** *)
@@ -302,6 +299,11 @@ val term : ?loc:Location.t -> term_node -> logic_type -> term
(** [..] of integers *)
val trange: ?loc:Location.t -> term option * term option -> term
+(** boolean constant
+ @since Frama-C+dev
+*)
+val tboolean: ?loc:Location.t -> bool -> term
+
(** integer constant *)
val tinteger: ?loc:Location.t -> int -> term
diff --git a/src/kernel_services/ast_queries/logic_to_c.ml b/src/kernel_services/ast_queries/logic_to_c.ml
index 3fe95d67f7c3f97bb231f1d5e141f2b12c38ed8b..e2ceb635f678a35241acdc7fce0820ce3b8deb69 100644
--- a/src/kernel_services/ast_queries/logic_to_c.ml
+++ b/src/kernel_services/ast_queries/logic_to_c.ml
@@ -32,8 +32,7 @@ let rec logic_type_to_typ = function
| Linteger -> TInt(ILongLong,[]) (*TODO: to have an unlimited integer type
in the logic interpretation*)
| Lreal -> TFloat(FDouble,[]) (* TODO: handle reals, not floats... *)
- | Ltype({lt_name = name},[]) when name = Utf8_logic.boolean ->
- TInt(ILongLong,[])
+ | Lboolean -> TInt(ILongLong,[])
| Ltype({lt_name = "set"},[t]) -> logic_type_to_typ t
| Ltype _ | Lvar _ | Larrow _ -> error_lval ()
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 69cb0cb35c6ff584a0287e04eea2b79cdf7a8f68..7fb43878542d6eb4ecb59bb9537e98ae92e31cf1 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1014,7 +1014,7 @@ struct
| Ctype t -> t
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
c_type_of loc (unroll_ltdef ty)
- | Ltype _ | Linteger | Lreal | Lvar _ | Larrow _ ->
+ | Ltype _ | Lboolean | Linteger | Lreal | Lvar _ | Larrow _ ->
C.error loc "not a C type"
let parseInt loc s =
@@ -1136,6 +1136,7 @@ struct
| None -> ctxt.error loc "no such type %s" id
end
+ | LTboolean -> Lboolean
| LTinteger -> Linteger
| LTreal -> Lreal
| LTattribute (ty,attr) ->
@@ -1413,15 +1414,16 @@ struct
with
| Ctype oldt, Ctype newt ->
c_mk_cast ~force e oldt newt
- | t1, Ltype ({lt_name = name},[])
- when name = Utf8_logic.boolean && is_integral_type t1 ->
- let t2 = Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[]) in
+ | t1, Lboolean when is_integral_type t1 ->
let e = mk_cast e Linteger in
- Logic_const.term ~loc (TBinOp(Ne,e,lzero ~loc())) t2
- | t1, Linteger when Logic_const.is_boolean_type t1 && explicit ->
+ Logic_const.term ~loc (TBinOp(Ne,e,lzero ~loc())) Lboolean
+ | Lboolean, Linteger when explicit ->
logic_coerce Linteger e
- | t1, Ctype t2 when Logic_const.is_boolean_type t1
- && is_integral_type newt && explicit ->
+ | Lboolean, (Linteger|Lreal) ->
+ C.error loc "invalid implicit cast from %a to %a"
+ Cil_printer.pp_logic_type e.term_type
+ Cil_printer.pp_logic_type newt
+ | Lboolean, Ctype t2 when is_integral_type newt && explicit ->
Logic_const.term ~loc (TCast (false, Ctype t2,e)) newt
| ty1, Ltype({lt_name="set"},[ty2])
when is_pointer_type ty1 &&
@@ -1438,14 +1440,14 @@ struct
| _ , Ltype({lt_name = "set"},[ ty2 ]) ->
let e = mk_cast e ty2 in
logic_coerce (make_set_type e.term_type) e
- | Linteger, Linteger | Lreal, Lreal -> e
+ | Lboolean, Lboolean | Linteger, Linteger | Lreal, Lreal -> e
| Linteger, Ctype t when isLogicPointerType newt && isLogicNull e ->
c_mk_cast ~force e Cil_const.intType t
| Linteger, (Ctype newt) | Lreal, (Ctype newt) when explicit ->
Logic_utils.mk_cast ~loc newt e
| Linteger, Ctype t when isIntegralType t ->
(try C.integral_cast t e with Failure s -> C.error loc "%s" s)
- | Linteger, Ctype _ | Lreal, Ctype _ ->
+ | Linteger, Ctype _ | Lreal, Ctype _ | Lboolean, Ctype _ ->
C.error loc "invalid implicit cast from %a to C type %a"
Cil_printer.pp_logic_type e.term_type
Cil_printer.pp_logic_type newt
@@ -1454,7 +1456,7 @@ struct
Logic_const.term
~loc (Tapp(truncate_info,[], [logic_coerce Lreal e])) Linteger
| Ctype t, Lreal when isArithmeticType t -> logic_coerce Lreal e
- | Ctype _, (Lreal | Linteger) ->
+ | Ctype _, (Lreal | Linteger | Lboolean) ->
C.error loc "invalid implicit cast from %a to logic type %a"
Cil_printer.pp_logic_type e.term_type
Cil_printer.pp_logic_type newt
@@ -1466,6 +1468,10 @@ struct
C.error loc
"invalid cast from real to integer. \
Use conversion functions instead"
+ | (Linteger | Lreal), Lboolean ->
+ C.error loc
+ "invalid cast arithmetic logic type to boolean. \
+ Use conversion functions instead"
| Larrow (args1,_), Larrow(args2,rt2) ->
(match e.term_node with
| Tlambda (prms,body) when
@@ -1561,6 +1567,7 @@ struct
else
C.error loc "invalid implicit conversion from '%a' to '%a'"
Cil_printer.pp_typ ty1 Cil_printer.pp_typ ty2
+ | Ctype ty, Lboolean when Cil.isBoolType ty -> Lboolean, oterm
| Ctype ty, Linteger when Cil.isIntegralType ty -> Linteger, oterm
| Ctype ty, Lreal when Cil.isArithmeticType ty -> Lreal, oterm
| Linteger, Lreal -> Lreal, oterm
@@ -1600,7 +1607,7 @@ struct
else term
in
stype, term
- | Linteger, Linteger | Lreal, Lreal -> ot, oterm
+ | Lboolean, Lboolean | Linteger, Linteger | Lreal, Lreal -> ot, oterm
| Lvar s1, Lvar s2 when s1 = s2 -> ot, oterm
| Larrow(args1,rt1), Larrow(args2,rt2)
when List.length args1 = List.length args2 ->
@@ -1613,8 +1620,8 @@ struct
in
let rt,_ = implicit_conversion ~overloaded loc oterm rt1 rt2 in
Larrow(args,rt), oterm
- | ((Ctype _| Linteger | Lreal | Ltype _ | Lvar _ | Larrow _),
- (Ctype _| Linteger | Lreal | Ltype _ | Lvar _ | Larrow _)) ->
+ | ((Ctype _| Lboolean | Linteger | Lreal | Ltype _ | Lvar _ | Larrow _),
+ (Ctype _| Lboolean | Linteger | Lreal | Ltype _ | Lvar _ | Larrow _)) ->
if overloaded then raise Not_applicable
else
C.error loc "invalid implicit conversion from %a to %a"
@@ -1632,13 +1639,9 @@ struct
else
C.error loc "incompatible types %a and %a@."
Cil_printer.pp_typ ot Cil_printer.pp_typ nt
- | Ctype ot, (Ltype({lt_name = n},[]) as nt) when
- n = Utf8_logic.boolean && Cil.isIntegralType ot -> nt
- | Ltype({lt_name = n},[]) as ot, Ctype nt when
- n = Utf8_logic.boolean && Cil.isIntegralType nt -> ot
- | (Linteger, (Ltype({lt_name = n},[]) as t)
- | (Ltype({lt_name = n},[]) as t), Linteger)
- when n = Utf8_logic.boolean -> t
+ | Ctype ot, (Lboolean as nt) when Cil.isIntegralType ot -> nt
+ | Lboolean as ot, Ctype nt when Cil.isIntegralType nt -> ot
+ | (Linteger, (Lboolean as t) | (Lboolean as t), Linteger) -> t
| Ltype(ot,oprms), Ltype(nt,nprms) when ot == nt ->
let res =
List.map2 (find_supertype ~overloaded loc t) oprms nprms
@@ -1659,6 +1662,7 @@ struct
| Ctype ot, Linteger when Cil.isIntegralType ot -> Linteger
| Ctype ot, Linteger when Cil.isPointerType ot && isLogicNull t ->
Ctype ot
+ | Lboolean, Lboolean -> Lboolean
| Linteger, Linteger -> Linteger
| Linteger, Lreal -> Lreal
| Linteger, Ctype nt when Cil.isArithmeticType nt -> Lreal
@@ -1672,7 +1676,7 @@ struct
let ret = find_supertype ~overloaded loc t oret nret in
let args = List.map2 (find_supertype ~overloaded loc t) nargs oargs in
Larrow(args,ret)
- | (Ctype _ | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _), _ ->
+ | (Ctype _ | Ltype _ | Lvar _ | Lboolean | Linteger | Lreal | Larrow _), _ ->
if overloaded then raise Not_applicable
else
C.error loc "incompatible types %a and %a"
@@ -1768,8 +1772,8 @@ struct
env, make_set_type ot, make_set_type nt
| t1,t2 when plain_boolean_type t1 && plain_boolean_type t2 ->
env,ot,nt
- | ((Ctype _ | Linteger | Lreal | Ltype ({lt_name = "boolean"},[])),
- (Ctype _ | Linteger | Lreal | Ltype ({ lt_name = "boolean"},[]))) ->
+ | ((Ctype _ | Linteger | Lreal | Lboolean),
+ (Ctype _ | Linteger | Lreal | Lboolean)) ->
env,ot,nt
| (Ltype _|Larrow _|Lvar _), _ | _, (Larrow _| Ltype _|Lvar _) ->
if overloaded then raise Not_applicable
@@ -1857,18 +1861,17 @@ struct
Cil_printer.pp_logic_type t)
| Ltype ({lt_name="set"} as lt,[t]) ->
Ltype(lt,[logic_arithmetic_promotion t])
- | Ltype _ | Lvar _ | Larrow _ ->
+ | Lboolean | Ltype _ | Lvar _ | Larrow _ ->
Kernel.fatal ~current:true
"logic arithmetic promotion on non-arithmetic type %a"
Cil_printer.pp_logic_type t
let rec integral_promotion t =
match unroll_type t with
- | Ctype ty when isIntegralType ty ->
- Linteger
+ | Ctype ty when isIntegralType ty -> Linteger
| Linteger -> Linteger
| Ltype ({lt_name="set"} as lt,[t]) -> Ltype(lt,[integral_promotion t])
- | Ltype _ | Lreal | Lvar _ | Larrow _ | Ctype _ ->
+ | Lboolean | Ltype _ | Lreal | Lvar _ | Larrow _ | Ctype _ ->
Kernel.fatal ~current:true
"logic integral promotion on non-integral type %a"
Cil_printer.pp_logic_type t
@@ -1968,12 +1971,8 @@ struct
when Cil.isArithmeticType t -> Lreal
(* In ACSL, you can convert implicitely from integral to boolean =>
prefer boolean as common type when doing comparison. *)
- | Ltype({lt_name = name},[]), t
- when is_integral_type t && name = Utf8_logic.boolean ->
- Ltype(Logic_env.find_logic_type Utf8_logic.boolean,[])
- | t, Ltype({lt_name = name},[])
- when is_integral_type t && name = Utf8_logic.boolean ->
- Ltype(Logic_env.find_logic_type Utf8_logic.boolean,[])
+ | Lboolean, t when is_integral_type t -> Lboolean
+ | t, Lboolean when is_integral_type t -> Lboolean
| Lreal, Ctype ty | Ctype ty, Lreal when isArithmeticType ty -> Lreal
| Ltype (s1,l1), Ltype (s2,l2)
when s1.lt_name = s2.lt_name && List.for_all2 is_same_type l1 l2 ->
@@ -3083,16 +3082,11 @@ struct
| PLrel (t1, (Eq | Neq | Lt | Le | Gt | Ge as op), t2) ->
let env = drop_qualifiers env in
let f _ op t1 t2 =
- (TBinOp(binop_of_rel op, t1, t2),
- Ltype(Logic_env.find_logic_type Utf8_logic.boolean,[]))
+ (TBinOp(binop_of_rel op, t1, t2), Lboolean)
in
type_relation ctxt env f t1 op t2
- | PLtrue ->
- let ctrue = Logic_env.find_logic_ctor "\\true" in
- TDataCons(ctrue,[]), Ltype(ctrue.ctor_type,[])
- | PLfalse ->
- let cfalse = Logic_env.find_logic_ctor "\\false" in
- TDataCons(cfalse,[]), Ltype(cfalse.ctor_type,[])
+ | PLtrue -> TConst(Boolean true), Lboolean
+ | PLfalse -> TConst(Boolean false), Lboolean
| PLlambda(prms,e) ->
let env = drop_qualifiers env in
let (prms, env) = add_quantifiers ctxt loc ~kind:LVFormal prms env in
@@ -3101,17 +3095,17 @@ struct
| PLnot t ->
let env = drop_qualifiers env in
let t = type_bool_term ctxt env t in
- TUnOp(LNot,t), Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[])
+ TUnOp(LNot,t), Lboolean
| PLand (t1,t2) ->
let env = drop_qualifiers env in
let t1 = type_bool_term ctxt env t1 in
let t2 = type_bool_term ctxt env t2 in
- TBinOp(LAnd,t1,t2), Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[])
+ TBinOp(LAnd,t1,t2), Lboolean
| PLor (t1,t2) ->
let env = drop_qualifiers env in
let t1 = type_bool_term ctxt env t1 in
let t2 = type_bool_term ctxt env t2 in
- TBinOp(LOr,t1,t2), Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[])
+ TBinOp(LOr,t1,t2), Lboolean
| PLtypeof t1 ->
let env = drop_qualifiers env in
let t1 = term env t1 in
@@ -3119,7 +3113,7 @@ struct
| PLtype ty ->
begin match logic_type ctxt loc env ty with
| Ctype ty -> Ttype ty, Ltype (Logic_env.find_logic_type "typetag",[])
- | Linteger | Lreal | Ltype _ | Lvar _ | Larrow _ ->
+ | Lboolean | Linteger | Lreal | Ltype _ | Lvar _ | Larrow _ ->
ctxt.error loc "cannot take type tag of logic type"
end
| PLlet (ident, def, body) ->
@@ -3403,7 +3397,7 @@ struct
if not (plain_boolean_type tt.term_type) then
ctxt.error t.lexpr_loc "boolean expected but %a found"
Cil_printer.pp_logic_type tt.term_type;
- mk_cast tt (Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[]))
+ mk_cast tt Lboolean
and type_num_term_option ctxt env t =
match t with
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index ecadf4ba6eda50471cfdcbf829e71e247f951b01..5003975902505b717b0ad3ea36bbe30e6864c4d0 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -33,7 +33,8 @@ let rec unroll_type ?(unroll_typedef=true) = function
| Ltype (tdef,_) as ty when Logic_const.is_unrollable_ltdef tdef ->
unroll_type ~unroll_typedef (Logic_const.unroll_ltdef ty)
| Ctype ty when unroll_typedef -> Ctype (Cil.unrollType ty)
- | Linteger | Lreal | Lvar _ | Larrow _ | Ctype _ | Ltype _ as ty -> ty
+ | Linteger | Lboolean | Lreal | Lvar _ | Larrow _ | Ctype _ | Ltype _ as ty ->
+ ty
let is_instance_of vars t1 t2 =
let rec aux map t1 t2 =
@@ -56,7 +57,7 @@ let is_instance_of vars t1 t2 =
(Cil.typeDeepDropAllAttributes t1)
(Cil.typeDeepDropAllAttributes t2),
map
- | (Lvar _ | Ctype _ | Linteger | Lreal | Ltype _ | Larrow _), _ ->
+ | (Lvar _ | Ctype _ | Lboolean | Linteger | Lreal | Ltype _ | Larrow _), _ ->
Cil_datatype.Logic_type.equal t1 t2, map
and aux_list map l1 l2 =
match l1, l2 with
@@ -290,6 +291,8 @@ let constant_to_lconstant c = match c with
LReal (real_of_float s f)
let lconstant_to_constant c = match c with
+ | Boolean b ->
+ CInt64 ((if b then Integer.one else Integer.zero), IBool, None)
| Integer (i,s) ->
begin
try
@@ -379,8 +382,7 @@ let is_zero_comparable t =
match unroll_type t.term_type with
| Ctype (TInt _ | TFloat _ | TPtr _ | TArray _ | TFun _ | TEnum _) -> true
| Ctype (TVoid _ | TNamed _ | TComp _ | TBuiltin_va_list _) -> false
- | Linteger | Lreal -> true
- | Ltype ({lt_name},[]) -> lt_name = Utf8_logic.boolean
+ | Linteger | Lreal | Lboolean -> true
| Ltype _ -> false
| Lvar _ | Larrow _ -> false
@@ -393,8 +395,7 @@ let scalar_term_conversion conversion t =
let ptr_conversion t =
conversion ~loc false t (Logic_const.term ~loc Tnull t.term_type) in
let bool_conversion t =
- let ctrue = Logic_env.Logic_ctor_info.find "\\true" in
- conversion ~loc true t (term ~loc (TDataCons(ctrue,[])) boolean_type) in
+ conversion ~loc true t (Logic_const.tboolean ~loc true) in
match unroll_type t.term_type with
| Ctype (TInt _ | TEnum _) -> int_conversion t
| Ctype (TFloat _) as ltyp -> real_conversion ~ltyp t
@@ -405,8 +406,7 @@ let scalar_term_conversion conversion t =
(* decay as pointer *)
| Linteger -> int_conversion t
| Lreal -> real_conversion t
- | Ltype ({lt_name = name},[]) when name = Utf8_logic.boolean ->
- bool_conversion t
+ | Lboolean -> bool_conversion t
| Ltype _ | Lvar _ | Larrow _
| Ctype (TVoid _ | TNamed _ | TComp _ | TBuiltin_va_list _)
-> Kernel.fatal
@@ -421,7 +421,7 @@ let scalar_term_to_predicate =
let scalar_term_to_boolean =
let conversion ~loc is_eq t1 t2 =
let op = if is_eq then Eq else Ne in
- term ~loc (TBinOp(op,t1,t2)) Logic_const.boolean_type
+ term ~loc (TBinOp(op,t1,t2)) Lboolean
in
scalar_term_conversion conversion
@@ -545,7 +545,7 @@ and offset_to_term_offset = function
and expr_to_boolean e =
let open Cil_types in
- let tbool n = Logic_const.term n Logic_const.boolean_type in
+ let tbool n = Logic_const.term n Lboolean in
let tnot t = tbool @@ TUnOp(LNot, t) in
let tcompare op a b =
let va = expr_to_term ~coerce:true a in
@@ -1280,6 +1280,7 @@ let rec is_same_pl_type t1 t2 =
let open Logic_ptree in
match t1, t2 with
| LTvoid, LTvoid
+ | LTboolean, LTboolean
| LTinteger, LTinteger
| LTreal, LTreal -> true
| LTint k1, LTint k2 ->
@@ -1315,7 +1316,7 @@ let rec is_same_pl_type t1 t2 =
is_same_list is_same_pl_type prms1 prms2 && is_same_pl_type t1 t2
| LTattribute(t1,attr1), LTattribute(t2,attr2) ->
is_same_pl_type t1 t2 && attr1 = attr2
- | (LTvoid | LTinteger | LTreal | LTint _ | LTfloat _ | LTarrow _
+ | (LTvoid | LTboolean | LTinteger | LTreal | LTint _ | LTfloat _ | LTarrow _
| LTarray _ | LTpointer _ | LTenum _
| LTunion _ | LTnamed _ | LTstruct _ | LTattribute _),_ ->
false
@@ -2209,7 +2210,7 @@ let lhost_c_type thost =
| Ctype typ -> Some typ
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
get (unroll_ltdef ty)
- | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _ -> None
+ | Ltype _ | Lvar _ | Lboolean | Linteger | Lreal | Larrow _ -> None
in
match Logic_const.plain_or_set get lty with
| None ->
@@ -2394,6 +2395,7 @@ let rec constFoldTermToInt ?(machdep=true) (e: term) : Integer.t option =
| TUnOp(unop, e) -> constFoldUnOpToInt ~machdep unop e
| TConst(LChr c) -> Some (charConstToInt c)
| TConst(LEnum {eival = v}) -> Cil.constFoldToInt ~machdep v
+ | TConst (Boolean b) -> Some (if b then Z.one else Z.zero)
| TConst (Integer (i, _)) -> Some i
| TConst (LReal _ | LWStr _ | LStr _) -> None
| TSizeOf typ -> constFoldSizeOfToInt ~machdep typ
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 2669ced475387e4835a49716b5079143ea86bcb5..c5f7c4577947da7e4f07a72187386487453a147b 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -40,6 +40,7 @@ type array_size =
(** logic types. *)
type logic_type =
| LTvoid (** C void *)
+ | LTboolean (** booleans *)
| LTinteger (** mathematical integers. *)
| LTreal (** mathematical real. *)
| LTint of Cil_types.ikind (** C integral type.*)
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 2e3e91305da4f48e33281e7d1dc0e01a3ca700ba..bb6bcecb3292a6805a73831c6e2a7d50041dd700 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -222,8 +222,7 @@ end = struct
let v =
match v.lv_type with
| Ctype ty when Cil.isIntegralType ty -> v
- | Linteger -> v
- | Ltype _ as ty when Logic_const.is_boolean_type ty -> v
+ | Linteger | Lboolean -> v
| Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
Error.not_yet
(error_msg
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 05320831cb2ba5cfce57e5d7559654b5e8cb92b2..50e43208234aec8a42d76eb3c8648d1e55d50c10 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -349,6 +349,7 @@ let rec infer ~force ~logic_env t =
in
let compute t =
match t.term_node with
+ | TConst (Boolean b) -> singleton (if b then Z.one else Z.zero)
| TConst (Integer (n, _)) -> singleton n
| TConst (LChr c) ->
let n = Cil.charConstToInt c in
@@ -488,7 +489,7 @@ let rec infer ~force ~logic_env t =
| Some (Ctype typ) ->
ignore ((infer ~force ~logic_env t'));
interv_of_typ typ;
- | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+ | None | Some _ ->
get_res (infer ~force ~logic_env t'))
| _ -> assert false)
| LBnone when li.l_var_info.lv_name = "\\sum" ||
@@ -585,7 +586,7 @@ and initiate_fixpoint ~logic_env li args_ival args =
(match li.l_type with
| Some (Ctype typ) ->
interv_of_typ typ, PoT_term t
- | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+ | None | Some _ ->
Ival (Ival.bottom), PoT_term t)
| _ -> assert false
in
@@ -625,11 +626,13 @@ and infer_term_host ~force ~logic_env thost =
| TVar v ->
(try Logic_env.find logic_env v with Not_found ->
match v.lv_type with
+ | Lboolean -> ival Z.zero Z.one
| Linteger -> top_ival
| Ctype (TFloat(fk, _)) -> Float(fk, None)
| Lreal -> Real
| Ctype _ -> interv_of_typ (Logic_utils.logicCType v.lv_type)
- | Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type")
+ | Ltype _ | Lvar _ | Larrow _ ->
+ Options.fatal "unexpected logic type")
| TResult ty ->
interv_of_typ ty
| TMem t ->
@@ -733,7 +736,7 @@ and infer_bound_variable ~loc ~logic_env (t1, lv, t2) =
let i = unify (join i1 i2) in
let t1, t2, i =
match lv.lv_type with
- | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ | Ltype _ | Lvar _ | Lreal | Lboolean | Larrow _ ->
Error.not_yet "quantification over non-integer type"
| Linteger -> t1, t2, i
| Ctype ty ->
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index 8c0478348ff40a11be1f1b57d865818f56d47980..020f06719b7fd906a16549fef106de144eae7582 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -259,7 +259,7 @@ module rec Transfer
let may_alias li = match li.l_var_info.lv_type with
| Ctype ty -> is_ptr_or_array ty
- | Linteger | Lreal -> false
+ | Lboolean | Linteger | Lreal -> false
| Ltype _ -> Error.not_yet "user defined type"
| Lvar _ -> Error.not_yet "named type"
| Larrow _ -> Error.not_yet "functional type"
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index df3fa3c6b4b174cf5ed97640890c39c9cfc0260f..b1c8f8c14f13920c2e42c82cb52c68be12beaf17 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -111,7 +111,8 @@ let typ_of_lty = function
| Ctype cty -> cty
| Linteger -> Gmp_types.Z.t ()
| Lreal -> Error.not_yet "real type"
- | Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type"
+ | Lboolean | Ltype _ | Lvar _ | Larrow _ ->
+ Options.fatal "unexpected logic type"
(******************************************************************************)
(** Memoization *)
@@ -277,6 +278,7 @@ let ty_of_logic_ty ?term ~profile lty =
| Ctype ty -> number_ty_of_typ ~post:false ty
| Lreal -> Real
| Larrow _ -> Nan
+ | Lboolean -> Error.not_yet "boolean logic type"
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
in
@@ -361,7 +363,7 @@ let rec type_term
(and of course also covers the missing cases). Also enforce the invariant
that every subterm is typed, even if it is not an integer. *)
match t.term_node with
- | TConst (Integer _ | LChr _ | LEnum _ | LReal _)
+ | TConst (Boolean _ | Integer _ | LChr _ | LEnum _ | LReal _)
| TSizeOf _
| TSizeOfStr _
| TAlignOf _ ->
@@ -521,7 +523,7 @@ let rec type_term
|_ -> if Options.Gmp_only.get() then Some Gmpz else None
end
| Lreal -> Some Real
- | Ctype _| Ltype _| Larrow _ | Lvar _ -> None
+ | Lboolean | Ctype _ | Ltype _ | Larrow _ | Lvar _ -> None
in
ignore
(type_term
@@ -615,7 +617,7 @@ let rec type_term
| TNamed _
| TComp _
| TBuiltin_va_list _))
- | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+ | Some (Lboolean | Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
ty_of_interv
?ctx:ctx_body
~use_gmp_opt:(gmp && use_gmp_opt)
@@ -909,7 +911,7 @@ let extract_typ t ty =
with Not_a_number ->
match t.term_type with
| Ctype _ as lty -> Logic_utils.logicCType lty
- | Linteger | Lreal ->
+ | Lboolean | Linteger | Lreal ->
Options.fatal "unexpected context NaN for term %a" Printer.pp_term t
| Ltype _ -> Error.not_yet "unsupported logic type: user-defined type"
| Lvar _ -> Error.not_yet "unsupported logic type: type variable"
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index e4f729209f8f92db3cdd65e46cf9c3ea7343d3dc..4842921bd11bccf7ab523e0e2540008a4ca0dda2 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -329,7 +329,7 @@ module Logic_binding = struct
| None -> match logic_v.lv_type with
| Ctype ty -> ty
| Linteger -> Gmp_types.Z.t ()
- | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil_const.charType
+ | Lboolean -> Cil_const.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
Format.asprintf
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index b1abe02964f2dd81c1325fcbb930961cd1cec70b..c144bef77f7517182a82f149a16b058bc317ca06 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -51,6 +51,8 @@ let constant_to_exp ~loc env t c =
Cil.mkString ~loc s, Analyses_types.Str_R
in
match c with
+ | Boolean b ->
+ (if b then Cil.one ~loc else Cil.zero ~loc), Analyses_types.C_number
| Integer(n, _repr) ->
let logic_env = Env.Logic_env.get env in
let ity = Typing.get_number_ty ~logic_env t in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index cea3235a866d0e0ec8355b138709f28edf10f86c..97bcb39caa54357fe75ffab17e217e70a093e7c2 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -272,6 +272,8 @@ let env_of_li ~adata ~loc kf env li =
| Real -> Error.not_yet "real number"
in
adata, Env.add_stmt env stmt
+ | Lboolean ->
+ Env.not_yet env "booleans"
| Ltype _ ->
Env.not_yet env "user-defined logic type"
| Lvar _ ->
diff --git a/src/plugins/e-acsl/src/libraries/interval_utils.ml b/src/plugins/e-acsl/src/libraries/interval_utils.ml
index 2b3a66396cfede22e832384babe3fabf91ad4006..7123a45a58c88d8d3aa1f3a834cf503d4264c03c 100644
--- a/src/plugins/e-acsl/src/libraries/interval_utils.ml
+++ b/src/plugins/e-acsl/src/libraries/interval_utils.ml
@@ -272,6 +272,7 @@ let interv_of_logic_typ = function
| Ctype ty -> interv_of_typ ty
| Linteger -> top_ival
| Lreal -> Real
+ | Lboolean -> Error.not_yet "boolean"
| Ltype _ -> Error.not_yet "user-defined logic type"
| Lvar _ -> Error.not_yet "type variable"
| Larrow _ -> Nan
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index e1ea93a8e4b694429e13b6f8980df08e7b9b5e1a..6252217ecbd5a291c9d4ef995b13fa48888c9294 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -165,7 +165,7 @@ let is_bitfield_pointers lty =
| _ ->
false
end
- | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _ ->
+ | Ltype _ | Lvar _ | Lboolean | Linteger | Lreal | Larrow _ ->
false
in
if Logic_const.is_set_type lty then
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 6ea6f74635e3967de6c3b6d100e358da724b2b46..61c1a73899c027eb2f8c8723e43d98904a83659c 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -46,9 +46,13 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:196: Warning:
- E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:204: Warning:
- E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:192: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
index d6ab15b134feef6c04847d8603b2d0b999f4f181..66d16674c03c91bd18f51a25b836c0cfc23e445f 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
@@ -7,7 +7,9 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:151: Warning:
- E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:138: Warning:
no assigns clause generated for function valid_read_or_empty because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/string.h:137: Warning:
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index c9851298903b4367411d8b16bb63c8b09e3a5e65..4e14e33da388847b5440e474374c1e29322cfdaa 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -7,7 +7,9 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:151: Warning:
- E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:113: Warning:
no assigns clause generated for function valid_read_or_empty because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/string.h:112: Warning:
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 8c8361ee2f55a6982fdffceb878c2034b4d970d8..e230fd583c0245c6e38cda79ff4ae361932fbadf 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -503,11 +503,10 @@ let rec isLogicNonCompositeType t =
match t with
| Lvar _ | Larrow _ -> false
| Ltype (info, _) ->
- Logic_const.is_boolean_type t ||
info.lt_name = "sign" ||
(try isLogicNonCompositeType (Logic_const.type_of_element t)
with Failure _ -> false)
- | Linteger | Lreal -> true
+ | Lboolean | Linteger | Lreal -> true
| Ctype t -> Cil.isScalarType t
let rec infer_type = function
@@ -517,6 +516,7 @@ let rec infer_type = function
| TFloat _ -> Cil_const.doubleType
| _ -> t)
| Lvar _ -> Cil_const.voidPtrType (* For polymorphic empty sets *)
+ | Lboolean -> Cil_const.boolType
| Linteger -> Cil_const.intType
| Lreal -> Cil_const.doubleType
| Ltype _ | Larrow _ as t ->
@@ -1008,6 +1008,8 @@ let rec eval_term ~alarm_mode env t =
ignore (env_state env lab);
eval_term ~alarm_mode { env with e_cur = lab } t
+ | TConst (Boolean true) -> einteger Cvalue.V.singleton_one
+ | TConst (Boolean false) -> einteger Cvalue.V.singleton_zero
| TConst (Integer (v, _)) -> einteger (Cvalue.V.inject_int v)
| TConst (LEnum e) ->
(match Cil.constFoldToInt e.eival with
@@ -1318,8 +1320,6 @@ let rec eval_term ~alarm_mode env t =
match ctor_info.ctor_name with
| "\\Positive" -> einteger positive_cvalue
| "\\Negative" -> einteger negative_cvalue
- | "\\true" -> einteger Cvalue.V.singleton_one
- | "\\false" -> einteger Cvalue.V.singleton_zero
| _ -> unsupported "logic inductive types"
end
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index ef9898edec49d940caf3922d379b809c4e3f100f..fa1cdc224cda47682d4403edb0aef9043041c862 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -52,6 +52,8 @@ let rec constant = function
| CStr _ | CWStr _ -> Warning.error "String constants not yet implemented"
and logic_constant = function
+ | Boolean true -> e_true
+ | Boolean false -> e_false
| Integer(z,_) -> e_bigint z
| LChr c -> e_int64 (Ctypes.char c)
| LReal r -> Cfloat.acsl_lit r
@@ -320,7 +322,7 @@ let cdomain obj =
let ldomain ltype =
match Logic_utils.unroll_type ~unroll_typedef:false ltype with
| Ctype typ -> cdomain (Ctypes.object_of typ)
- | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _ -> None
+ | Ltype _ | Lvar _ | Lboolean | Linteger | Lreal | Larrow _ -> None
(* -------------------------------------------------------------------------- *)
(* --- Volatile --- *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index a026b4ac453d1401d74e562bf73f5eda18f12fd9..f90e9262f35bd6f38661d1d6b25211a638ecc686 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -158,6 +158,7 @@ let sort_of_ctype t = sort_of_object (Ctypes.object_of t)
let sort_of_ltype t = match Logic_utils.unroll_type ~unroll_typedef:false t with
| Ctype typ -> sort_of_ctype typ
| Ltype _ | Lvar _ | Larrow _ -> Logic.Sdata
+ | Lboolean -> Logic.Sbool
| Linteger -> Logic.Sint
| Lreal -> Logic.Sreal
@@ -215,6 +216,7 @@ let atype lt ts =
let rec tau_of_ltype t =
match Logic_utils.unroll_type ~unroll_typedef:false t with
+ | Lboolean -> Logic.Bool
| Linteger -> Logic.Int
| Lreal -> Logic.Real
| Ctype typ -> tau_of_ctype typ
@@ -222,7 +224,6 @@ let rec tau_of_ltype t =
| Larrow _ ->
Warning.error "array type non-supported(%a)"
Printer.pp_logic_type t
- | Ltype _ as b when Logic_const.is_boolean_type b -> Logic.Bool
| Ltype(lt,lts) -> atype lt (List.map tau_of_ltype lts)
let tau_of_return = function None -> Logic.Prop | Some t -> tau_of_ltype t
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 20a6f81500acda300c516d1980d85e3d35849c5f..1dc34ddc4a07f1d6417cd89e2801991361b549c8 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -37,6 +37,7 @@ type builtin =
| HACK of (F.term list -> F.term)
type kind =
+ | B (* boolean *)
| Z (* integer *)
| R (* real *)
| I of Ctypes.c_int
@@ -53,6 +54,7 @@ let okind = function
let ckind typ = okind (object_of typ)
let skind = function
+ | B -> Logic.Sbool
| I _ | Z -> Logic.Sint
| F _ | R -> Logic.Sreal
| A -> Logic.Sdata
@@ -63,16 +65,19 @@ let rec lkind t =
| Ltype({lt_name="set"},[t]) -> lkind t
| Lreal -> R
| Linteger -> Z
+ | Lboolean -> B
| Ltype _ | Larrow _ | Lvar _ -> A
let kind_of_tau = function
| Qed.Logic.Int -> Z
| Qed.Logic.Real -> R
+ | Qed.Logic.Bool -> B
| _ -> A
let pp_kind fmt = function
| I i -> Ctypes.pp_int fmt i
| F f -> Ctypes.pp_float fmt f
+ | B -> Format.pp_print_string fmt "bool"
| Z -> Format.pp_print_string fmt "int"
| R -> Format.pp_print_string fmt "real"
| A -> Format.pp_print_string fmt "_"
diff --git a/src/plugins/wp/LogicBuiltins.mli b/src/plugins/wp/LogicBuiltins.mli
index 504bd54799b54d0221a031e157494710e58f6002..c72bc193ea3fca22da719070643ab0d8bea9a49b 100644
--- a/src/plugins/wp/LogicBuiltins.mli
+++ b/src/plugins/wp/LogicBuiltins.mli
@@ -30,6 +30,7 @@ open Lang
type category = Lang.lfun Qed.Logic.category
type kind =
+ | B (** boolean *)
| Z (** integer *)
| R (** real *)
| I of Ctypes.c_int (** C-ints *)
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 4a3c76171f47c4673c4a21496848a3c04aa18ac6..86c92393cded77b4452cbf190526ca942ba8112e 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -854,15 +854,13 @@ struct
let rec logic_type t =
match Logic_utils.unroll_type ~unroll_typedef:false t with
| Ctype _ -> ()
- | Linteger | Lreal | Lvar _ | Larrow _ -> ()
+ | Lboolean | Linteger | Lreal | Lvar _ | Larrow _ -> ()
| Ltype(lt,ps) ->
List.iter logic_type ps ;
if not (Typedefs.mem lt) then
begin
Typedefs.update lt None ;
- if not (Lang.is_builtin lt) &&
- not (Logic_const.is_boolean_type t)
- then
+ if not (Lang.is_builtin lt) then
let section = LogicUsage.section_of_type lt in
let cluster = Definitions.section section in
match section with
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index b49ce991d37a695a905a8bb2a2d3ee368d7548eb..77b875676c0626ad8f6cd09fa7ed82a70b1bbae0 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -284,7 +284,7 @@ struct
let eqsort_of_type t =
match Logic_utils.unroll_type ~unroll_typedef:false t with
| Ltype({lt_name="set"},[_]) -> EQ_set
- | Linteger | Lreal | Lvar _ | Larrow _ | Ltype _ -> EQ_plain
+ | Lboolean | Linteger | Lreal | Lvar _ | Larrow _ | Ltype _ -> EQ_plain
| Ctype t ->
match Ctypes.object_of t with
| C_pointer _ -> EQ_loc
@@ -462,6 +462,7 @@ struct
let rec cvsort_of_ltype src_ltype =
match Logic_utils.unroll_type ~unroll_typedef:false src_ltype with
+ | Lboolean -> L_bool
| Linteger -> L_integer
| Lreal -> L_real
| Ctype src_ctype ->
@@ -598,14 +599,14 @@ struct
L.map Cmath.int_of_bool (C.logic env t)
| L_real | L_cfloat _ | L_pointer _ | L_array _ ->
Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
- Printer.pp_logic_type src_ltype Printer.pp_logic_type Logic_const.boolean_type
+ Printer.pp_logic_type src_ltype Printer.pp_logic_type Lboolean
let rec term_cast_to_ltype env dst_ltype t =
match Logic_utils.unroll_type ~unroll_typedef:false dst_ltype with
| Ctype typ-> term_cast_to_ctype env typ t
+ | Lboolean -> term_cast_to_boolean env t
| Linteger -> term_cast_to_integer env t
| Lreal -> term_cast_to_real env t
- | Ltype _ as b when Logic_const.is_boolean_type b -> term_cast_to_boolean env t
| Ltype({lt_name="set"},[elt_ltype]) -> (* lifting, set of elements ? *)
term_cast_to_ltype env elt_ltype t
| (Ltype _ | Lvar _ | Larrow _) as dst_ltype ->
@@ -691,9 +692,6 @@ struct
| Tlambda _ ->
Warning.error "Lambda-functions not yet implemented"
- | TDataCons({ctor_name="\\true"},_) -> Vexp(e_true)
- | TDataCons({ctor_name="\\false"},_) -> Vexp(e_false)
-
| TDataCons(c,ts) ->
let es = List.map (val_of_term env) ts in
let r = match LogicBuiltins.ctor c with
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
index 4a51426aad2d032bde154cb779aa18cd690dd965..9b698c9fd3ae57bb2cfa897496976ee7add29e4e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -80,13 +80,13 @@
------------------------------------------------------------
[wp:script:allgoals]
Goal Post-condition (file split.i, line 55) in 'test_step_peq':
- Assume { (* Pre-condition *) Have: L_LQ = L_LP. }
+ Assume { (* Pre-condition *) Have: (L_LQ=true) <-> (L_LP=true). }
Prove: P_S.
------------------------------------------------------------
[wp:script:allgoals]
Goal Post-condition (file split.i, line 59) in 'test_step_pneq':
- Assume { (* Pre-condition *) Have: L_LQ != L_LP. }
+ Assume { (* Pre-condition *) Have: !((L_LQ=true) <-> (L_LP=true)). }
Prove: P_S.
------------------------------------------------------------
@@ -195,13 +195,13 @@
[wp:script:allgoals]
Goal Post-condition (file split.i, line 107) in 'test_goal_eq':
Assume { (* Pre-condition *) Have: P_S. }
- Prove: L_LQ = L_LP.
+ Prove: (L_LQ=true) <-> (L_LP=true).
------------------------------------------------------------
[wp:script:allgoals]
Goal Post-condition (file split.i, line 111) in 'test_goal_neq':
Assume { (* Pre-condition *) Have: P_S. }
- Prove: L_LQ != L_LP.
+ Prove: !((L_LQ=true) <-> (L_LP=true)).
------------------------------------------------------------
[wp:script:allgoals]
@@ -330,7 +330,7 @@
typed_test_step_pneq_ensures subgoal:
Goal Wp.Tactical.typed_test_step_pneq_ensures-0 (generated):
- Assume { (* True/False *) When: (L_LQ=true) /\ (L_LP=false). }
+ Assume { (* True/False *) When: (L_LP=false) /\ (L_LQ=true). }
Prove: P_S.
------------------------------------------------------------