From ad86f36f3343878c747313a5f51fc210be369f3d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 26 Apr 2019 11:34:39 +0200
Subject: [PATCH] [WP] fixes _Bool layout
---
src/plugins/wp/ctypes.ml | 18 +++++++++---------
src/plugins/wp/ctypes.mli | 2 +-
2 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index bde88014eff..a108e37fd5a 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -30,7 +30,7 @@ open Cil_datatype
module WpLog = Wp_parameters
type c_int =
- | Bool
+ | CBool
| UInt8
| SInt8
| UInt16
@@ -43,19 +43,19 @@ type c_int =
let compare_c_int : c_int -> c_int -> _ = Extlib.compare_basic
let signed = function
- | Bool -> false
+ | CBool -> false
| UInt8 | UInt16 | UInt32 | UInt64 -> false
| SInt8 | SInt16 | SInt32 | SInt64 -> true
let i_bits = function
- | Bool -> 1
+ | CBool -> 8
| UInt8 | SInt8 -> 8
| UInt16 | SInt16 -> 16
| UInt32 | SInt32 -> 32
| UInt64 | SInt64 -> 64
let i_bytes = function
- | Bool -> 1
+ | CBool -> 1
| UInt8 | SInt8 -> 1
| UInt16 | SInt16 -> 2
| UInt32 | SInt32 -> 4
@@ -73,12 +73,12 @@ let is_char = function
| SInt8 -> not Cil.theMachine.Cil.theMachine.char_is_unsigned
| UInt16 | SInt16
| UInt32 | SInt32
- | UInt64 | SInt64 | Bool -> false
+ | UInt64 | SInt64 | CBool -> false
let c_int ikind =
let mach = Cil.theMachine.Cil.theMachine in
match ikind with
- | IBool -> if Wp_parameters.get_bool_range () then Bool else UInt8
+ | IBool -> CBool
| IChar -> if mach.char_is_unsigned then UInt8 else SInt8
| ISChar -> SInt8
| IUChar -> UInt8
@@ -163,7 +163,7 @@ let idx = function
| SInt32 -> 5
| UInt64 -> 6
| SInt64 -> 7
- | Bool -> 8
+ | CBool -> 8
let i_memo f =
let m = Array.make 9 None in
@@ -186,7 +186,7 @@ let f_memo f =
| None -> let r = f z in m.(k) <- Some r ; r
let i_iter f =
- List.iter f [Bool;UInt8;SInt8;UInt16;SInt16;UInt32;SInt32;UInt64;SInt64]
+ List.iter f [CBool;UInt8;SInt8;UInt16;SInt16;UInt32;SInt32;UInt64;SInt64]
let f_iter f =
List.iter f [Float32;Float64]
@@ -210,7 +210,7 @@ let bounds i = i_memo i_bounds i
(* -------------------------------------------------------------------------- *)
let pp_int fmt i =
- if i = Bool then Format.pp_print_string fmt "bool"
+ if i = CBool then Format.pp_print_string fmt "bool"
else Format.fprintf fmt "%cint%d" (if signed i then 's' else 'u') (i_bits i)
let pp_float fmt f = Format.fprintf fmt "float%d" (f_bits f)
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index 234bd3119eb..bb3c965c1bd 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/src/plugins/wp/ctypes.mli
@@ -28,7 +28,7 @@ open Cil_types
(** Runtime integers. *)
type c_int =
- | Bool
+ | CBool
| UInt8
| SInt8
| UInt16
--
GitLab