Skip to content

Commit 53c7eba

Browse files
sim642sim642
committed
Document castkinds
1 parent 41e7bd5 commit 53c7eba

4 files changed

Lines changed: 29 additions & 29 deletions

File tree

‎src/cil.ml‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -616,15 +616,15 @@ and binop =
616616
| LOr (** logical or *)
617617

618618
and castkind =
619-
| Explicit (** Explicit conversion *)
620-
| IntegerPromotion
621-
| DefaultArgumentPromotion
622-
| ArithmeticConversion
623-
| ConditionalConversion (* non-standard terminology *)
624-
| PointerConversion (* non-standard terminology *)
625-
| Implicit (* Implicit conversion *)
626-
| Internal (** Internal conversion not required by standard *)
627-
| Unknown (* TODO: eventually remove *)
619+
| Explicit (** Explicit conversion. @see C11 6.3.1. *)
620+
| IntegerPromotion (** Integer promotion. @see C11 6.3.1.1.2. *)
621+
| DefaultArgumentPromotion (** Default argument promotion. @see C11 6.5.2.2.6. *)
622+
| ArithmeticConversion (** Usual arithmetic conversion. @see C11 6.3.1.8. *)
623+
| ConditionalConversion (** Conditional conversion (non-standard terminology). @see C11 6.5.15.5 and 6.5.15.6. *)
624+
| PointerConversion (** Pointer conversion (non-standard). @see C11 6.5.6.8, 6.5.8.5 and 6.5.9.5. *)
625+
| 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.8.4.2.5 and 6.8.6.4.3. *)
626+
| Internal (** CIL-internal conversion (non-standard). *)
627+
| Unknown (** Unknown conversion. *)
628628

629629
(** An lvalue denotes the contents of a range of memory addresses. This range
630630
is denoted as a host object along with an offset within the object. The

‎src/cil.mli‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -725,15 +725,15 @@ and binop =
725725
set {!useLogicalOperators}. *)
726726

727727
and castkind =
728-
| Explicit (** Explicit conversion *)
729-
| IntegerPromotion
730-
| DefaultArgumentPromotion
731-
| ArithmeticConversion
732-
| ConditionalConversion (* non-standard terminology *)
733-
| PointerConversion (* non-standard terminology *)
734-
| Implicit (** Implicit conversion *)
735-
| Internal (** Internal conversion not required by standard *)
736-
| Unknown (* TODO: eventually remove *)
728+
| Explicit (** Explicit conversion. @see C11 6.3.1. *)
729+
| IntegerPromotion (** Integer promotion. @see C11 6.3.1.1.2. *)
730+
| DefaultArgumentPromotion (** Default argument promotion. @see C11 6.5.2.2.6. *)
731+
| ArithmeticConversion (** Usual arithmetic conversion. @see C11 6.3.1.8. *)
732+
| ConditionalConversion (** Conditional conversion (non-standard terminology). @see C11 6.5.15.5 and 6.5.15.6. *)
733+
| PointerConversion (** Pointer conversion (non-standard). @see C11 6.5.6.8, 6.5.8.5 and 6.5.9.5. *)
734+
| 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.8.4.2.5 and 6.8.6.4.3. *)
735+
| Internal (** CIL-internal conversion (non-standard). *)
736+
| Unknown (** Unknown conversion. *)
737737

