Skip to content
Snippets Groups Projects
Commit 1157b716 authored by Julien Signoles's avatar Julien Signoles
Browse files

[E-ACSL] code factorisation which improves translation of ghost stmts

parent 48d16df9
No related branches found
No related tags found
No related merge requests found
......@@ -7,6 +7,8 @@
- [Yannick] Logic functions
- [Nikola] temporal memory properties
- memory profiling
- [Guillaume] ajouter les annotations de RTE dans la table des annotations
(avec une option)
#####################
# E-ACSL CONSTRUCTS #
......
......@@ -90,10 +90,10 @@ int main(void)
int __e_acsl_valid;
__initialize((void *)P,sizeof(int));
__e_acsl_valid_read = __valid_read((void *)P,sizeof(int));
e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",(char *)"main",
e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(P)",16);
__e_acsl_valid = __valid((void *)P,sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
e_acsl_assert(__e_acsl_valid,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid(P)",16);
(*P) ++;
}
......
......@@ -102,10 +102,10 @@ int main(void)
int __e_acsl_valid;
__initialize((void *)P,sizeof(int));
__e_acsl_valid_read = __valid_read((void *)P,sizeof(int));
e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",(char *)"main",
e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(P)",16);
__e_acsl_valid = __valid((void *)P,sizeof(int));
e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
e_acsl_assert(__e_acsl_valid,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid(P)",16);
(*P) ++;
}
......
......@@ -637,9 +637,10 @@ and named_predicate_to_exp ?name kf ?rte env p =
let env = if rte then translate_rte kf env e else env in
e, env
and translate_rte kf env e =
let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
let l = get_rte kf stmt e in
and translate_rte_annots:
'a. (Format.formatter -> 'a -> unit) -> 'a ->
kernel_function -> Env.t -> code_annotation list -> Env.t =
fun pp elt kf env l ->
let old_valid = !is_visiting_valid in
let old_kind = Env.annotation_kind env in
let env = Env.set_annotation_kind env Misc.RTE in
......@@ -649,8 +650,7 @@ and translate_rte kf env e =
| AAssert(_, p) ->
handle_error
(fun env ->
Options.feedback ~dkey ~level:4 "prevent RTE from %a"
Printer.pp_exp e;
Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
translate_named_predicate kf (Env.rte env false) p)
env
| _ -> assert false)
......@@ -660,6 +660,11 @@ and translate_rte kf env e =
is_visiting_valid := old_valid;
Env.set_annotation_kind env old_kind
and translate_rte kf env e =
let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
let l = get_rte kf stmt e in
translate_rte_annots Printer.pp_exp e kf env l
and translate_named_predicate kf env p =
Options.feedback ~dkey ~level:3 "translating predicate %a"
Printer.pp_predicate_named p;
......
......@@ -35,6 +35,14 @@ val translate_post_code_annotation:
val translate_named_predicate:
kernel_function -> Env.t -> predicate named -> Env.t
val translate_rte_annots:
(Format.formatter -> 'a -> unit) ->
'a ->
kernel_function ->
Env.t ->
code_annotation list ->
Env.t
val predicate_to_exp: kernel_function -> predicate named -> exp
val set_original_project: Project.t -> unit
......
......@@ -460,13 +460,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
stmt.ghost <- false;
(* translate potential RTEs of ghost code *)
let rtes = get_rte_by_stmt kf stmt in
List.fold_left
(fun env a -> match a.annot_content with
| AAssert(_, p) ->
Translate.translate_named_predicate kf (Env.rte env false) p
| _ -> assert false)
env
rtes
Translate.translate_rte_annots Printer.pp_stmt stmt kf env rtes
end else
env
in
......@@ -522,11 +516,11 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let b, env =
Env.pop_and_get env stmt ~global_clear:true Env.After
in
if is_main && Pre_analysis.use_model () && generate then begin
if is_main && Pre_analysis.use_model () then begin
let stmts = b.bstmts in
let l = List.rev stmts in
match l with
| [] -> assert false (* return is here *)
| [] -> assert false (* at least the 'return' stmt *)
| ret :: l ->
let loc = Stmt.loc stmt in
let delete_stmts =
......@@ -548,7 +542,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
new_stmt, env
else
stmt, env
else
else (* i.e. not (is_return stmt) *)
if generate then
let stmt = rename_alloc_function stmt in
(* must generate [pre_block] which includes [stmt] before generating
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment