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
8820f825
Commit
8820f825
authored
2 months ago
by
Jan Rochel
Browse files
Options
Downloads
Patches
Plain Diff
[alias] adapt comments for better odoc rendering
parent
29383cc1
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/alias/src/API.mli
+21
-21
21 additions, 21 deletions
src/plugins/alias/src/API.mli
with
21 additions
and
21 deletions
src/plugins/alias/src/API.mli
+
21
−
21
View file @
8820f825
...
@@ -179,14 +179,14 @@ module Abstract_state : sig
...
@@ -179,14 +179,14 @@ module Abstract_state : sig
val
get_vars
:
v
->
t
->
VarSet
.
t
val
get_vars
:
v
->
t
->
VarSet
.
t
(** set of lvals which can be used to refered to the given vertex
(** set of lvals which can be used to refered to the given vertex
Example graph:
{a} → {b}
-t→
{c}
Example graph:
<a> → <b>
-t→
<c>
The lvals corresponding to the rightmost vertex are
{
c, b.t, a->t
}
:
The lvals corresponding to the rightmost vertex are
<
c, b.t, a->t
>
:
- c: simply refers to a variable associated with the vertex.
- c: simply refers to a variable associated with the vertex.
- b.t: starting from the second vertex one can follow a field-edge
- b.t: starting from the second vertex one can follow a field-edge
labelled
"t"
to come upon the rightmost vertex.
labelled
[t]
to come upon the rightmost vertex.
- a->t: Following a pointer edge from the leftmost vertex one obtains
- a->t: Following a pointer edge from the leftmost vertex one obtains
"
*a
"
. Following the
"t"
field-edge one arrives at the rightmost
[
*a
]
. Following the
[t]
field-edge one arrives at the rightmost
vertex, corresponding to
"
( *a ).t
"
or
"
a->t
"
. *)
vertex, corresponding to
[
( *a ).t
]
or
[
a->t
]
. *)
val
get_lval_set
:
v
->
t
->
LSet
.
t
val
get_lval_set
:
v
->
t
->
LSet
.
t
(** pretty printer; debug=true prints the graph, debug = false only
(** pretty printer; debug=true prints the graph, debug = false only
...
@@ -209,9 +209,9 @@ module Abstract_state : sig
...
@@ -209,9 +209,9 @@ module Abstract_state : sig
(** Note: You probably want to use [alias_lvals] instead of this function.
(** Note: You probably want to use [alias_lvals] instead of this function.
Combining [find_vertex] with [get_lval_set], this function yields all the
Combining [find_vertex] with [get_lval_set], this function yields all the
different ways the vertex containing the given lval can be referred to.
different ways the vertex containing the given lval can be referred to.
Example:
{a}
→
{
b,c
}
Example:
<a>
→
<
b,c
>
If
"a"
points to
"b"
, then the vertex containing
"b"
can be referred to not
If
[a]
points to
[b]
, then the vertex containing
[b]
can be referred to not
only by
"b"
but also by
"c"
or
"
*a
"
.
only by
[b]
but also by
[c]
or
[
*a
]
.
Does not raise an exception but returns an empty set if the lval is not in
Does not raise an exception but returns an empty set if the lval is not in
the graph. *)
the graph. *)
val
find_synonyms
:
lval
->
t
->
LSet
.
t
val
find_synonyms
:
lval
->
t
->
LSet
.
t
...
@@ -221,10 +221,10 @@ module Abstract_state : sig
...
@@ -221,10 +221,10 @@ module Abstract_state : sig
- variables from a neighbouring vertex, i.e. a vertex that shares a
- variables from a neighbouring vertex, i.e. a vertex that shares a
successor with the vertex of [lv].
successor with the vertex of [lv].
Example:
{
a,b
}
→
{c} ← {d} ← {e}
Example:
<
a,b
>
→
<c> ← <d> ← <e>
The aliases of
"a"
are
{
a,b,d
}
:
The aliases of
[a]
are
<
a,b,d
>
:
-
"b"
shares a vertex with
"a"
-
[b]
shares a vertex with
[a]
-
"d"
is in a neighbouring vertex, pointing to
"c"
as does
{
a,b
}
*)
-
[d]
is in a neighbouring vertex, pointing to
[c]
as does
<
a,b
>
*)
val
alias_vars
:
lval
->
t
->
VarSet
.
t
val
alias_vars
:
lval
->
t
->
VarSet
.
t
val
find_aliases
:
lval
->
t
->
LSet
.
t
val
find_aliases
:
lval
->
t
->
LSet
.
t
...
@@ -236,11 +236,11 @@ module Abstract_state : sig
...
@@ -236,11 +236,11 @@ module Abstract_state : sig
successor with the vertex of [lv].
successor with the vertex of [lv].
- lvals reconstructed from the variables from the two previous sets.
- lvals reconstructed from the variables from the two previous sets.
Example:
{
a,b
}
→
{c} ← {d} ← {e}
Example:
<
a,b
>
→
<c> ← <d> ← <e>
The aliases of
"a"
are
{
a,b,d,*e
}
:
The aliases of
[a]
are
<
a,b,d,*e
>
:
-
"b"
shares a vertex with
"a"
-
[b]
shares a vertex with
[a]
-
"d"
is in a neighbouring vertex, as it shares a successor with
{
a,b
}
-
[d]
is in a neighbouring vertex, as it shares a successor with
<
a,b
>
- *e is obtained by following backwards the pointer edge from
{d}
to
{e}
. *)
-
[
*e
]
is obtained by following backwards the pointer edge from
<d>
to
<e>
. *)
val
alias_lvals
:
lval
->
t
->
LSet
.
t
val
alias_lvals
:
lval
->
t
->
LSet
.
t
val
find_all_aliases
:
lval
->
t
->
LSet
.
t
val
find_all_aliases
:
lval
->
t
->
LSet
.
t
...
@@ -258,14 +258,14 @@ module Abstract_state : sig
...
@@ -258,14 +258,14 @@ module Abstract_state : sig
[
@@
alert
deprecated
"Use points_to_vars or points_to_lvals instead!"
]
[
@@
alert
deprecated
"Use points_to_vars or points_to_lvals instead!"
]
(** all the alias sets of a given state
(** all the alias sets of a given state
Example:
{
a,b
}
→
{c} ← {d}
←
{
e,f
}
Example:
<
a,b
>
→
<c> ← <d>
←
<
e,f
>
The aliases sets are
{{
a,b,d
}
,
{
e,f
}}
The aliases sets are
<<
a,b,d
>
,
<
e,f
>>
*)
*)
val
alias_sets_vars
:
t
->
VarSet
.
t
list
val
alias_sets_vars
:
t
->
VarSet
.
t
list
(** all the alias sets of a given state, including reconstructed lvals
(** all the alias sets of a given state, including reconstructed lvals
Example:
{
a,b
}
→
{c} ← {d}
←
{
e,f
}
Example:
<
a,b
>
→
<c> ← <d>
←
<
e,f
>
The aliases sets are
{{
a,b,d,*e,*f
}
,
{
e,f
}}
The aliases sets are
<<
a,b,d,*e,*f
>
,
<
e,f
>>
*)
*)
val
alias_sets_lvals
:
t
->
LSet
.
t
list
val
alias_sets_lvals
:
t
->
LSet
.
t
list
...
...
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