Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
a74a3d23
Commit
a74a3d23
authored
1 year ago
by
Andre Maroneze
Browse files
Options
Downloads
Patches
Plain Diff
[kernel] rewrite some comments
parent
bd88fe7d
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/kernel_services/ast_queries/cil.mli
+15
-13
15 additions, 13 deletions
src/kernel_services/ast_queries/cil.mli
with
15 additions
and
13 deletions
src/kernel_services/ast_queries/cil.mli
+
15
−
13
View file @
a74a3d23
...
@@ -1172,18 +1172,20 @@ val need_cast: ?force:bool -> typ -> typ -> bool
...
@@ -1172,18 +1172,20 @@ val need_cast: ?force:bool -> typ -> typ -> bool
This applies only to implicit casts. Casts already present
This applies only to implicit casts. Casts already present
in the source code are exempt from this hook.
in the source code are exempt from this hook.
@since Frama-C+dev*)
@since Frama-C+dev
*)
val
typeForInsertedCast
:
(
exp
->
typ
->
typ
->
typ
)
ref
val
typeForInsertedCast
:
(
exp
->
typ
->
typ
->
typ
)
ref
(** [checkCast context fromsource nullptr_cast oldt newt] emits a warning
(** [checkCast context fromsource nullptr_cast oldt newt] emits a warning
or an error if the cast from [oldt] to [newt] is invalid
.
or an error if the cast from [oldt] to [newt] is invalid
(does nothing
O
therwise
, doesn't make anything
.
o
therwise
)
.
[nullptr_cast] is [true] iff the expression being casted is a null pointer.
[nullptr_cast] is [true] iff the expression being casted is a null pointer.
Default is false.
Default is false.
[fromsource] is [false] (default) if the cast is not from the source.
[fromsource] is [false] (default) if the cast is not present in the source
code.
Check [areCompatibleTypes] documentation for [context].
Check [areCompatibleTypes] documentation for [context].
Suspicious cases that only emit
s
a warning
:
Suspicious cases that only emit a warning:
- Implicit cast from a pointer to an integer.
- Implicit cast from a pointer to an integer.
- Cast from a pointer to a function type to another pointer to a function
- Cast from a pointer to a function type to another pointer to a function
type when the function types are not compatible.
type when the function types are not compatible.
...
@@ -1191,7 +1193,8 @@ val typeForInsertedCast: (exp -> typ -> typ -> typ) ref
...
@@ -1191,7 +1193,8 @@ val typeForInsertedCast: (exp -> typ -> typ -> typ) ref
- Cast, in both directions, between pointer to an object type and pointer
- Cast, in both directions, between pointer to an object type and pointer
to a function type.
to a function type.
@since Frama-C+dev*)
@since Frama-C+dev
*)
val
checkCast
:
val
checkCast
:
?
context
:
qualifier_check_context
->
?
context
:
qualifier_check_context
->
?
nullptr_cast
:
bool
->
?
nullptr_cast
:
bool
->
...
@@ -1201,14 +1204,13 @@ val checkCast:
...
@@ -1201,14 +1204,13 @@ val checkCast:
(** Generic version of {!Cil.mkCastT}.
(** Generic version of {!Cil.mkCastT}.
Construct a cast when having the old type of the expression.
Construct a cast when having the old type of the expression.
[fromsource] is [false] (default) if the cast is not from the source.
[fromsource] is [false] (default) if the cast is not present in the source
code.
If [check] is [true] (default), we check that the cast is valid,
If [check] is [true] (default), we check that the cast is valid,
fail
if the cast is invalid.
emitting an error or warning
if the cast is invalid.
If the new type is the same as the old type, then no cast is added,
If the new type is the same as the old type, then no cast is added,
unless [force] is [true] (default is [false]).
unless [force] is [true] (default is [false]).
Casting from [oldt] to [newt].
Cast from [oldt] to [newt], returning the new type and the new expression.
Take the expression as argument and can modify it.
Return the new type and the new expression.
@since Frama-C+dev
@since Frama-C+dev
*)
*)
...
@@ -1218,13 +1220,13 @@ val mkCastTGen: ?check:bool -> ?context:qualifier_check_context ->
...
@@ -1218,13 +1220,13 @@ val mkCastTGen: ?check:bool -> ?context:qualifier_check_context ->
(** Construct a cast when having the old type of the expression. If the new
(** Construct a cast when having the old type of the expression. If the new
type is the same as the old type, then no cast is added, unless [force]
type is the same as the old type, then no cast is added, unless [force]
is [true] (default is [false]).
is [true] (default is [false]).
Fail if
the cast is invalid.
Emit an error or warning if [check] is true and
the cast is invalid.
@before 23.0-Vanadium different order of arguments.
@before 23.0-Vanadium different order of arguments.
@before Frama-C+dev no [check] argument, it was always [false].
@before Frama-C+dev no [check] argument, it was always [false].
*)
*)
val
mkCastT
:
?
check
:
bool
->
?
force
:
bool
->
oldt
:
typ
->
newt
:
typ
->
exp
->
exp
val
mkCastT
:
?
check
:
bool
->
?
force
:
bool
->
oldt
:
typ
->
newt
:
typ
->
exp
->
exp
(** Like {!Cil.mkCastT} but uses typeOf to get [oldt]
(** Like {!Cil.mkCastT}
,
but uses
[
typeOf
]
to get [oldt]
.
@before 23.0-Vanadium different order of arguments.
@before 23.0-Vanadium different order of arguments.
@before Frama-C+dev no [check] argument, it was always [false].
@before Frama-C+dev no [check] argument, it was always [false].
*)
*)
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment