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
272e20ed
Commit
272e20ed
authored
Apr 06, 2020
by
Andre Maroneze
Browse files
[Eva] Fix a few typos
parent
1fb898cc
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/plugins/value/domains/abstract_domain.mli
View file @
272e20ed
...
@@ -362,7 +362,7 @@ module type S = sig
...
@@ -362,7 +362,7 @@ module type S = sig
that depend on the memory location [loc].
that depend on the memory location [loc].
If the first argument is not None, it contains the logical clause being
If the first argument is not None, it contains the logical clause being
interpreted and the pre-state in which the terms of the clause are
interpreted and the pre-state in which the terms of the clause are
evaluated. The clause can be an
\
assign,
\
allocate
d
or
\
free clause.
evaluated. The clause can be an assign
s
, allocate
s
or free
s
clause.
[loc] is then the memory location concerned by the clause. *)
[loc] is then the memory location concerned by the clause. *)
val
logic_assign
:
(
logic_assign
*
state
)
option
->
location
->
state
->
state
val
logic_assign
:
(
logic_assign
*
state
)
option
->
location
->
state
->
state
...
...
src/plugins/value/domains/domain_builder.ml
View file @
272e20ed
...
@@ -286,7 +286,7 @@ module Restrict
...
@@ -286,7 +286,7 @@ module Restrict
(* This module propagates states of type [(state * mode) option]:
(* This module propagates states of type [(state * mode) option]:
- None is propagated as long as no functions from [Scope.functions]
- None is propagated as long as no functions from [Scope.functions]
is
analyzed.
are
analyzed.
- then the current [mode] is propagated alongside the state. Queries and
- then the current [mode] is propagated alongside the state. Queries and
transfer functions are applied accordingly. The current mode is replaced
transfer functions are applied accordingly. The current mode is replaced
at function calls by [mode.calls]. *)
at function calls by [mode.calls]. *)
...
@@ -422,7 +422,7 @@ module Restrict
...
@@ -422,7 +422,7 @@ module Restrict
(* Starts an analysis at call [call] with state [state]. The domain was not
(* Starts an analysis at call [call] with state [state]. The domain was not
enabled before this call: the concrete arguments may contain variables that
enabled before this call: the concrete arguments may contain variables that
have never been introduced into the state, so we should not use them. This
have never been introduced into the state, so we should not use them. This
function only introduce the formal parameters in the state. *)
function only introduce
s
the formal parameters in the state. *)
let
start_analysis
call
state
=
let
start_analysis
call
state
=
let
formals
=
List
.
map
(
fun
argument
->
argument
.
formal
)
call
.
arguments
in
let
formals
=
List
.
map
(
fun
argument
->
argument
.
formal
)
call
.
arguments
in
let
kind
=
Abstract_domain
.
Formal
call
.
kf
in
let
kind
=
Abstract_domain
.
Formal
call
.
kf
in
...
...
src/plugins/value/domains/domain_mode.mli
View file @
272e20ed
...
@@ -20,7 +20,7 @@
...
@@ -20,7 +20,7 @@
(* *)
(* *)
(**************************************************************************)
(**************************************************************************)
(** This module defines the mode to restrict an abstract domain
s
on specific
(** This module defines the mode to restrict an abstract domain on specific
functions. *)
functions. *)
(** Permission for an abstract domain to read/write its state.
(** Permission for an abstract domain to read/write its state.
...
...
src/plugins/value/engine/abstractions.mli
View file @
272e20ed
...
@@ -25,9 +25,9 @@
...
@@ -25,9 +25,9 @@
(** {2 Registration of abstractions.} *)
(** {2 Registration of abstractions.} *)
(** Dynamic registration of the abstractions to be used in an Eva analysis:
(** Dynamic registration of the abstractions to be used in an Eva analysis:
- value abstractions, detail
l
ed in the {Abstract_value} signature;
- value abstractions, detailed in the {Abstract_value} signature;
- location abstractions, detail
l
ed in the {Abstract_location} signature;
- location abstractions, detailed in the {Abstract_location} signature;
- state abstractions, or abstract domains, detail
l
ed in {Abstract_domain}.
- state abstractions, or abstract domains, detailed in {Abstract_domain}.
*)
*)
(** Module types of value abstractions: either a single leaf module, or
(** Module types of value abstractions: either a single leaf module, or
...
@@ -138,7 +138,7 @@ val register_hook: ((module S) -> (module S)) -> unit
...
@@ -138,7 +138,7 @@ val register_hook: ((module S) -> (module S)) -> unit
(** {2 Configuration of an analysis.} *)
(** {2 Configuration of an analysis.} *)
(** Configuration defining the abstractions to be used in an analysis.
(** Configuration defining the abstractions to be used in an analysis.
A configuration is a set of flags, i.e. a set of abstract domain. Each flag
A configuration is a set of flags, i.e. a set of abstract domain
s
. Each flag
comes with an optional mode. None is the default mode: the given domain is
comes with an optional mode. None is the default mode: the given domain is
enabled for the whole analysis. See {!Domain_mode} for more details. *)
enabled for the whole analysis. See {!Domain_mode} for more details. *)
module
Config
:
sig
module
Config
:
sig
...
...
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