Skip to content

Commit 7525631

Browse files
committed
Remove Unknown castkind
1 parent f720db4 commit 7525631

6 files changed

Lines changed: 7 additions & 11 deletions

File tree

src/cil.ml

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -624,7 +624,6 @@ and castkind =
624624
| PointerConversion (** Pointer conversion (non-standard). @see C11 6.5.6.8, 6.5.8.5 and 6.5.9.5. *)
625625
| Implicit (** Implicit conversion. @see C11 6.3.1, 6.5.2.2.7, 6.5.2.4.2, 6.5.16.1.2, 6.5.16.2.3, 6.7.9.11, 6.8.4.2.5 and 6.8.6.4.3. *)
626626
| Internal (** CIL-internal conversion (non-standard). *)
627-
| Unknown (** Unknown conversion. *)
628627

629628
(** An lvalue denotes the contents of a range of memory addresses. This range
630629
is denoted as a host object along with an offset within the object. The
@@ -2893,7 +2892,6 @@ let d_castkind () k =
28932892
| PointerConversion -> text "PointerConversion"
28942893
| Implicit -> text "Implicit"
28952894
| Internal -> text "Internal"
2896-
| Unknown -> text "Unknown"
28972895

28982896
let invalidStmt = mkStmt (Instr [])
28992897

src/cil.mli

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -733,7 +733,6 @@ and castkind =
733733
| PointerConversion (** Pointer conversion (non-standard). @see C11 6.5.6.8, 6.5.8.5 and 6.5.9.5. *)
734734
| Implicit (** Implicit conversion. @see C11 6.3.1, 6.5.2.2.7, 6.5.2.4.2, 6.5.16.1.2, 6.5.16.2.3, 6.7.9.11, 6.8.4.2.5 and 6.8.6.4.3. *)
735735
| Internal (** CIL-internal conversion (non-standard). *)
736-
| Unknown (** Unknown conversion. *)
737736

738737
(** {b Lvalues.} Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator.
739738
In C the syntax for lvalues is not always a good indication of the meaning

src/ext/zrapp/rmciltmps.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -429,7 +429,7 @@ let varXformClass action data sid fd nofrm = object(self)
429429
None -> DoChildren
430430
| Some e' ->
431431
(* Cast e' to the correct type. *)
432-
let e'' = mkCast ~kind:Unknown ~e:e' ~newt:vi.vtype in
432+
let e'' = mkCast ~kind:Internal ~e:e' ~newt:vi.vtype in
433433
ChangeTo e'')
434434
| Lval(Mem e', off) ->
435435
(* don't substitute constants in memory lvals *)
@@ -468,15 +468,15 @@ let lvalXformClass action data sid fd nofrm = object(self)
468468
in
469469
ChangeDoChildrenPost(Lval(Mem e', off), post)
470470
| Some e' ->
471-
let e'' = mkCast ~kind:Unknown ~e:e' ~newt:(typeOf(Lval lv)) in
471+
let e'' = mkCast ~kind:Internal ~e:e' ~newt:(typeOf(Lval lv)) in
472472
ChangeDoChildrenPost(e'', castrm)
473473
end
474474
| Lval lv -> begin
475475
match action data sid lv fd nofrm with
476476
| None -> DoChildren
477477
| Some e' -> begin
478478
(* Cast e' to the correct type. *)
479-
let e'' = mkCast ~kind:Unknown ~e:e' ~newt:(typeOf(Lval lv)) in
479+
let e'' = mkCast ~kind:Internal ~e:e' ~newt:(typeOf(Lval lv)) in
480480
ChangeDoChildrenPost(e'', castrm)
481481
end
482482
end

src/formatcil.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ let test () =
157157
(* Construct an instruction *)
158158
let makeInstr () =
159159
Call(Some (var res),
160-
Lval (Mem (CastE(Unknown, TPtr(TFun(TPtr(intType, []),
160+
Lval (Mem (CastE(Explicit, TPtr(TFun(TPtr(intType, []),
161161
Some [ ("", intType, []);
162162
("a2", TPtr(intType, []), []);
163163
("a3", TPtr(TPtr(intType, []),

src/formatparse.mly

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1354,7 +1354,7 @@ stmt:
13541354
let e = (fst $3) args in
13551355
let e =
13561356
if isPointerType(typeOf e) then
1357-
mkCast ~kind:Unknown ~e:e ~newt:!upointType
1357+
mkCast ~kind:Internal ~e:e ~newt:!upointType (* TODO: why this cast here? not done for other ifs/loops *)
13581358
else e
13591359
in
13601360
mkStmt

src/frontc/cabs2cil.ml

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1473,8 +1473,7 @@ let rec castTo ~kind
14731473
| ConditionalConversion
14741474
| PointerConversion
14751475
| Implicit
1476-
| Internal
1477-
| Unknown -> false
1476+
| Internal -> false
14781477
in
14791478
let debugCast = false in
14801479
if debugCast then
@@ -4329,7 +4328,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
43294328
| CEExp (se, e) ->
43304329
let e' =
43314330
let te = typeOf e in
4332-
let _, zte = castTo ~kind:Unknown intType te zero in
4331+
let _, zte = castTo ~kind:Internal intType te zero in (* TODO: is this even reachable? *)
43334332
BinOp(Ne, e, zte, intType)
43344333
in
43354334
finishExp se e' intType

0 commit comments

Comments
 (0)