Skip to content

Commit a63af50

Browse files
committed
Add Cilfacade.mkCast to fix base invariant crashes
1 parent 2bfadcd commit a63af50

File tree

5 files changed

+14
-3
lines changed

5 files changed

+14
-3
lines changed

.semgrep/cil.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ rules:
55
- pattern: Cil.typeOfLval
66
- pattern: Cil.typeOfInit
77
- pattern: Cil.typeOffset
8+
- pattern: Cil.mkCast
89
- pattern: Cil.get_stmtLoc
910
paths:
1011
exclude:

src/analyses/base.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -511,7 +511,7 @@ struct
511511
let toInt i =
512512
match IdxDom.to_int @@ ID.cast_to ik i with
513513
| Some x -> Const (CInt (x,ik, None))
514-
| _ -> mkCast ~e:(Const (CStr ("unknown",No_encoding))) ~newt:intType
514+
| _ -> Cilfacade.mkCast ~e:(Const (CStr ("unknown",No_encoding))) ~newt:intType
515515

516516
in
517517
match o with

src/cdomains/apron/apronDomain.apron.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -368,7 +368,7 @@ struct
368368
match V.to_cil_varinfo fundec v with
369369
| Some vinfo ->
370370
(* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *)
371-
let var = Cil.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
371+
let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
372372
let coeff, flip = coeff_to_const true c in
373373
let prod = BinOp(Mult, coeff, var, longlong) in
374374
if flip then

src/cdomains/intDomain.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -319,7 +319,7 @@ struct
319319
let name () = "IntDomLifter(" ^ (I.name ()) ^ ")"
320320
let to_yojson x = I.to_yojson x.v
321321
let invariant e x =
322-
let e' = Cil.(mkCast ~e ~newt:(TInt (x.ikind, []))) in
322+
let e' = Cilfacade.mkCast ~e ~newt:(TInt (x.ikind, [])) in
323323
I.invariant_ikind e' x.ikind x.v
324324
let tag x = I.tag x.v
325325
let arbitrary ik = failwith @@ "Arbitrary not implement for " ^ (name ()) ^ "."

src/util/cilfacade.ml

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -442,6 +442,16 @@ and typeOffset basetyp =
442442
| _ -> raise (TypeOfError Field_NonCompound)
443443

444444

445+
(** {!Cil.mkCast} using our {!typeOf}. *)
446+
let mkCast ~(e: exp) ~(newt: typ) =
447+
let oldt =
448+
try
449+
typeOf e
450+
with TypeOfError _ -> (* e might involve alloc variables, weird offsets, etc *)
451+
Cil.voidType (* oldt is only used for avoiding duplicate cast, so this falls back to adding cast *)
452+
in
453+
Cil.mkCastT ~e ~oldt ~newt
454+
445455
let get_ikind_exp e = get_ikind (typeOf e)
446456

447457

0 commit comments

Comments
 (0)