Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
992cfa5e
Commit
992cfa5e
authored
Jul 15, 2019
by
Allan Blanchard
Browse files
Replaces calls to deprecated functions related to Visitor_behavior
parent
f20e009f
Changes
11
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/at_with_lscope.ml
View file @
992cfa5e
...
...
@@ -215,7 +215,7 @@ let put_block_at_label env block label =
end
in
let
bhv
=
Env
.
get_behavior
env
in
ignore
(
Visitor
.
visitFramacStmt
o
(
Cil
.
g
et
_
stmt
bhv
stmt
));
ignore
(
Visitor
.
visitFramacStmt
o
(
Visitor_behavior
.
G
et
.
stmt
bhv
stmt
));
!
env_ref
let
to_exp
~
loc
kf
env
pot
label
=
...
...
src/plugins/e-acsl/dup_functions.ml
View file @
992cfa5e
...
...
@@ -65,7 +65,7 @@ let dup_funspec tbl bhv spec =
if
Global
.
mem_logic_info
li
then
Cil
.
ChangeDoChildrenPost
({
li
with
l_var_info
=
li
.
l_var_info
}
(* force a copy *)
,
Cil
.
g
et
_
logic_info
bhv
)
Visitor_behavior
.
G
et
.
logic_info
bhv
)
else
Cil
.
JustCopy
...
...
@@ -73,8 +73,8 @@ let dup_funspec tbl bhv spec =
Cil
.
DoChildrenPost
(
function
(* no way to directly visit fieldinfo and model_info uses *)
|
TField
(
fi
,
off
)
->
TField
(
Cil
.
g
et
_
fieldinfo
bhv
fi
,
off
)
|
TModel
(
mi
,
off
)
->
TModel
(
Cil
.
g
et
_
model_info
bhv
mi
,
off
)
|
TField
(
fi
,
off
)
->
TField
(
Visitor_behavior
.
G
et
.
fieldinfo
bhv
fi
,
off
)
|
TModel
(
mi
,
off
)
->
TModel
(
Visitor_behavior
.
G
et
.
model_info
bhv
mi
,
off
)
|
off
->
off
)
method
!
vlogic_var_use
orig_lvi
=
...
...
@@ -91,7 +91,7 @@ let dup_funspec tbl bhv spec =
Cil
.
ChangeDoChildrenPost
({
orig_lvi
with
lv_id
=
orig_lvi
.
lv_id
}
(* force a copy *)
,
fun
lvi
->
(* using [
Cil.g
et
_
logic_var bhv lvi] is correct only because the
(* using [
Visitor_behavior.G
et
.
logic_var bhv lvi] is correct only because the
lv_id used to compare the lvi does not change between the
original one and this copy *)
try
...
...
@@ -105,7 +105,7 @@ let dup_funspec tbl bhv spec =
lvi
with
Not_found
->
assert
vi
.
vglob
;
Cil
.
g
et
_
logic_var
bhv
lvi
)
Visitor_behavior
.
G
et
.
logic_var
bhv
lvi
)
method
!
videntified_term
_
=
Cil
.
DoChildrenPost
Logic_const
.
refresh_identified_term
...
...
@@ -192,7 +192,7 @@ let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
(* remove the specs attached to the previous kf iff it is a definition:
it is necessary to keep stable the number of annotations in order to get
[Keep_status] working fine. *)
let
kf
=
Cil
.
g
et
_
kernel_function
bhv
kf
in
let
kf
=
Visitor_behavior
.
G
et
.
kernel_function
bhv
kf
in
if
Kernel_function
.
is_definition
kf
then
begin
Queue
.
add
(
fun
()
->
...
...
@@ -351,14 +351,14 @@ if there are memory-related annotations.@]"
end
;
let
kf
=
try
Globals
.
Functions
.
get
(
Cil
.
g
et_orig
inal_
varinfo
self
#
behavior
vi
)
Globals
.
Functions
.
get
(
Visitor_behavior
.
G
et_orig
.
varinfo
self
#
behavior
vi
)
with
Not_found
->
Options
.
fatal
"unknown function `%s' while trying to duplicate it"
vi
.
vname
in
let
spec
=
Annotations
.
funspec
~
populate
:
false
kf
in
let
vi_bhv
=
Cil
.
g
et
_
varinfo
self
#
behavior
vi
in
let
vi_bhv
=
Visitor_behavior
.
G
et
.
varinfo
self
#
behavior
vi
in
let
new_g
,
new_decl
=
dup_global
loc
...
...
src/plugins/e-acsl/env.ml
View file @
992cfa5e
...
...
@@ -115,7 +115,7 @@ let empty_local_env =
rte
=
true
}
let
dummy
=
{
visitor
=
new
Visitor
.
generic_frama_c_visitor
(
Cil
.
inplace
_visit
()
);
{
visitor
=
new
Visitor
.
generic_frama_c_visitor
(
Visitor_behavior
.
inplace
()
);
lscope
=
Lscope
.
empty
;
lscope_reset
=
true
;
annotation_kind
=
Misc
.
Assertion
;
...
...
@@ -150,7 +150,7 @@ let current_kf env =
let
v
=
env
.
visitor
in
match
v
#
current_kf
with
|
None
->
None
|
Some
kf
->
Some
(
Cil
.
g
et
_
kernel_function
v
#
behavior
kf
)
|
Some
kf
->
Some
(
Visitor_behavior
.
G
et
.
kernel_function
v
#
behavior
kf
)
let
set_current_kf
env
kf
=
let
v
=
env
.
visitor
in
...
...
src/plugins/e-acsl/env.mli
View file @
992cfa5e
...
...
@@ -125,7 +125,7 @@ val get_generated_variables: t -> (varinfo * localized_scope) list
(** All the new variables local to the visited function. *)
val
get_visitor
:
t
->
Visitor
.
generic_frama_c_visitor
val
get_behavior
:
t
->
Cil
.
v
isitor_behavior
val
get_behavior
:
t
->
V
isitor_behavior
.
t
val
current_kf
:
t
->
kernel_function
option
(** Kernel function currently visited in the new project. *)
...
...
src/plugins/e-acsl/label.ml
View file @
992cfa5e
...
...
@@ -44,12 +44,12 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
|
_
::
_
->
old
.
labels
<-
[]
;
new_stmt
.
labels
<-
labels
@
new_stmt
.
labels
;
let
old
=
Cil
.
g
et_orig
inal_
stmt
vis
#
behavior
old
in
let
old
=
Visitor_behavior
.
G
et_orig
.
stmt
vis
#
behavior
old
in
Labeled_stmts
.
add
old
new_stmt
;
(* update the gotos of the function jumping to one of the labels *)
let
o
orig_stmt
=
object
inherit
Visitor
.
frama_c_inplace
(* invariant of this method: [s =
Cil.m
emo
_
stmt vis#behavior orig_stmt] *)
(* invariant of this method: [s =
Visitor_behavior.M
emo
.
stmt vis#behavior orig_stmt] *)
method
!
vstmt_aux
s
=
match
s
.
skind
,
orig_stmt
.
skind
with
|
Goto
(
s_ref
,
_
)
,
Goto
(
orig_ref
,
_
)
->
if
Cil_datatype
.
Stmt
.
equal
!
orig_ref
old
&&
s_ref
!=
orig_ref
then
...
...
@@ -65,7 +65,7 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
end
in
let
f
=
Extlib
.
the
vis
#
current_func
in
let
mv_labels
s
=
ignore
(
Visitor
.
visitFramacStmt
(
o
s
)
(
Cil
.
m
emo
_
stmt
vis
#
behavior
s
))
ignore
(
Visitor
.
visitFramacStmt
(
o
s
)
(
Visitor_behavior
.
M
emo
.
stmt
vis
#
behavior
s
))
in
List
.
iter
mv_labels
f
.
sallstmts
...
...
src/plugins/e-acsl/logic_functions.ml
View file @
992cfa5e
...
...
@@ -227,7 +227,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
li
.
l_profile
;
Env
.
set_current_kf
env
(
Cil
.
g
et_orig
inal_
kernel_function
(
Env
.
get_behavior
env
)
old_kf
)
(
Visitor_behavior
.
G
et_orig
.
kernel_function
(
Env
.
get_behavior
env
)
old_kf
)
in
vi
,
kf
,
gen_body
...
...
src/plugins/e-acsl/mmodel_analysis.ml
View file @
992cfa5e
...
...
@@ -713,7 +713,7 @@ if there are memory-related annotations.@]"
let
must_model_vi
bhv
?
kf
?
stmt
vi
=
let
vi
=
match
bhv
with
|
None
->
vi
|
Some
bhv
->
Cil
.
g
et_orig
inal_
varinfo
bhv
vi
|
Some
bhv
->
Visitor_behavior
.
G
et_orig
.
varinfo
bhv
vi
in
let
_kf
=
match
kf
,
stmt
with
|
None
,
None
|
Some
_
,
_
->
kf
...
...
src/plugins/e-acsl/mmodel_analysis.mli
View file @
992cfa5e
...
...
@@ -31,18 +31,18 @@ val reset: unit -> unit
val
use_model
:
unit
->
bool
(** Is one variable monitored (at least)? *)
val
must_model_vi
:
?
bhv
:
Cil
.
v
isitor_behavior
->
?
kf
:
kernel_function
val
must_model_vi
:
?
bhv
:
V
isitor_behavior
.
t
->
?
kf
:
kernel_function
->
?
stmt
:
stmt
->
varinfo
->
bool
(** [must_model_vi ?kf ?stmt vi] returns [true] if the varinfo [vi] at the given
[stmt] in the given function [kf] must be tracked by the memory model
library. If behavior [bhv] is specified then assume that [vi] is part
of the new project generated by the given copy behavior [bhv] *)
val
must_model_lval
:
?
bhv
:
Cil
.
v
isitor_behavior
->
?
kf
:
kernel_function
val
must_model_lval
:
?
bhv
:
V
isitor_behavior
.
t
->
?
kf
:
kernel_function
->
?
stmt
:
stmt
->
lval
->
bool
(** Same as {!must_model_vi}, for left-values *)
val
must_model_exp
:
?
bhv
:
Cil
.
v
isitor_behavior
->
?
kf
:
kernel_function
val
must_model_exp
:
?
bhv
:
V
isitor_behavior
.
t
->
?
kf
:
kernel_function
->
?
stmt
:
stmt
->
exp
->
bool
(** Same as {!must_model_vi}, for expressions *)
...
...
src/plugins/e-acsl/temporal.ml
View file @
992cfa5e
...
...
@@ -487,7 +487,7 @@ let mk_global_init ~loc vi off init env =
in
(* The input [vi] is from the old project, so get the corresponding variable
from the new one, otherwise AST integrity is violated *)
let
vi
=
Cil
.
g
et
_
varinfo
(
Env
.
get_behavior
env
)
vi
in
let
vi
=
Visitor_behavior
.
G
et
.
varinfo
(
Env
.
get_behavior
env
)
vi
in
let
lv
=
Var
vi
,
off
in
mk_stmt_from_assign
loc
lv
exp
(* }}} *)
...
...
@@ -504,7 +504,7 @@ let handle_function_parameters kf env =
if
is_enabled
()
then
let
env
,
_
=
List
.
fold_left
(
fun
(
env
,
index
)
param
->
let
param
=
Cil
.
g
et
_
varinfo
(
Env
.
get_behavior
env
)
param
in
let
param
=
Visitor_behavior
.
G
et
.
varinfo
(
Env
.
get_behavior
env
)
param
in
let
env
=
if
Mmodel_analysis
.
must_model_vi
~
kf
param
then
track_argument
param
index
env
...
...
src/plugins/e-acsl/translate.ml
View file @
992cfa5e
...
...
@@ -226,7 +226,7 @@ let cast_integer_to_float lty lty_t e =
let
rec
thost_to_host
kf
env
th
=
match
th
with
|
TVar
{
lv_origin
=
Some
v
}
->
Var
(
Cil
.
g
et
_
varinfo
(
Env
.
get_behavior
env
)
v
)
,
env
,
v
.
vname
Var
(
Visitor_behavior
.
G
et
.
varinfo
(
Env
.
get_behavior
env
)
v
)
,
env
,
v
.
vname
|
TVar
({
lv_origin
=
None
}
as
logic_v
)
->
Var
(
Env
.
Logic_binding
.
get
env
logic_v
)
,
env
,
logic_v
.
lv_name
|
TResult
_typ
->
...
...
@@ -234,7 +234,7 @@ let rec thost_to_host kf env th = match th with
let
kf
=
Extlib
.
the
vis
#
current_kf
in
let
lhost
=
Misc
.
result_lhost
kf
in
(
match
lhost
with
|
Var
v
->
Var
(
Cil
.
g
et
_
varinfo
(
Env
.
get_behavior
env
)
v
)
,
env
,
"result"
|
Var
v
->
Var
(
Visitor_behavior
.
G
et
.
varinfo
(
Env
.
get_behavior
env
)
v
)
,
env
,
"result"
|
_
->
assert
false
)
|
TMem
t
->
let
e
,
env
=
term_to_exp
kf
env
t
in
...
...
@@ -646,7 +646,7 @@ and at_to_exp_no_lscope env t_opt label e =
end
in
let
bhv
=
Env
.
get_behavior
new_env
in
ignore
(
Visitor
.
visitFramacStmt
o
(
Cil
.
g
et
_
stmt
bhv
stmt
));
ignore
(
Visitor
.
visitFramacStmt
o
(
Visitor_behavior
.
G
et
.
stmt
bhv
stmt
));
res
,
!
env_ref
,
false
and
env_of_li
li
kf
env
loc
=
...
...
src/plugins/e-acsl/visit.ml
View file @
992cfa5e
...
...
@@ -54,7 +54,7 @@ end = struct
fold
(
fun
vi
env
->
if
Mmodel_analysis
.
must_model_vi
~
kf
vi
then
let
vi
=
Cil
.
g
et
_
varinfo
(
Env
.
get_behavior
env
)
vi
in
let
vi
=
Visitor_behavior
.
G
et
.
varinfo
(
Env
.
get_behavior
env
)
vi
in
Env
.
add_stmt
?
before
env
(
mk_stmt
vi
)
else
env
)
...
...
@@ -144,7 +144,7 @@ struct
let
exp_in_depth
env
e
=
let
env_ref
=
ref
env
in
let
o
=
object
inherit
Cil
.
genericCilVisitor
(
Cil
.
copy_visit
(
Project
.
current
()
))
inherit
Cil
.
genericCilVisitor
(
Visitor_behavior
.
copy
(
Project
.
current
()
))
method
!
vexpr
e
=
match
e
.
enode
with
(* the guard below could be optimized: if no annotation **depends on this
string**, then it is not required to monitor it.
...
...
@@ -172,11 +172,11 @@ module Global_observer: sig
val
add_initializer
:
varinfo
->
offset
->
init
->
unit
(* add the initializer for the given observed variable *)
val
mk_init
:
Cil
.
v
isitor_behavior
->
Env
.
t
->
varinfo
*
fundec
*
Env
.
t
val
mk_init
:
V
isitor_behavior
.
t
->
Env
.
t
->
varinfo
*
fundec
*
Env
.
t
(* generates a new C function containing the observers for global variable
declaration and initialization *)
val
mk_delete
:
Cil
.
v
isitor_behavior
->
stmt
list
->
stmt
list
val
mk_delete
:
V
isitor_behavior
.
t
->
stmt
list
->
stmt
list
(* generates the observers for global variable de-allocation *)
end
=
struct
...
...
@@ -254,7 +254,7 @@ end = struct
let
env
,
stmts
=
Varinfo
.
Hashtbl
.
fold_sorted
(
fun
old_vi
l
stmts
->
let
new_vi
=
Cil
.
g
et
_
varinfo
bhv
old_vi
in
let
new_vi
=
Visitor_behavior
.
G
et
.
varinfo
bhv
old_vi
in
List
.
fold_left
(
fun
(
env
,
stmts
)
(
off
,
init
)
->
let
env
=
literal_in_initializer
env
init
in
...
...
@@ -269,7 +269,7 @@ end = struct
let
stmts
=
Varinfo
.
Hashtbl
.
fold_sorted
(
fun
old_vi
_
stmts
->
let
new_vi
=
Cil
.
g
et
_
varinfo
bhv
old_vi
in
let
new_vi
=
Visitor_behavior
.
G
et
.
varinfo
bhv
old_vi
in
(* a global is both allocated and initialized *)
Misc
.
mk_store_stmt
new_vi
::
Misc
.
mk_initialize
~
loc
:
Location
.
unknown
(
Cil
.
var
new_vi
)
...
...
@@ -329,7 +329,7 @@ end = struct
let
mk_delete
bhv
stmts
=
Varinfo
.
Hashtbl
.
fold_sorted
(
fun
old_vi
_l
acc
->
let
new_vi
=
Cil
.
g
et
_
varinfo
bhv
old_vi
in
let
new_vi
=
Visitor_behavior
.
G
et
.
varinfo
bhv
old_vi
in
Misc
.
mk_delete_stmt
new_vi
::
acc
)
tbl
stmts
...
...
@@ -340,7 +340,7 @@ end
class
e_acsl_visitor
prj
generate
=
object
(
self
)
inherit
Visitor
.
generic_frama_c_visitor
(
if
generate
then
Cil
.
copy_visit
prj
else
Cil
.
inplace
_visit
()
)
(
if
generate
then
Visitor_behavior
.
copy
prj
else
Visitor_behavior
.
inplace
()
)
val
mutable
main_fct
=
None
(* fundec of the main entry point, in the new project [prj].
...
...
@@ -472,7 +472,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if
generate
then
Cil
.
JustCopyPost
(
fun
l
->
let
new_vi
=
Cil
.
g
et
_
varinfo
self
#
behavior
vi
in
let
new_vi
=
Visitor_behavior
.
G
et
.
varinfo
self
#
behavior
vi
in
if
Misc
.
is_library_loc
vi
.
vdecl
then
Misc
.
register_library_function
new_vi
;
if
Builtins
.
mem
vi
.
vname
then
Builtins
.
update
vi
.
vname
new_vi
;
...
...
@@ -514,7 +514,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* Make a unique mapping for each global variable omitting initializers.
Initializers (used to capture literal strings) are added to
[global_vars] via the [vinit] visitor method (see comments below). *)
Global_observer
.
add
(
Cil
.
g
et_orig
inal_
varinfo
self
#
behavior
vi
)
Global_observer
.
add
(
Visitor_behavior
.
G
et_orig
.
varinfo
self
#
behavior
vi
)
|
_
->
()
);
if
generate
then
Cil
.
DoChildrenPost
(
fun
g
->
List
.
iter
do_it
g
;
g
)
else
Cil
.
DoChildren
...
...
@@ -550,7 +550,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
method
!
vvdec
vi
=
(
try
let
old_vi
=
Cil
.
g
et_orig
inal_
varinfo
self
#
behavior
vi
in
let
old_vi
=
Visitor_behavior
.
G
et_orig
.
varinfo
self
#
behavior
vi
in
let
old_kf
=
Globals
.
Functions
.
get
old_vi
in
funspec
:=
Cil
.
visitCilFunspec
...
...
@@ -611,12 +611,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
try
Kernel_function
.
find_return
old_kf
with
Kernel_function
.
No_Statement
->
assert
false
in
Stmt
.
equal
stmt
(
Cil
.
g
et
_
stmt
self
#
behavior
old_ret
)
Stmt
.
equal
stmt
(
Visitor_behavior
.
G
et
.
stmt
self
#
behavior
old_ret
)
method
private
is_first_stmt
old_kf
stmt
=
try
Stmt
.
equal
(
Cil
.
g
et_orig
inal_
stmt
self
#
behavior
stmt
)
(
Visitor_behavior
.
G
et_orig
.
stmt
self
#
behavior
stmt
)
(
Kernel_function
.
find_first_stmt
old_kf
)
with
Kernel_function
.
No_Statement
->
assert
false
...
...
@@ -674,7 +674,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Project
.
on
prj
(
Translate
.
translate_pre_code_annotation
kf
env
)
a
in
env
,
a
::
new_annots
)
(
Cil
.
g
et_orig
inal_
stmt
self
#
behavior
stmt
)
(
Visitor_behavior
.
G
et_orig
.
stmt
self
#
behavior
stmt
)
(
env
,
[]
)
else
env
,
[]
...
...
@@ -722,9 +722,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let
new_stmt
,
env
,
must_mv
=
Loops
.
preserve_invariant
prj
env
kf
stmt
in
let
orig
=
Cil
.
g
et_orig
inal_
stmt
self
#
behavior
stmt
in
Cil
.
s
et_orig
_
stmt
self
#
behavior
new_stmt
orig
;
Cil
.
s
et
_
stmt
self
#
behavior
orig
new_stmt
;
let
orig
=
Visitor_behavior
.
G
et_orig
.
stmt
self
#
behavior
stmt
in
Visitor_behavior
.
S
et_orig
.
stmt
self
#
behavior
new_stmt
orig
;
Visitor_behavior
.
S
et
.
stmt
self
#
behavior
orig
new_stmt
;
new_stmt
,
env
,
must_mv
else
stmt
,
env
,
false
...
...
@@ -835,9 +835,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if
not
(
Cil_datatype
.
Stmt
.
equal
new_stmt
res
)
then
E_acsl_label
.
move
(
self
:>
Visitor
.
generic_frama_c_visitor
)
new_stmt
res
;
let
orig
=
Cil
.
g
et_orig
inal_
stmt
self
#
behavior
stmt
in
Cil
.
s
et
_
stmt
self
#
behavior
orig
res
;
Cil
.
s
et_orig
_
stmt
self
#
behavior
res
orig
;
let
orig
=
Visitor_behavior
.
G
et_orig
.
stmt
self
#
behavior
stmt
in
Visitor_behavior
.
S
et
.
stmt
self
#
behavior
orig
res
;
Visitor_behavior
.
S
et_orig
.
stmt
self
#
behavior
res
orig
;
res
,
env
end
else
stmt
,
env
...
...
@@ -999,7 +999,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
List
.
fold_left
(
fun
acc
vi
->
if
Mmodel_analysis
.
must_model_vi
vi
&&
not
vi
.
vdefined
then
let
vi
=
Cil
.
g
et
_
varinfo
self
#
behavior
vi
in
let
vi
=
Visitor_behavior
.
G
et
.
varinfo
self
#
behavior
vi
in
Misc
.
mk_store_stmt
vi
::
acc
else
acc
)
new_blk
.
bstmts
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment