Commit 6204e457 authored by Julien Signoles's avatar Julien Signoles
Browse files

[temporal] restore proper behavior through Temporal.is_enable

[translate] remove useless function from its API
parent feed4619
......@@ -30,6 +30,10 @@ module Libc = Functions.Libc
open Cil_types
open Cil_datatype
let generate = ref false
let enable param = generate := param
let is_enabled () = !generate
(* ************************************************************************** *)
(* Types {{{ *)
(* ************************************************************************** *)
......@@ -490,7 +494,7 @@ let mk_global_init ~loc vi off init env =
(* ************************************************************************** *)
let handle_function_parameters kf env =
if Options.Temporal_validity.get () then
if is_enabled () then
let env, _ = List.fold_left
(fun (env, index) param ->
let param = Visitor_behavior.Get.varinfo (Env.get_behavior env) param in
......@@ -506,7 +510,7 @@ let handle_function_parameters kf env =
env
let handle_stmt stmt env =
if Options.Temporal_validity.get () then begin
if is_enabled () then begin
match stmt.skind with
| Instr instr -> handle_instruction stmt instr env
| Return(ret, loc) -> Extlib.may_map
......@@ -518,7 +522,7 @@ let handle_stmt stmt env =
env
let generate_global_init vi off init env =
if Options.Temporal_validity.get () then
if is_enabled () then
mk_global_init ~loc:vi.vdecl vi off init env
else
None
......
......@@ -23,6 +23,12 @@
(** Transformations to detect temporal memory errors (e.g., dereference of
stale pointers). *)
val enable: bool -> unit
(** Enable/disable temporal transformations *)
val is_enabled: unit -> bool
(** Return a boolean value indicating whether temporal analysis is enabled *)
val handle_function_parameters: Cil_types.kernel_function -> Env.t -> Env.t
(** [handle_function_parameters kf env] updates the local environment [env],
according to the parameters of [kf], with statements allowing to track
......
......@@ -954,9 +954,6 @@ let assumes_predicate bhv =
Logic_const.ptrue
bhv.b_assumes
let original_project_ref = ref Project_skeleton.dummy
let set_original_project p = original_project_ref := p
let translate_preconditions kf env behaviors =
let env = Env.set_annotation_kind env Misc.Precondition in
let do_behavior env b =
......
......@@ -48,8 +48,6 @@ val term_to_exp: typ option -> term -> exp
val predicate_to_exp: kernel_function -> predicate -> exp
val set_original_project: Project.t -> unit
(*
Local Variables:
compile-command: "make -C ../.."
......
......@@ -1031,8 +1031,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Literal_strings.reset ();
Global_observer.reset ();
Keep_status.before_translation ();
self#reset_env ();
Translate.set_original_project (Project.current ())
self#reset_env ()
end
......
......@@ -146,49 +146,53 @@ let () =
let generate_code =
Resulting_projects.memo
(fun name ->
apply_on_e_acsl_ast
(fun () ->
Options.feedback "beginning translation.";
let prepared_prj = Prepare_ast.prepare () in
let res =
Project.on prepared_prj
(fun () ->
let dup_prj = Dup_functions.dup () in
let res =
Project.on
dup_prj
(fun () ->
Gmp_types.init ();
Mmodel_analysis.reset ();
let visit prj = Visit.do_visit ~prj true in
let prj = File.create_project_from_visitor name visit in
Loops.apply_after_transformation prj;
(* remove the RTE's results computed from E-ACSL: their are
partial and associated with the wrong kernel function
(the one of the old project). *)
let selection =
State_selection.with_dependencies !Db.RteGen.self
in
Project.clear ~selection ~project:prj ();
Resulting_projects.mark_as_computed ();
Project.copy
~selection:(State_selection.singleton Kernel.Files.self)
prj;
prj)
apply_on_e_acsl_ast
(fun () ->
Options.feedback "beginning translation.";
Temporal.enable (Options.Temporal_validity.get ());
let prepared_prj = Prepare_ast.prepare () in
let res =
Project.on prepared_prj
(fun () ->
let dup_prj = Dup_functions.dup () in
let res =
Project.on
dup_prj
(fun () ->
Gmp_types.init ();
Mmodel_analysis.reset ();
let visit prj = Visit.do_visit ~prj true in
let prj =
File.create_project_from_visitor name visit
in
Loops.apply_after_transformation prj;
(* remove the RTE's results computed from E-ACSL:
their are partial and associated with the wrong
kernel function (the one of the old project). *)
let selection =
State_selection.with_dependencies !Db.RteGen.self
in
Project.clear ~selection ~project:prj ();
Resulting_projects.mark_as_computed ();
let selection =
State_selection.singleton Kernel.Files.self
in
Project.copy ~selection prj;
prj)
()
in
if Options.Debug.get () = 0 then
Project.remove ~project:dup_prj ();
res)
()
in
if Options.Debug.get () = 0 then
Project.remove ~project:dup_prj ();
res)
()
in
if Options.Debug.get () = 0 then begin
Project.remove ~project:prepared_prj ();
end;
Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ());
res)
())
in
if Options.Debug.get () = 0 then begin
Project.remove ~project:prepared_prj ();
end;
Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ());
res)
())
let generate_code =
Dynamic.register
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment