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
60bc2c1e
Commit
60bc2c1e
authored
6 years ago
by
Patrick Baudin
Browse files
Options
Downloads
Patches
Plain Diff
[wp] adds some comments
parent
496ae212
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/plugins/wp/MemTyped.ml
+20
-13
20 additions, 13 deletions
src/plugins/wp/MemTyped.ml
with
20 additions
and
13 deletions
src/plugins/wp/MemTyped.ml
+
20
−
13
View file @
60bc2c1e
...
...
@@ -1057,7 +1057,14 @@ let block_length sigma obj l =
(* --- Cast --- *)
(* -------------------------------------------------------------------------- *)
module
Layout
=
module
Layout
:
sig
val
pretty
:
Format
.
formatter
->
c_object
->
unit
val
fits
:
dst
:
c_object
->
src
:
c_object
->
bool
(* returns [true] in these cases:
- [dst] fits into [src]
- [dst] equals [src] *)
end
=
struct
type
atom
=
P
of
typ
|
I
of
c_int
|
F
of
c_float
...
...
@@ -1144,10 +1151,10 @@ struct
let
add_array
ly
n
w
=
if
n
=
1
then
ly
@
w
else
add_many
ly
n
w
let
rec
compare
l1
l2
=
match
l1
,
l2
with
|
[]
,
[]
->
Equal
|
[]
,
_
->
Fit
let
rec
compare
~
dst
~
src
=
match
dst
,
src
with
|
[]
,
[]
->
Equal
(* src = dst *)
|
[]
,
_
->
Fit
(* exists obj ; src = dst concat obj *)
|
_
,
[]
->
Mismatch
|
p
::
w1
,
q
::
w2
->
match
p
,
q
with
...
...
@@ -1166,7 +1173,7 @@ struct
else
Mismatch
|
Arr
(
u
,
n
)
,
Arr
(
v
,
m
)
->
begin
match
compare
u
v
with
match
compare
~
dst
:
u
~
src
:
v
with
|
Mismatch
->
Mismatch
|
Fit
->
Mismatch
|
Equal
->
...
...
@@ -1181,18 +1188,18 @@ struct
compare
w1
w2
end
|
Arr
(
v
,
n
)
,
Str
_
->
compare
(
v
@
add_array
v
(
n
-
1
)
w1
)
l2
compare
~
dst
:
(
v
@
add_array
v
(
n
-
1
)
w1
)
~
src
|
Str
_
,
Arr
(
v
,
n
)
->
compare
l1
(
v
@
add_array
v
(
n
-
1
)
w2
)
compare
~
dst
~
src
:
(
v
@
add_array
v
(
n
-
1
)
w2
)
let
fits
obj1
obj2
=
match
obj1
,
obj2
with
let
fits
~
dst
~
src
=
match
dst
,
src
with
|
C_int
i1
,
C_int
i2
->
i1
=
i2
|
C_float
f1
,
C_float
f2
->
f1
=
f2
|
C_comp
c
,
C_comp
d
when
Compinfo
.
equal
c
d
->
true
|
C_pointer
_
,
C_pointer
_
->
true
|
_
->
match
compare
(
layout
obj1
)
(
layout
obj2
)
with
match
compare
~
dst
:
(
layout
dst
)
~
src
:
(
layout
src
)
with
|
Equal
|
Fit
->
true
|
Mismatch
->
false
...
...
@@ -1223,10 +1230,10 @@ let cast s l =
match
Context
.
get
pointer
with
|
NoCast
->
Warning
.
error
~
source
:
"Typed Model"
"%a"
pp_mismatch
s
|
Fits
->
if
Layout
.
fits
s
.
post
s
.
pre
then
l
else
if
Layout
.
fits
~
dst
:
s
.
post
~
src
:
s
.
pre
then
l
else
Warning
.
error
~
source
:
"Typed Model"
"%a"
pp_mismatch
s
|
Unsafe
->
if
not
(
Layout
.
fits
s
.
post
s
.
pre
)
then
if
not
(
Layout
.
fits
~
dst
:
s
.
post
~
src
:
s
.
pre
)
then
Warning
.
emit
~
severe
:
false
~
source
:
"Typed Model"
~
effect
:
"Keep pointer value"
"%a"
pp_mismatch
s
;
l
...
...
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