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
5492c6c5
Commit
5492c6c5
authored
Dec 13, 2019
by
Julien Signoles
Browse files
[e-acsl:lint] address Michele's comments
parent
342cf647
Changes
7
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/src/analyses/exit_points.mli
View file @
5492c6c5
...
...
@@ -45,4 +45,4 @@ val delete_vars: stmt -> Varinfo.Set.t
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/lscope.mli
View file @
5492c6c5
...
...
@@ -24,7 +24,7 @@ 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]
. *)
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 *)
...
...
src/plugins/e-acsl/src/analyses/typing.ml
View file @
5492c6c5
...
...
@@ -184,7 +184,7 @@ end = struct
module
H
=
Hashtbl
.
Make
(
struct
type
t
=
term
(*
t
he comparison over terms is the physical equality. It cannot be the
(*
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.
...
...
src/plugins/e-acsl/src/code_generator/logic_functions.ml
View file @
5492c6c5
...
...
@@ -134,7 +134,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
|
Typing
.
Nan
->
Typing
.
typ_of_lty
lvi
.
lv_type
in
(* build the formals: cannot use [Cil.makeFormal] since the function
does not
yet
exist *)
does not exis
t ye
t *)
let
vi
=
Cil
.
makeVarinfo
false
true
lvi
.
lv_name
ty
in
vi
::
params
,
(
lvi
.
lv_name
,
ty
,
[]
)
::
params_ty
)
li
.
l_profile
...
...
src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
View file @
5492c6c5
...
...
@@ -65,8 +65,8 @@ let rec has_set_as_index = function
has_set_as_index
toffset
(* Performs Range Elimination on index [TIndex(term, offset)]. Term part.
Raises [Range_elimination_exception]
if
whether the operation is unsound
or
if
we don't support the construction yet. *)
Raises [Range_elimination_exception] whe
ther ei
ther the operation is unsound
or
we don't support the construction yet. *)
let
eliminate_ranges_from_index_of_term
~
loc
t
=
match
t
.
term_node
with
|
Trange
(
Some
n1
,
Some
n2
)
->
...
...
@@ -79,8 +79,8 @@ let eliminate_ranges_from_index_of_term ~loc t =
(* Performs Range Elimination on index [TIndex(term, offset)]. Offset part.
Raises [Range_elimination_exception], through [eliminate_ranges_from_
index_of_term],
if
whether the operation is unsound or
if we don't support
the construction yet. *)
index_of_term], whe
ther ei
ther the operation is unsound or
we don't support
the construction yet. *)
let
rec
eliminate_ranges_from_index_of_toffset
~
loc
toffset
quantifiers
=
match
toffset
with
|
TIndex
(
t
,
toffset'
)
->
...
...
src/plugins/e-acsl/src/code_generator/translate.ml
View file @
5492c6c5
...
...
@@ -958,8 +958,9 @@ let assumes_predicate bhv =
List
.
fold_left
(
fun
acc
p
->
let
loc
=
p
.
ip_content
.
pred_loc
in
Logic_const
.
pand
~
loc
(
acc
,
Logic_const
.
unamed
~
loc
p
.
ip_content
.
pred_content
))
Logic_const
.
pand
~
loc
(
acc
,
Logic_const
.
unamed
~
loc
p
.
ip_content
.
pred_content
))
Logic_const
.
ptrue
bhv
.
b_assumes
...
...
src/plugins/e-acsl/src/project_initializer/keep_status.ml
View file @
5492c6c5
...
...
@@ -67,8 +67,8 @@ let pretty_kind fmt k =
(* information attached to every kernel_function containing an annotation *)
type
kf_info
=
{
mutable
cpt
:
int
;
(* counter building the relationship between [push] and
[must_translate *)
{
mutable
cpt
:
int
(* counter building the relationship between [push] and
[must_translate
]
*)
;
mutable
statuses
:
(
kind
*
bool
)
Datatype
.
Int
.
Map
.
t
(* map associating a property as an integer to its kind and status
([true] = proved) *)
}
...
...
Write
Preview
Markdown
is supported
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