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
5c56d8d7
Commit
5c56d8d7
authored
Oct 11, 2019
by
Julien Signoles
Browse files
[archi] fix bug with loop invariants
parent
3defbd29
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/src/code_generator/injector.ml
View file @
5c56d8d7
...
...
@@ -235,7 +235,7 @@ let add_new_block_in_stmt env kf stmt =
(* [TODO ARCHI] what about the above comment? *)
(* Add temporal analysis instrumentations *)
let
env
=
Temporal
.
handle_stmt
stmt
env
kf
in
let
new_stmt
,
env
,
must_mv
=
let
new_stmt
,
env
=
if
Functions
.
check
kf
then
let
env
=
(* handle ghost statement *)
...
...
@@ -248,10 +248,10 @@ let add_new_block_in_stmt env kf stmt =
env
in
(* handle loop invariants *)
let
new_stmt
,
env
,
must_mv
=
Loops
.
preserve_invariant
env
kf
stmt
in
new_stmt
,
env
,
must_mv
let
new_stmt
,
env
=
Loops
.
preserve_invariant
env
kf
stmt
in
new_stmt
,
env
else
stmt
,
env
,
false
stmt
,
env
in
let
mk_post_env
env
stmt
=
Annotations
.
fold_code_annot
...
...
@@ -343,7 +343,6 @@ let add_new_block_in_stmt env kf stmt =
E_acsl_label
.
move
kf
new_stmt
res
;
res
,
env
in
if
must_mv
then
Loops
.
mv_invariants
kf
~
old
:
new_stmt
stmt
;
Options
.
debug
~
level
:
4
"@[new stmt (from sid %d):@ %a@]"
stmt
.
sid
Printer
.
pp_stmt
new_stmt
;
new_stmt
,
env
...
...
@@ -769,7 +768,6 @@ let inject () =
Misc
.
reorder_ast
()
;
let
ast
=
Ast
.
get
()
in
inject_in_file
ast
;
Loops
.
apply_after_transformation
()
;
reset_all
ast
;
(*
...
...
src/plugins/e-acsl/src/code_generator/loops.ml
View file @
5c56d8d7
...
...
@@ -43,30 +43,9 @@ let term_to_exp_ref
(************************* Loop invariants ********************************)
(**************************************************************************)
module
Loop_invariants_actions
=
Hook
.
Make
(
struct
end
)
let
apply_after_transformation
=
Loop_invariants_actions
.
apply
let
mv_invariants
kf
~
old
stmt
=
Options
.
feedback
~
current
:
true
~
level
:
3
"keep loop invariants attached to its loop"
;
let
filter
_
ca
=
match
ca
.
annot_content
with
|
AInvariant
(
_
,
b
,
_
)
->
b
|
_
->
false
in
let
l
=
Annotations
.
code_annot_emitter
~
filter
stmt
in
if
l
!=
[]
then
Loop_invariants_actions
.
extend
(
fun
()
->
List
.
iter
(
fun
(
ca
,
e
)
->
Annotations
.
remove_code_annot
e
~
kf
old
ca
;
Annotations
.
add_code_annot
e
~
kf
stmt
ca
)
l
)
let
preserve_invariant
env
kf
stmt
=
match
stmt
.
skind
with
|
Loop
(
_
,
({
bstmts
=
stmts
}
as
blk
)
,
loc
,
cont
,
break
)
->
let
rec
handle_invariants
(
stmts
,
env
,
_
as
acc
)
=
function
let
rec
handle_invariants
(
stmts
,
env
as
acc
)
=
function
|
[]
->
(* empty loop body: no need to verify the invariant twice *)
acc
...
...
@@ -80,16 +59,17 @@ let preserve_invariant env kf stmt = match stmt.skind with
let
blk
,
env
=
Env
.
pop_and_get
env
last
~
global_clear
:
false
Env
.
Before
in
Constructor
.
mk_block
last
blk
::
stmts
,
env
,
invariants
!=
[]
|
s
::
tl
->
handle_invariants
(
s
::
stmts
,
env
,
false
)
tl
Constructor
.
mk_block
last
blk
::
stmts
,
env
|
s
::
tl
->
handle_invariants
(
s
::
stmts
,
env
)
tl
in
let
env
=
Env
.
set_annotation_kind
env
Constructor
.
Invariant
in
let
stmts
,
env
,
has_loop
=
handle_invariants
([]
,
env
,
false
)
stmts
in
let
stmts
,
env
=
handle_invariants
([]
,
env
)
stmts
in
let
new_blk
=
{
blk
with
bstmts
=
List
.
rev
stmts
}
in
{
stmt
with
skind
=
Loop
([]
,
new_blk
,
loc
,
cont
,
break
)
}
,
env
,
has_loop
|
_
->
stmt
,
env
,
false
env
|
_
->
stmt
,
env
(**************************************************************************)
(**************************** Nested loops ********************************)
...
...
src/plugins/e-acsl/src/code_generator/loops.mli
View file @
5c56d8d7
...
...
@@ -28,18 +28,10 @@ open Cil_types
(************************* Loop invariants ********************************)
(**************************************************************************)
val
apply_after_transformation
:
unit
->
unit
val
mv_invariants
:
kernel_function
->
old
:
stmt
->
stmt
->
unit
(** Transfer the loop invariants from the [old] loop to the new one.
Both statements must be loops. *)
val
preserve_invariant
:
Env
.
t
->
Kernel_function
.
t
->
stmt
->
stmt
*
Env
.
t
*
bool
Env
.
t
->
Kernel_function
.
t
->
stmt
->
stmt
*
Env
.
t
(** modify the given stmt loop to insert the code which preserves its loop
invariants. Also return the modify environment and a boolean which
indicates whether the annotations corresponding to the loop invariant must
be moved from the new statement to the old one. *)
invariants. Also return the modify environment. *)
(**************************************************************************)
(**************************** Nested loops ********************************)
...
...
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