738738
(** {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.
739739
In C the syntax for lvalues is not always a good indication of the meaning

‎src/formatparse.mly‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -504,7 +504,7 @@ expression:
504504
{ ((fun args ->
505505
let t = (fst $2) args in
506506
let e = (fst $4) args in
507-
mkCast ~kind:Explicit ~e:e ~newt:t),
507+
mkCast ~kind:Explicit ~e:e ~newt:t), (* C11 6.3.1 *)
508508

509509
(fun e ->
510510
let t', e' =

‎src/frontc/cabs2cil.ml‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1174,7 +1174,7 @@ module BlockChunk =
11741174
let t = typeOf e in
11751175
(* If needed, convert e to type t, and check in case the label was too big *)
11761176
let checkRange e =
1177-
let e' = makeCast ~kind:Implicit ~e ~newt:t in
1177+
let e' = makeCast ~kind:Implicit ~e ~newt:t in (* C11 6.8.4.2.5 *)
11781178
let constFold = constFold false in
11791179
let e'' = if !lowerConstants then constFold e' else e' in
11801180
begin match (constFold e), (constFold e'') with
@@ -3507,7 +3507,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
35073507
(SynthetizeLoc.doChunkTail se, e, t)
35083508
| _ ->
35093509
let (e', t') = processArrayFun e t in
3510-
let (t'', e'') = castTo ~kind:Implicit t' lvt e' in
3510+
let (t'', e'') = castTo ~kind:Implicit t' lvt e' in (* C11 6.5.16.1.2 *)
35113511
(*
35123512
ignore (E.log "finishExp: e = %a\n e'' = %a\n" d_plainexp e d_plainexp e'');
35133513
*)
@@ -3998,7 +3998,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
39983998
need the check. *)
39993999
let newtyp, newexp =
40004000
if needcast then
4001-
castTo ~kind:Explicit t' typ e'
4001+
castTo ~kind:Explicit t' typ e' (* C11 6.3.1 *)
40024002
else
40034003
t', e'
40044004
in
@@ -4123,7 +4123,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
41234123
| _ -> E.s (error "Expected lval for ++ or --")
41244124
in
41254125
let tresult, result = doBinOp uop' e' t one intType in
4126-
finishExp (se +++ (Set(lv, makeCastT ~kind:Implicit ~e:result ~oldt:tresult ~newt:t,
4126+
finishExp (se +++ (Set(lv, makeCastT ~kind:Implicit ~e:result ~oldt:tresult ~newt:t, (* C11 6.5.2.4.2 *)
41274127
!currentLoc, !currentExpLoc)))
41284128
e'
41294129
t
@@ -4171,7 +4171,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
41714171
se, e'
41724172
in
41734173
finishExp
4174-
(se' +++ (Set(lv, makeCastT ~kind:Implicit ~e:opresult ~oldt:tresult ~newt:(typeOfLval lv),
4174+
(se' +++ (Set(lv, makeCastT ~kind:Implicit ~e:opresult ~oldt:tresult ~newt:(typeOfLval lv), (* C11 6.5.2.4.2 *)
41754175
!currentLoc, !currentExpLoc)))
41764176
result
41774177
t
@@ -4287,7 +4287,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
42874287
let tresult, result = doBinOp bop' e1' t1 e2' t2 in
42884288
(* We must cast the result to the type of the lv1, which may be
42894289
different than t1 if lv1 was a Cast *)
4290-
let tresult', result' = castTo ~kind:Implicit tresult (typeOfLval lv1) result in
4290+
let tresult', result' = castTo ~kind:Implicit tresult (typeOfLval lv1) result in (* C11 6.5.16.2.3 *)
42914291
(* Catch the case of an lval that might depend on itself,
42924292
e.g. p[p[0]] when p[0] == 0. We need to use a temporary
42934293
here if the result of the expression will be used:
@@ -4452,7 +4452,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
44524452
test/small1/union5, in which a transparent union is passed
44534453
as an argument *)
44544454
let (sa, a', att) = force_right_to_left_evaluation (doExp false a (AExp None)) in
4455-
let (_, a'') = castTo ~kind:Implicit att at a' in
4455+
let (_, a'') = castTo ~kind:Implicit att at a' in (* C11 6.5.2.2.7 *)
44564456
(sa :: ss, a'' :: args')
44574457
| ([], args) -> (* No more types *)
44584458
(* Do not give a warning for functions without a prototype*)
@@ -6559,7 +6559,7 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function
65596559
TVoid _ -> None
65606560
| (TInt _ | TEnum _ | TFloat _ | TPtr _) as rt ->
65616561
ignore (warnOpt "Body of function %s falls-through. Adding a return statement" !currentFunctionFDEC.svar.vname);
6562-
Some (makeCastT ~kind:Implicit ~e:zero ~oldt:intType ~newt:rt)
6562+
Some (makeCastT ~kind:Implicit ~e:zero ~oldt:intType ~newt:rt) (* C11 6.8.6.4.3 *)
65636563
| _ ->
65646564
ignore (warn "Body of function %s falls-through and cannot find an appropriate return value" !currentFunctionFDEC.svar.vname);
65656565
None
@@ -6683,7 +6683,7 @@ and assignInit (lv: lval)
66836683
(acc: chunk) : chunk =
66846684
match ie with
66856685
SingleInit e ->
6686-
let (_, e'') = castTo ~kind:Implicit iet (typeOfLval lv) e in
6686+
let (_, e'') = castTo ~kind:Implicit iet (typeOfLval lv) e in (* 6.5.16.1.2 *)
66876687
acc +++ (Set(lv, e'', !currentLoc, !currentExpLoc))
66886688
| CompoundInit (t, initl) -> begin
66896689
match unrollType t with
@@ -6900,7 +6900,7 @@ and doStatement (s : A.statement) : chunk =
69006900
typeRemoveAttributes ["warn_unused_result"] !currentReturnType
69016901
in
69026902
let (se, e', et) = doExp false e (AExp (Some rt)) in
6903-
let (et'', e'') = castTo ~kind:Implicit et rt e' in
6903+
let (et'', e'') = castTo ~kind:Implicit et rt e' in (* C11 6.8.6.4.3 *)
69046904
se @@ (returnChunk (Some e'') loc' eloc')
69056905
end
69066906

0 commit comments

Comments
 (0)