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
e2fbbc53
Commit
e2fbbc53
authored
Dec 16, 2019
by
Julien Signoles
Browse files
[e-acsl:archi] take into account 2nd Michele's review
parent
f4e9007e
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/src/code_generator/constructor.ml
View file @
e2fbbc53
...
...
@@ -69,7 +69,7 @@ let mk_lib_call ~loc ?result fname args =
let
vi
=
Misc
.
get_lib_fun_vi
fname
in
let
f
=
Cil
.
evar
~
loc
vi
in
vi
.
vreferenced
<-
true
;
let
make_args
args
ty_
param
s
=
let
make_args
args
param
_ty
=
List
.
map2
(
fun
(
_
,
ty
,
_
)
arg
->
let
e
=
...
...
@@ -79,7 +79,7 @@ let mk_lib_call ~loc ?result fname args =
|
_
,
_
,
_
->
arg
in
Cil
.
mkCast
~
force
:
false
~
newt
:
ty
~
e
)
ty_
param
s
param
_ty
args
in
let
args
=
match
Cil
.
unrollType
vi
.
vtype
with
...
...
src/plugins/e-acsl/src/code_generator/constructor.mli
View file @
e2fbbc53
...
...
@@ -31,7 +31,7 @@ val mk_deref: loc:Location.t -> exp -> exp
val
mk_block
:
stmt
->
block
->
stmt
(* ********************************************************************** *)
(* E-ACSL specific code: build calls to its API *)
(* E-ACSL specific code: build calls to its
RTL
API *)
(* ********************************************************************** *)
val
mk_lib_call
:
loc
:
Location
.
t
->
?
result
:
lval
->
string
->
exp
list
->
stmt
...
...
src/plugins/e-acsl/src/code_generator/global_observer.mli
View file @
e2fbbc53
...
...
@@ -26,23 +26,23 @@ open Cil_types
val
function_name
:
string
(** Name of the function in which [mk_init_function] (see below) generates the
**
code. *)
code. *)
val
reset
:
unit
->
unit
val
is_empty
:
unit
->
bool
val
add
:
varinfo
->
unit
(** Observe
s
the given variable if necessary. *)
(** Observe the given variable if necessary. *)
val
add_initializer
:
varinfo
->
offset
->
init
->
unit
(** Add the initializer for the given observed variable. *)
val
mk_init_function
:
unit
->
varinfo
*
fundec
(** Generate
s
a new C function containing the observers for global variable
(** Generate a new C function containing the observers for global variable
declarations and initializations. *)
val
mk_delete_stmts
:
stmt
list
->
stmt
list
(** Generate
s
the observers for global variable de-allocations. *)
(** Generate the observers for global variable de-allocations. *)
(*
Local Variables:
...
...
src/plugins/e-acsl/src/code_generator/injector.ml
View file @
e2fbbc53
...
...
@@ -27,7 +27,7 @@ open Cil_datatype
let
dkey
=
Options
.
dkey_translation
(* ************************************************************************** *)
(*
Code
*)
(*
Expression
*)
(* ************************************************************************** *)
let
replace_literal_string_in_exp
env
kf_opt
(* None for globals *)
e
=
...
...
@@ -108,6 +108,10 @@ let inject_in_local_init loc env kf vi = function
in
ConsInit
(
vi
,
l
,
ck
)
,
env
(* ************************************************************************** *)
(* Instructions and statements *)
(* ************************************************************************** *)
(* rewrite names of functions for which we have alternative definitions in the
RTL. *)
let
rename_caller
loc
args
exp
=
match
exp
.
enode
with
...
...
@@ -466,7 +470,7 @@ and inject_in_block (env: Env.t) kf blk =
blk
.
bstmts
in
blk
.
bstmts
<-
List
.
rev
stmts
;
(* now inject code that de-allocate the necessary observation variables and
(* now inject code that de-allocate
s
the necessary observation variables and
blocks of the runtime memory that have been previously allocated *)
(* calls to [free] for de-allocating variables observing \at(_,_) *)
let
free_stmts
=
At_with_lscope
.
Free
.
find_all
kf
in
...
...
src/plugins/e-acsl/src/libraries/misc.ml
View file @
e2fbbc53
...
...
@@ -49,10 +49,11 @@ let reset () = Datatype.String.Hashtbl.clear library_functions
let
is_fc_or_compiler_builtin
vi
=
Cil
.
is_builtin
vi
||
(
String
.
length
vi
.
vname
>
10
(* number of characters in "__builtin_" *)
&&
let
prefix
=
String
.
sub
vi
.
vname
0
10
in
Datatype
.
String
.
equal
prefix
"__builtin_"
)
(
let
prefix_length
=
10
(* number of characters in "__builtin_" *)
in
String
.
length
vi
.
vname
>
prefix_length
&&
let
prefix
=
String
.
sub
vi
.
vname
0
prefix_length
in
Datatype
.
String
.
equal
prefix
"__builtin_"
)
(* ************************************************************************** *)
(** {2 Builders} *)
...
...
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