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
342cf647
Commit
342cf647
authored
Dec 06, 2019
by
Julien Signoles
Browse files
[e-acsl] lint
parent
c4cee6f8
Changes
28
Hide whitespace changes
Inline
Side-by-side
.Makefile.lint
View file @
342cf647
...
...
@@ -378,42 +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/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
src/plugins/e-acsl/src/analyses/exit_points.mli
View file @
342cf647
...
...
@@ -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 @
342cf647
...
...
@@ -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 @
342cf647
...
...
@@ -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 @
342cf647
...
...
@@ -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 @
342cf647
...
...
@@ -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 visible by [t]. *)
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/typing.ml
View file @
342cf647
...
...
@@ -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
(* the 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
(* the 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
)
let
tbl
=
H
.
create
97
...
...
@@ -246,10 +246,10 @@ let ty_of_interv ?ctx = function
|
Some
(
C_float
_
|
Rational
|
Real
as
ty
)
->
ty
)
with
Cil
.
Not_representable
->
match
ctx
with
|
None
|
Some
(
C_integer
_
|
Gmpz
|
Nan
)
->
Gmpz
|
Some
(
C_float
_
|
Rational
)
->
Rational
|
Some
Real
->
Real
match
ctx
with
|
None
|
Some
(
C_integer
_
|
Gmpz
|
Nan
)
->
Gmpz
|
Some
(
C_float
_
|
Rational
)
->
Rational
|
Some
Real
->
Real
(* compute a new {!computed_info} by coercing the given type [ty] to the given
context [ctx]. [op] is the type for the operator. *)
...
...
@@ -263,9 +263,9 @@ let coerce ~arith_operand ~ctx ~op ty =
or if the term corresponding to [ty] is an operand of an arithmetic
operation which must be explicitly coerced in order to force the
operation to be of the expected type. *)
if
(
ctx
=
Gmpz
&&
ty
<>
Gmpz
)
||
arith_operand
then
{
ty
;
op
;
cast
=
Some
ctx
}
else
{
ty
;
op
;
cast
=
None
}
if
(
ctx
=
Gmpz
&&
ty
<>
Gmpz
)
||
arith_operand
then
{
ty
;
op
;
cast
=
Some
ctx
}
else
{
ty
;
op
;
cast
=
None
}
let
number_ty_of_typ
ty
=
match
Cil
.
unrollType
ty
with
|
TInt
(
ik
,
_
)
|
TEnum
({
ekind
=
ik
}
,
_
)
->
C_integer
ik
...
...
@@ -723,13 +723,13 @@ let get_integer_op_of_predicate p = (type_predicate p).op
let
extract_typ
t
ty
=
try
typ_of_number_ty
ty
with
Not_a_number
->
match
t
.
term_type
with
|
Ctype
_
as
lty
->
Logic_utils
.
logicCType
lty
|
Linteger
|
Lreal
->
Options
.
fatal
"unexpected context NaN for term %a"
Printer
.
pp_term
t
|
Ltype
_
->
Error
.
not_yet
"unsupported logic type: user-defined type"
|
Lvar
_
->
Error
.
not_yet
"unsupported logic type: type variable"
|
Larrow
_
->
Error
.
not_yet
"unsupported logic type: type arrow"
match
t
.
term_type
with
|
Ctype
_
as
lty
->
Logic_utils
.
logicCType
lty
|
Linteger
|
Lreal
->
Options
.
fatal
"unexpected context NaN for term %a"
Printer
.
pp_term
t
|
Ltype
_
->
Error
.
not_yet
"unsupported logic type: user-defined type"
|
Lvar
_
->
Error
.
not_yet
"unsupported logic type: type variable"
|
Larrow
_
->
Error
.
not_yet
"unsupported logic type: type arrow"
let
get_typ
t
=
let
info
=
Memo
.
get
t
in
...
...
src/plugins/e-acsl/src/analyses/typing.mli
View file @
342cf647
...
...
@@ -154,8 +154,8 @@ val typ_of_lty: logic_type -> typ
(******************************************************************************)
val
compute_quantif_guards_ref
:
(
predicate
->
logic_var
list
->
predicate
->
(
term
*
relation
*
logic_var
*
relation
*
term
)
list
)
ref
:
(
predicate
->
logic_var
list
->
predicate
->
(
term
*
relation
*
logic_var
*
relation
*
term
)
list
)
ref
(** Forward reference. *)
(*
...
...
src/plugins/e-acsl/src/code_generator/env.ml
View file @
342cf647
...
...
@@ -159,7 +159,7 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
|
Varname
.
Function
->
LFunction
kf
|
Varname
.
Block
->
LLocal_block
kf
in
(* Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
(* Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
let
e
=
Cil
.
evar
v
in
let
stmts
=
mk_stmts
v
e
in
let
new_stmts
=
acc_list_rev
local_block
.
new_stmts
stmts
in
...
...
@@ -172,15 +172,15 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
new_stmts
=
new_stmts
;
pre_stmts
=
local_block
.
pre_stmts
;
post_stmts
=
local_block
.
post_stmts
}
}
in
v
,
e
,
if
is_z_t
||
is_q_t
then
begin
let
extend_tbl
tbl
=
(* Options.feedback "memoizing %a for term %a"
Varinfo.pretty v (fun fmt t -> match t with None -> Format.fprintf fmt
"NONE" | Some t -> Term.pretty fmt t) t;*)
(* Options.feedback "memoizing %a for term %a"
Varinfo.pretty v (fun fmt t -> match t with None -> Format.fprintf fmt
"NONE" | Some t -> Term.pretty fmt t) t;*)
{
clear_stmts
=
Gmp
.
clear
~
loc
e
::
tbl
.
clear_stmts
;
new_exps
=
match
t
with
|
None
->
tbl
.
new_exps
...
...
@@ -353,11 +353,11 @@ let extend_stmt_in_place env stmt ~label block =
env
let
push
env
=
(* Options.feedback "push (was %d)" (List.length env.env_stack);*)
(* Options.feedback "push (was %d)" (List.length env.env_stack);*)
{
env
with
env_stack
=
empty_local_env
::
env
.
env_stack
}
let
pop
env
=
(* Options.feedback "pop";*)
(* Options.feedback "pop";*)
let
_
,
tl
=
top
env
in
{
env
with
env_stack
=
tl
}
...
...
@@ -377,7 +377,7 @@ let transfer ~from env = match from.env_stack, env.env_stack with
type
where
=
Before
|
Middle
|
After
let
pop_and_get
?
(
split
=
false
)
env
stmt
~
global_clear
where
=
let
split
=
split
&&
stmt
.
labels
=
[]
in
(* Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split;*)
(* Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split;*)
let
local_env
,
tl
=
top
env
in
let
clear
=
if
global_clear
then
begin
...
...
@@ -386,8 +386,8 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
end
else
local_env
.
mp_tbl
.
clear_stmts
in
(* Options.feedback "clearing %d mpz (global_clear: %b)"
(List.length clear) global_clear;*)
(* Options.feedback "clearing %d mpz (global_clear: %b)"
(List.length clear) global_clear;*)
let
block
=
local_env
.
block_info
in
let
b
=
let
pre_stmts
,
stmt
=
...
...
@@ -481,9 +481,9 @@ let pretty fmt env =
let
local_env
,
_
=
top
env
in
Format
.
fprintf
fmt
"local new_stmts %t"
(
fun
fmt
->
List
.
iter
(
fun
s
->
Printer
.
pp_stmt
fmt
s
)
local_env
.
block_info
.
new_stmts
)
List
.
iter
(
fun
s
->
Printer
.
pp_stmt
fmt
s
)
local_env
.
block_info
.
new_stmts
)
(*
Local Variables:
...
...
src/plugins/e-acsl/src/code_generator/env.mli
View file @
342cf647
...
...
@@ -120,19 +120,19 @@ module Logic_scope: sig
val
extend
:
t
->
Lscope
.
lscope_var
->
t
(** Add a new logic variable with its associated information in the
logic scope of the environment. *)
logic scope of the environment. *)
val
reset
:
t
->
t
(** Return a new environment in which the logic scope is reset
iff [set_reset _ true] has been called beforehand. Do nothing otherwise. *)
iff [set_reset _ true] has been called beforehand. Do nothing otherwise. *)
val
set_reset
:
t
->
bool
->
t
(** Setter of the information indicating whether the logic scope should be
reset at next call to [reset]. *)
reset at next call to [reset]. *)
val
get_reset
:
t
->
bool
(** Getter of the information indicating whether the logic scope should be
reset at next call to [reset]. *)
reset at next call to [reset]. *)
end
(* ************************************************************************** *)
...
...
src/plugins/e-acsl/src/code_generator/label.ml
View file @
342cf647
...
...
@@ -31,7 +31,7 @@ module Labeled_stmts =
let
size
=
7
let
dependencies
=
[]
(* delayed *)
let
name
=
"E-ACSL.Labels"
end
)
end
)
let
self
=
Labeled_stmts
.
self
...
...
src/plugins/e-acsl/src/code_generator/logic_functions.ml
View file @
342cf647
...
...
@@ -121,22 +121,22 @@ let generate_kf ~loc fname env ret_ty params_ty li =
let
params
,
params_ty
=
List
.
fold_right2
(
fun
lvi
pty
(
params
,
params_ty
)
->
let
ty
=
match
pty
with
|
Typing
.
Gmpz
->
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
Gmp_types
.
Z
.
t_as_ptr
()
|
Typing
.
C_integer
ik
->
TInt
(
ik
,
[]
)
|
Typing
.
C_float
ik
->
TFloat
(
ik
,
[]
)
(* for the time being, no reals but rationals instead *)
|
Typing
.
Rational
->
Gmp_types
.
Q
.
t
()
|
Typing
.
Real
->
Error
.
not_yet
"real number"
|
Typing
.
Nan
->
Typing
.
typ_of_lty
lvi
.
lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
does not yet exist *)
let
vi
=
Cil
.
makeVarinfo
false
true
lvi
.
lv_name
ty
in
vi
::
params
,
(
lvi
.
lv_name
,
ty
,
[]
)
::
params_ty
)
let
ty
=
match
pty
with
|
Typing
.
Gmpz
->
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
Gmp_types
.
Z
.
t_as_ptr
()
|
Typing
.
C_integer
ik
->
TInt
(
ik
,
[]
)
|
Typing
.
C_float
ik
->
TFloat
(
ik
,
[]
)
(* for the time being, no reals but rationals instead *)
|
Typing
.
Rational
->
Gmp_types
.
Q
.
t
()
|
Typing
.
Real
->
Error
.
not_yet
"real number"
|
Typing
.
Nan
->
Typing
.
typ_of_lty
lvi
.
lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
does not yet exist *)
let
vi
=
Cil
.
makeVarinfo
false
true
lvi
.
lv_name
ty
in
vi
::
params
,
(
lvi
.
lv_name
,
ty
,
[]
)
::
params_ty
)
li
.
l_profile
params_ty
([]
,
[]
)
...
...
@@ -208,11 +208,11 @@ let generate_kf ~loc fname env ret_ty params_ty li =
let
locals
,
blocks
=
List
.
fold_left
(
fun
(
local_vars
,
block_vars
as
acc
)
(
v
,
scope
)
->
match
scope
with
|
Env
.
LFunction
kf'
when
Kernel_function
.
equal
kf
kf'
->
v
::
local_vars
,
block_vars
|
Env
.
LLocal_block
kf'
when
Kernel_function
.
equal
kf
kf'
->
v
::
local_vars
,
block_vars
|
_
->
acc
)
|
Env
.
LFunction
kf'
when
Kernel_function
.
equal
kf
kf'
->
v
::
local_vars
,
block_vars
|
Env
.
LLocal_block
kf'
when
Kernel_function
.
equal
kf
kf'
->
v
::
local_vars
,
block_vars
|
_
->
acc
)
(
fundec
.
slocals
,
fundec
.
sbody
.
blocals
)
vars
in
...
...
@@ -238,7 +238,7 @@ module Params_ty =
(* for each logic_info, associate its possible profiles, i.e. the types of its
parameters + the generated varinfo for the function *)
let
memo_tbl
:
kernel_function
Params_ty
.
Hashtbl
.
t
Logic_info
.
Hashtbl
.
t
kernel_function
Params_ty
.
Hashtbl
.
t
Logic_info
.
Hashtbl
.
t
=
Logic_info
.
Hashtbl
.
create
7
let
reset
()
=
Logic_info
.
Hashtbl
.
clear
memo_tbl
...
...
src/plugins/e-acsl/src/code_generator/loops.ml
View file @
342cf647
...
...
@@ -76,18 +76,18 @@ let preserve_invariant env kf stmt = match stmt.skind with
(**************************************************************************)
(* It could happen that the bounds provided for a quantifier [lv] are bigger
than its type. [bounds_for_small_type] handles such cases
and provides smaller bounds whenever possible.
Let B be the inferred interval and R the range of [lv.typ]
- Case 1: B \subseteq R
Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
Return: B
- Case 2: B \not\subseteq R and the bounds of B are inferred exactly
Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
Return: B \intersect R
- Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
Return: R with a guard guaranteeing that [lv] does not overflow *)
than its type. [bounds_for_small_type] handles such cases
and provides smaller bounds whenever possible.
Let B be the inferred interval and R the range of [lv.typ]
- Case 1: B \subseteq R
Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
Return: B
- Case 2: B \not\subseteq R and the bounds of B are inferred exactly
Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
Return: B \intersect R
- Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
Return: R with a guard guaranteeing that [lv] does not overflow *)
let
bounds_for_small_type
~
loc
(
t1
,
lv
,
t2
)
=
match
lv
.
lv_type
with
|
Ltype
_
|
Lvar
_
|
Lreal
|
Larrow
_
->
...
...
@@ -154,9 +154,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let
res
=
Logic_const
.
term
~
loc
(
TBinOp
(
PlusA
,
t
,
tone
))
Linteger
in
Extlib
.
may
(
fun
ty
->
Typing
.
unsafe_set
tone
~
ctx
:
ty
ctx
;
Typing
.
unsafe_set
t
~
ctx
:
ty
ctx
;
Typing
.
unsafe_set
res
ty
)
Typing
.
unsafe_set
tone
~
ctx
:
ty
ctx
;
Typing
.
unsafe_set
t
~
ctx
:
ty
ctx
;
Typing
.
unsafe_set
res
ty
)
ty
;
res
in
...
...
@@ -169,14 +169,14 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
t1
|
Rgt
|
Rge
|
Req
|
Rneq
->
assert
false
in
in
let
t2_one
,
bop2
=
match
rel2
with
|
Rlt
->
t2
,
Lt
|
Rle
->
(* we increment the loop counter one more time (at the end of the
loop). Thus to prevent overflow, check the type of [t2+1]
instead of [t2]. *)
loop). Thus to prevent overflow, check the type of [t2+1]
instead of [t2]. *)
t_plus_one
t2
,
Le
|
Rgt
|
Rge
|
Req
|
Rneq
->
assert
false
...
...
@@ -206,10 +206,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
(* initialize the loop counter to [t1] *)
let
e1
,
env
=
term_to_exp
kf
(
Env
.
push
env
)
t1
in
let
init_blk
,
env
=
Env
.
pop_and_get
env
(
Gmp
.
affect
~
loc
:
e1
.
eloc
lv_x
x
e1
)
~
global_clear
:
false
Env
.
Middle
env
(
Gmp
.
affect
~
loc
:
e1
.
eloc
lv_x
x
e1
)
~
global_clear
:
false
Env
.
Middle
in
(* generate the guard [x bop t2] *)
let
block_to_stmt
b
=
mkStmt
~
valid_sid
:
true
(
Block
b
)
in
...
...
@@ -223,16 +223,16 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let
guard_exp
,
env
=
term_to_exp
kf
(
Env
.
push
env
)
guard
in
let
break_stmt
=
mkStmt
~
valid_sid
:
true
(
Break
guard_exp
.
eloc
)
in
let
guard_blk
,
env
=
Env
.
pop_and_get
env
(
mkStmt
~
valid_sid
:
true
(
If
(
guard_exp
,
mkBlock
[
mkEmptyStmt
~
loc
()
]
,
mkBlock
[
break_stmt
]
,
guard_exp
.
eloc
)))
~
global_clear
:
false
Env
.
Middle
env
(
mkStmt
~
valid_sid
:
true
(
If
(
guard_exp
,
mkBlock
[
mkEmptyStmt
~
loc
()
]
,
mkBlock
[
break_stmt
]
,
guard_exp
.
eloc
)))
~
global_clear
:
false
Env
.
Middle
in
let
guard
=
block_to_stmt
guard_blk
in
(* increment the loop counter [x++];
...
...
@@ -240,10 +240,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let
tlv_one
=
t_plus_one
~
ty
:
ctx_one
tlv
in
let
incr
,
env
=
term_to_exp
kf
(
Env
.
push
env
)
tlv_one
in
let
next_blk
,
env
=
Env
.
pop_and_get
env
(
Gmp
.
affect
~
loc
:
incr
.
eloc
lv_x
x
incr
)
~
global_clear
:
false
Env
.
Middle
env
(
Gmp
.
affect
~
loc
:
incr
.
eloc
lv_x
x
incr
)
~
global_clear
:
false
Env
.
Middle
in
(* generate the whole loop *)
let
next
=
block_to_stmt
next_blk
in
...
...
@@ -261,13 +261,13 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
in
let
start
=
block_to_stmt
init_blk
in
let
stmt
=
mkStmt
~
valid_sid
:
true
(
Loop
(
[]
,
mkBlock
stmts
,
loc
,
None
,
Some
break_stmt
))
~
valid_sid
:
true
(
Loop
(
[]
,
mkBlock
stmts
,
loc
,
None
,
Some
break_stmt
))
in
(* remove logic binding before returning *)