Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
00ff948a
Commit
00ff948a
authored
Dec 20, 2019
by
Loïc Correnson
Browse files
Merge branch 'master' into feature/server/load-request
# Conflicts: # src/plugins/server/kernel_ast.ml
parents
e0c30c56
574af106
Changes
251
Hide whitespace changes
Inline
Side-by-side
.Makefile.lint
View file @
00ff948a
...
...
@@ -378,43 +378,10 @@ ML_LINT_KO+=src/plugins/variadic/standard.ml
ML_LINT_KO+=src/plugins/variadic/translate.ml
ML_LINT_KO+=src/plugins/variadic/va_build.ml
ML_LINT_KO+=src/plugins/variadic/va_types.mli
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/exit_points.ml
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/exit_points.mli
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/interval.ml
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/literal_strings.ml
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/lscope.ml
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/lscope.mli
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/rte.ml
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/typing.ml
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/typing.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/env.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/env.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/gmp.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/label.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/logic_functions.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/loops.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/loops.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/mmodel_translate.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/quantif.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/quantif.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/rational.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/translate.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/translate.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/visit.ml
ML_LINT_KO+=src/plugins/e-acsl/src/libraries/builtins.ml
ML_LINT_KO+=src/plugins/e-acsl/src/libraries/error.ml
ML_LINT_KO+=src/plugins/e-acsl/src/libraries/error.mli
ML_LINT_KO+=src/plugins/e-acsl/src/libraries/functions.ml
ML_LINT_KO+=src/plugins/e-acsl/src/libraries/functions.mli
ML_LINT_KO+=src/plugins/e-acsl/src/libraries/misc.ml
ML_LINT_KO+=src/plugins/e-acsl/src/libraries/misc.mli
ML_LINT_KO+=src/plugins/e-acsl/src/main.ml
ML_LINT_KO+=src/plugins/e-acsl/src/options.ml
ML_LINT_KO+=src/plugins/e-acsl/src/project_initializer/dup_functions.ml
ML_LINT_KO+=src/plugins/e-acsl/src/project_initializer/keep_status.ml
doc/pandoc/style.css
View file @
00ff948a
...
...
@@ -61,7 +61,7 @@ body {
max-width
:
8cm
;
height
:
100%
;
padding
:
0cm
0.5cm
0cm
0.5cm
;
background
:
#
888
;
background
:
#
eee
;
}
#CONTENT
{
...
...
@@ -85,6 +85,10 @@ body {
font-size
:
smaller
;
}
#NAVIGATION
a
{
color
:
black
;
}
#NAVIGATION
a
.root
{
display
:
block
;
font-family
:
"Optima"
,
"Verdana"
,
"Arial"
,
sans
;
...
...
@@ -104,14 +108,6 @@ body {
background-color
:
darkorange
;
}
#NAVIGATION
a
{
color
:
white
;
}
#NAVIGATION
code
{
color
:
black
;
}
#NAVIGATION
ul
{
width
:
6cm
;
}
...
...
@@ -120,7 +116,6 @@ body {
margin-left
:
0px
;
padding-top
:
2px
;
padding-bottom
:
2px
;
background-color
:
darkgrey
;
}
/* -------------------------------------------------------------------------- */
...
...
@@ -143,13 +138,11 @@ h2 {
margin-top
:
5mm
;
margin-bottom
:
2mm
;
border-bottom
:
solid
thin
darkred
;
color
:
darkred
;
}
h3
{
width
:
17cm
;
font-family
:
"Optima"
,
"Verdana"
,
"Arial"
,
sans
;
color
:
black
;
margin-top
:
5mm
;
margin-bottom
:
3mm
;
border-bottom
:
thin
solid
#404040
;
...
...
@@ -163,7 +156,6 @@ h4,h5,h6 {
font-size
:
10pt
;
font-style
:
italic
;
font-weight
:
bold
;
color
:
darkred
;
}
p
{
margin
:
6px
0px
6px
0px
;
width
:
15cm
;
}
...
...
@@ -178,6 +170,8 @@ li {
padding-right
:
6px
;
}
li
p
{
margin
:
0px
}
pre
{
width
:
15cm
;
background-color
:
#eef
;
...
...
nix/default.nix
View file @
00ff948a
...
...
@@ -192,7 +192,6 @@ rec {
caveat_importer_src
=
plugins
.
caveat-importer
.
src
;
acsl_importer_src
=
plugins
.
acsl-importer
.
src
;
volatile_src
=
plugins
.
volatile
.
src
;
e_acsl_src
=
plugins
.
e-acsl
.
src
;
security_src
=
plugins
.
security
.
src
;
context_from_precondition_src
=
plugins
.
context-from-precondition
.
src
;
postPatch
=
''
...
...
@@ -213,8 +212,6 @@ rec {
chmod -R u+w -- "$sourceRoot/src/plugins/volatile"
cp -r --preserve=mode "$acsl_importer_src" "$sourceRoot/src/plugins/acsl-importer"
chmod -R u+w -- "$sourceRoot/src/plugins/acsl-importer"
cp -r --preserve=mode "$e_acsl_src" "$sourceRoot/src/plugins/e-acsl"
chmod -R u+w -- "$sourceRoot/src/plugins/e-acsl"
echo IN_FRAMA_CI=yes > "$sourceRoot/in_frama_ci"
cp -r --preserve=mode "$context_from_precondition_src" "$sourceRoot/src/plugins/context-from-precondition"
chmod -R u+w -- "$sourceRoot/src/plugins/context-from-precondition"
...
...
src/kernel_services/ast_data/kernel_function.ml
View file @
00ff948a
...
...
@@ -559,10 +559,28 @@ let is_definition kf =
|
Definition
_
->
true
|
Declaration
_
->
false
let
is_first_stmt
kf
stmt
=
try
let
first
=
find_first_stmt
kf
in
Stmt
.
equal
stmt
first
with
No_Statement
->
false
let
is_return_stmt
kf
stmt
=
try
let
return
=
find_return
kf
in
Stmt
.
equal
stmt
return
with
No_Statement
->
false
let
is_entry_point
kf
=
let
main
,
_
=
Globals
.
entry_point
()
in
equal
kf
main
let
is_main
kf
=
let
name
=
get_name
kf
in
Datatype
.
String
.
equal
name
"main"
let
returns_void
kf
=
let
result_type
,_,_,_
=
Cil
.
splitFunctionType
(
get_type
kf
)
in
match
Cil
.
unrollType
result_type
with
...
...
src/kernel_services/ast_data/kernel_function.mli
View file @
00ff948a
...
...
@@ -183,8 +183,23 @@ val is_entry_point: t -> bool
option -main).
@since Sodium-20150201 *)
val
is_main
:
t
->
bool
(** @return true iff the given function is the function called 'main' in the
program.
@since Frama-C+dev *)
val
returns_void
:
t
->
bool
val
is_first_stmt
:
t
->
stmt
->
bool
(** @return true iff the statement is the first statement of the given
function.
@since Frama-C+dev *)
val
is_return_stmt
:
t
->
stmt
->
bool
(** @return true iff the statement is the return statement of the given
function.
@since Frama-C+dev *)
(* ************************************************************************* *)
(** {2 Getters} *)
(* ************************************************************************* *)
...
...
src/kernel_services/ast_queries/logic_typing.ml
View file @
00ff948a
...
...
@@ -1447,7 +1447,13 @@ struct
Ltype
(
t1
,
l
)
,
oterm
|
t1
,
Ltype
({
lt_name
=
"set"
}
,
[
t2
])
->
let
typ
,
term
=
implicit_conversion
~
overloaded
loc
oterm
t1
t2
in
make_set_type
typ
,
term
let
stype
=
make_set_type
typ
in
let
term
=
if
not
(
Logic_const
.
is_set_type
term
.
term_type
)
then
Logic_const
.
tlogic_coerce
~
loc
:
term
.
term_loc
term
stype
else
term
in
stype
,
term
|
Linteger
,
Linteger
|
Lreal
,
Lreal
->
ot
,
oterm
|
Lvar
s1
,
Lvar
s2
when
s1
=
s2
->
ot
,
oterm
|
Larrow
(
args1
,
rt1
)
,
Larrow
(
args2
,
rt2
)
...
...
src/plugins/e-acsl/Makefile.in
View file @
00ff948a
...
...
@@ -65,6 +65,7 @@ SRC_PROJECT_INITIALIZER:=\
# code generator
SRC_CODE_GENERATOR
:=
\
constructor
\
gmp
\
label
\
env
\
...
...
@@ -76,7 +77,10 @@ SRC_CODE_GENERATOR:= \
logic_functions
\
translate
\
temporal
\
visit
memory_observer
\
literal_observer
\
global_observer
\
injector
SRC_CODE_GENERATOR
:=
$(
addprefix
src/code_generator/,
$(SRC_CODE_GENERATOR)
)
#########################
...
...
@@ -253,9 +257,9 @@ EACSL_CLEANFILES = doc/doxygen/doxygen.cfg \
Makefile config.log config.status configure .depend autom4te.cache/
*
\
META.frama-c-e_acsl Makefile.plugin.generated src/local_config.ml top/
*
e-acsl-distclean
:
:
clean
e-acsl-distclean
:
clean
$(PRINT_RM)
generated project files
$(RM)
$(
addprefix
$(E_ACSL_DIR)
/,
$(EACSL_CLEANFILES)
)
$(RM)
$(
wildcard
$(
addprefix
$(E_ACSL_DIR)
/,
$(EACSL_CLEANFILES)
)
)
################################
# Building source distribution #
...
...
@@ -328,6 +332,13 @@ PLUGIN_HEADER_EXCEPTIONS:=
# and dedicated to distributed tests
PLUGIN_DISTRIB_TESTS
:=
$(EACSL_DISTRIB_TESTS)
########
# Misc #
########
wc
:
ocamlwc
-p
$(EACSL_OCAML_FILES)
##########
# Header #
##########
...
...
src/plugins/e-acsl/doc/Changelog
View file @
00ff948a
...
...
@@ -19,6 +19,8 @@
# configure configure
###############################################################################
-* E-ACSL [2019/12/04] Fix bug with compiler built-ins.
############################
Plugin E-ACSL 20.0 (Calcium)
############################
...
...
src/plugins/e-acsl/headers/header_spec.txt
View file @
00ff948a
...
...
@@ -52,16 +52,26 @@ src/analyses/typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/at_with_lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/at_with_lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/constructor.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/constructor.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/env.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/env.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/global_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/global_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/gmp.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/gmp.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/injector.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/injector.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/literal_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/literal_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/logic_functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/logic_functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/loops.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/memory_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/memory_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/mmodel_translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/mmodel_translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/quantif.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
...
...
src/plugins/e-acsl/src/analyses/exit_points.mli
View file @
00ff948a
...
...
@@ -21,12 +21,12 @@
(**************************************************************************)
(** E-ACSL tracks a local variable by injecting:
- a call to [__e_acsl_store_block] at the beginning of its scope, and
- a call to [__e_acsl_delete_block] at the end of the scope.
This is not always sufficient to track variables because execution
may exit a scope early (for instance via a goto or a break statement).
This module computes program points at which extra `delete_block` statements
need to be added to handle such early scope exits. *)
- a call to [__e_acsl_store_block] at the beginning of its scope, and
- a call to [__e_acsl_delete_block] at the end of the scope.
This is not always sufficient to track variables because execution
may exit a scope early (for instance via a goto or a break statement).
This module computes program points at which extra `delete_block` statements
need to be added to handle such early scope exits. *)
open
Cil_types
open
Cil_datatype
...
...
@@ -39,10 +39,10 @@ val clear: unit -> unit
val
delete_vars
:
stmt
->
Varinfo
.
Set
.
t
(** Given a statement which potentially leads to an early scope exit (such as
goto, break or continue) return the list of local variables which
need to be removed from tracking before that statement is executed.
Before calling this function [generate] need to be executed. *)
goto, break or continue) return the list of local variables which
need to be removed from tracking before that statement is executed.
Before calling this function [generate] need to be executed. *)
val
store_vars
:
stmt
->
Varinfo
.
Set
.
t
(** Compute variables that should be re-recorded before a labelled statement to
which some goto jumps *)
which some goto jumps
.
*)
src/plugins/e-acsl/src/analyses/interval.ml
View file @
00ff948a
...
...
@@ -519,8 +519,8 @@ let rec infer t =
|
LBnone
|
LBreads
_
->
(
match
li
.
l_type
with
|
None
->
assert
false
|
Some
ret_type
->
interv_of_logic_typ
ret_type
)
|
None
->
assert
false
|
Some
ret_type
->
interv_of_logic_typ
ret_type
)
|
LBinductive
_
->
Error
.
not_yet
"logic functions inductively defined"
)
...
...
src/plugins/e-acsl/src/analyses/literal_strings.ml
View file @
00ff948a
...
...
@@ -23,8 +23,8 @@
open
Cil_types
let
strings
:
varinfo
Datatype
.
String
.
Hashtbl
.
t
=
Datatype
.
String
.
Hashtbl
.
create
16
:
varinfo
Datatype
.
String
.
Hashtbl
.
t
=
Datatype
.
String
.
Hashtbl
.
create
16
let
reset
()
=
Datatype
.
String
.
Hashtbl
.
clear
strings
...
...
src/plugins/e-acsl/src/analyses/lscope.ml
View file @
00ff948a
...
...
@@ -41,9 +41,9 @@ let get_all t = List.rev t
let
exists
lv
t
=
let
is_lv
=
function
|
Lvs_let
(
lv'
,
_
)
|
Lvs_quantif
(
_
,
_
,
lv'
,
_
,
_
)
|
Lvs_formal
(
lv'
,
_
)
|
Lvs_global
(
lv'
,
_
)
->
Cil_datatype
.
Logic_var
.
equal
lv
lv'
|
Lvs_let
(
lv'
,
_
)
|
Lvs_quantif
(
_
,
_
,
lv'
,
_
,
_
)
|
Lvs_formal
(
lv'
,
_
)
|
Lvs_global
(
lv'
,
_
)
->
Cil_datatype
.
Logic_var
.
equal
lv
lv'
in
List
.
exists
is_lv
t
...
...
@@ -51,14 +51,14 @@ exception Lscope_used
let
is_used
lscope
pot
=
let
o
=
object
inherit
Visitor
.
frama_c_inplace
method
!
vlogic_var_use
lv
=
match
lv
.
lv_origin
with
|
Some
_
->
Cil
.
SkipChildren
|
None
->
if
exists
lv
lscope
then
raise
Lscope_used
else
Cil
.
SkipChildren
|
Some
_
->
Cil
.
SkipChildren
|
None
->
if
exists
lv
lscope
then
raise
Lscope_used
else
Cil
.
SkipChildren
end
in
try
(
match
pot
with
|
Misc
.
PoT_pred
p
->
ignore
(
Visitor
.
visitFramacPredicate
o
p
)
|
Misc
.
PoT_term
t
->
ignore
(
Visitor
.
visitFramacTerm
o
t
));
|
Misc
.
PoT_pred
p
->
ignore
(
Visitor
.
visitFramacPredicate
o
p
)
|
Misc
.
PoT_term
t
->
ignore
(
Visitor
.
visitFramacTerm
o
t
));
false
with
Lscope_used
->
true
\ No newline at end of file
true
src/plugins/e-acsl/src/analyses/lscope.mli
View file @
00ff948a
...
...
@@ -23,8 +23,8 @@
open
Cil_types
(* Handle the logic scope of a term.
We define the logic scope of a term [t] to be the set of PURELY logic
variables that are
visible by [t]
. *)
We define the logic scope of a term [t] to be the set of PURELY logic
variables that are
bound in [t] in case of use
. *)
type
lscope_var
=
|
Lvs_let
of
logic_var
*
term
(* the expression to which the lv is binded *)
...
...
@@ -45,9 +45,9 @@ val add: lscope_var -> t -> t
val
get_all
:
t
->
lscope_var
list
(* Return the list of [lscope_var] of the given logic scope.
The first element is the first [lscope_var] that was added to [t], the
second element is the second [lscope_var] that was added to [t], an so on. *)
The first element is the first [lscope_var] that was added to [t], the
second element is the second [lscope_var] that was added to [t], an so on. *)
val
is_used
:
t
->
Misc
.
pred_or_term
->
bool
(* [is_used lscope pot] returns [true] iff [pot] uses a variable from
[lscope]. *)
\ No newline at end of file
[lscope]. *)
src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
View file @
00ff948a
...
...
@@ -442,14 +442,8 @@ let register_predicate kf pred state =
branch (not considering the exception handlers) *)
let
doStmt
stmt
=
let
_
,
kf
=
Kernel_function
.
find_from_sid
stmt
.
sid
in
let
is_first
=
try
Stmt
.
equal
stmt
(
Kernel_function
.
find_first_stmt
kf
)
with
Kernel_function
.
No_Statement
->
assert
false
in
let
is_last
=
try
Stmt
.
equal
stmt
(
Kernel_function
.
find_return
kf
)
with
Kernel_function
.
No_Statement
->
assert
false
in
let
is_first
=
Kernel_function
.
is_first_stmt
kf
stmt
in
let
is_last
=
Kernel_function
.
is_return_stmt
kf
stmt
in
Dataflow
.
Post
(
fun
state
->
let
state
=
Env
.
default_varinfos
state
in
...
...
@@ -710,11 +704,7 @@ if there are memory-related annotations.@]"
Env
.
consolidated_mem
vi
end
let
must_model_vi
bhv
?
kf
?
stmt
vi
=
let
vi
=
match
bhv
with
|
None
->
vi
|
Some
bhv
->
Visitor_behavior
.
Get_orig
.
varinfo
bhv
vi
in
let
must_model_vi
?
kf
?
stmt
vi
=
let
_kf
=
match
kf
,
stmt
with
|
None
,
None
|
Some
_
,
_
->
kf
|
None
,
Some
stmt
->
Some
(
Kernel_function
.
find_englobing_kf
stmt
)
...
...
@@ -743,19 +733,19 @@ consolidated_must_model_vi vi
false
*)
let
rec
apply_on_vi_base_from_lval
f
bhv
?
kf
?
stmt
=
function
|
Var
vi
,
_
->
f
bhv
?
kf
?
stmt
vi
|
Mem
e
,
_
->
apply_on_vi_base_from_exp
f
bhv
?
kf
?
stmt
e
let
rec
apply_on_vi_base_from_lval
f
?
kf
?
stmt
=
function
|
Var
vi
,
_
->
f
?
kf
?
stmt
vi
|
Mem
e
,
_
->
apply_on_vi_base_from_exp
f
?
kf
?
stmt
e
and
apply_on_vi_base_from_exp
f
bhv
?
kf
?
stmt
e
=
match
e
.
enode
with
and
apply_on_vi_base_from_exp
f
?
kf
?
stmt
e
=
match
e
.
enode
with
|
Lval
lv
|
AddrOf
lv
|
StartOf
lv
->
apply_on_vi_base_from_lval
f
bhv
?
kf
?
stmt
lv
apply_on_vi_base_from_lval
f
?
kf
?
stmt
lv
|
BinOp
((
PlusPI
|
IndexPI
|
MinusPI
)
,
e1
,
_
,
_
)
->
apply_on_vi_base_from_exp
f
bhv
?
kf
?
stmt
e1
apply_on_vi_base_from_exp
f
?
kf
?
stmt
e1
|
BinOp
(
MinusPP
,
e1
,
e2
,
_
)
->
apply_on_vi_base_from_exp
f
bhv
?
kf
?
stmt
e1
||
apply_on_vi_base_from_exp
f
bhv
?
kf
?
stmt
e2
|
Info
(
e
,
_
)
|
CastE
(
_
,
e
)
->
apply_on_vi_base_from_exp
f
bhv
?
kf
?
stmt
e
apply_on_vi_base_from_exp
f
?
kf
?
stmt
e1
||
apply_on_vi_base_from_exp
f
?
kf
?
stmt
e2
|
Info
(
e
,
_
)
|
CastE
(
_
,
e
)
->
apply_on_vi_base_from_exp
f
?
kf
?
stmt
e
|
BinOp
((
PlusA
|
MinusA
|
Mult
|
Div
|
Mod
|
Shiftlt
|
Shiftrt
|
Lt
|
Gt
|
Le
|
Ge
|
Eq
|
Ne
|
BAnd
|
BXor
|
BOr
|
LAnd
|
LOr
)
,
_
,
_
,
_
)
|
Const
_
->
(* possible in case of static address *)
false
...
...
@@ -765,18 +755,16 @@ and apply_on_vi_base_from_exp f bhv ?kf ?stmt e = match e.enode with
let
must_model_lval
=
apply_on_vi_base_from_lval
must_model_vi
let
must_model_exp
=
apply_on_vi_base_from_exp
must_model_vi
let
must_never_monitor_lval
bhv
?
kf
?
stmt
lv
=
let
must_never_monitor_lval
?
kf
?
stmt
lv
=
apply_on_vi_base_from_lval
(
fun
_bhv
?
kf
:_
?
stmt
:_
vi
->
must_never_monitor
vi
)
bhv
(
fun
?
kf
:_
?
stmt
:_
vi
->
must_never_monitor
vi
)
?
kf
?
stmt
lv
let
must_never_monitor_exp
bhv
?
kf
?
stmt
lv
=
let
must_never_monitor_exp
?
kf
?
stmt
lv
=
apply_on_vi_base_from_exp
(
fun
_bhv
?
kf
:_
?
stmt
:_
vi
->
must_never_monitor
vi
)
bhv
(
fun
?
kf
:_
?
stmt
:_
vi
->
must_never_monitor
vi
)
?
kf
?
stmt
lv
...
...
@@ -785,23 +773,23 @@ let must_never_monitor_exp bhv ?kf ?stmt lv =
(** {1 Public API} *)
(* ************************************************************************** *)
let
must_model_vi
?
bhv
?
kf
?
stmt
vi
=
let
must_model_vi
?
kf
?
stmt
vi
=
not
(
must_never_monitor
vi
)
&&
(
Options
.
Full_mmodel
.
get
()
||
Error
.
generic_handle
(
must_model_vi
bhv
?
kf
?
stmt
)
false
vi
)
||
Error
.
generic_handle
(
must_model_vi
?
kf
?
stmt
)
false
vi
)
let
must_model_lval
?
bhv
?
kf
?
stmt
lv
=
not
(
must_never_monitor_lval
bhv
?
kf
?
stmt
lv
)
let
must_model_lval
?
kf
?
stmt
lv
=
not
(
must_never_monitor_lval
?
kf
?
stmt
lv
)
&&
(
Options
.
Full_mmodel
.
get
()
||
Error
.
generic_handle
(
must_model_lval
bhv
?
kf
?
stmt
)
false
lv
)
||
Error
.
generic_handle
(
must_model_lval
?
kf
?
stmt
)
false
lv
)
let
must_model_exp
?
bhv
?
kf
?
stmt
exp
=
not
(
must_never_monitor_exp
bhv
?
kf
?
stmt
exp
)
let
must_model_exp
?
kf
?
stmt
exp
=
not
(
must_never_monitor_exp
?
kf
?
stmt
exp
)
&&
(
Options
.
Full_mmodel
.
get
()
||
Error
.
generic_handle
(
must_model_exp
bhv
?
kf
?
stmt
)
false
exp
)
||
Error
.
generic_handle
(
must_model_exp
?
kf
?
stmt
)
false
exp
)
let
use_model
()
=
not
(
Env
.
is_empty
()
)
...
...
@@ -810,6 +798,6 @@ let use_model () =
(*
Local Variables:
compile-command: "make"
compile-command: "make
-C ../..
"
End:
*)
src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
View file @
00ff948a
...
...
@@ -31,19 +31,15 @@ val reset: unit -> unit
val
use_model
:
unit
->
bool
(** Is one variable monitored (at least)? *)
val
must_model_vi
:
?
bhv
:
Visitor_behavior
.
t
->
?
kf
:
kernel_function
->
?
stmt
:
stmt
->
varinfo
->
bool
val
must_model_vi
:
?
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] *)
library. *)
val
must_model_lval
:
?
bhv
:
Visitor_behavior
.
t
->
?
kf
:
kernel_function
->
?
stmt
:
stmt
->
lval
->
bool
val
must_model_lval
:
?
kf
:
kernel_function
->
?
stmt
:
stmt
->
lval
->
bool
(** Same as {!must_model_vi}, for left-values *)
val
must_model_exp
:
?
bhv
:
Visitor_behavior
.
t
->
?
kf
:
kernel_function
->
?
stmt
:
stmt
->
exp
->
bool
val
must_model_exp
:
?
kf
:
kernel_function
->
?
stmt
:
stmt
->
exp
->
bool
(** Same as {!must_model_vi}, for expressions *)
(*
...
...
src/plugins/e-acsl/src/analyses/typing.ml
View file @
00ff948a
...
...
@@ -28,9 +28,9 @@ open Cil_types
let
dkey
=
Options
.
dkey_typing
let
compute_quantif_guards_ref
:
(
predicate
->
logic_var
list
->
predicate
->
(
term
*
relation
*
logic_var
*
relation
*
term
)
list
)
ref
=
Extlib
.
mk_fun
"compute_quantif_guards_ref"
:
(
predicate
->
logic_var
list
->
predicate
->
(
term
*
relation
*
logic_var
*
relation
*
term
)
list
)
ref
=
Extlib
.
mk_fun
"compute_quantif_guards_ref"
(******************************************************************************)
(** Datatype and constructor *)
...
...
@@ -168,11 +168,11 @@ let typ_of_lty = function
(******************************************************************************)
type
computed_info
=
{
ty
:
D
.
t
;
(* type required for the term *)
op
:
D
.
t
;
(* type required for the operation *)
cast
:
D
.
t
option
;
(* if not [None], type of the context which the term
{
ty
:
D
.
t
;
(* type required for the term *)
op
:
D
.
t
;
(* type required for the operation *)
cast
:
D
.
t
option
;
(* if not [None], type of the context which the term
must be casted to. If [None], no cast needed. *)
}
}
(* Memoization module which retrieves the computed info of some terms. If the
info is already computed for a term, it is never recomputed *)
...
...
@@ -183,23 +183,23 @@ module Memo: sig
end
=
struct
module
H
=
Hashtbl
.
Make
(
struct
type
t
=
term
(*
t
he comparison over terms is the physical equality. It cannot be the
structural one (given by [Cil_datatype.Term.equal]) because the very
same term can be used in 2 different contexts which lead to different
casts.
By construction, there are no physically equal terms in the AST
built by Cil. Consequently the memoisation should be fully
useless. However the translation of E-ACSL guarded quantification
generates new terms (see module {!Quantif}) which must be typed. The term
corresponding to the bound variable [x] is actually used twice: once in
the guard and once for encoding [x+1] when incrementing it. The
memoization is only useful here and indeed prevent the generation of
one extra variable in some cases. *)
let
equal
(
t1
:
term
)
t2
=
t1
==
t2
let
hash
=
Cil_datatype
.
Term
.
hash
end
)
type
t
=
term
(*
T
he comparison over terms is the physical equality. It cannot be the
structural one (given by [Cil_datatype.Term.equal]) because the very
same term can be used in 2 different contexts which lead to different
casts.
By construction, there are no physically equal terms in the AST
built by Cil. Consequently the memoisation should be fully
useless. However the translation of E-ACSL guarded quantification
generates new terms (see module {!Quantif}) which must be typed. The term
corresponding to the bound variable [x] is actually used twice: once in
the guard and once for encoding [x+1] when incrementing it. The