Commit a843e683 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Handling declarations in the bodies of switch statements

parent ae883b2d
......@@ -58,6 +58,7 @@ PLUGIN_CMO:= local_config \
gmpz \
literal_strings \
mmodel_analysis \
prepare_ast \
dup_functions \
exit_points \
label \
......
......@@ -25,7 +25,7 @@ let check () =
let t = Error.nb_untypable () in
let n = Error.nb_not_yet () in
let print msg n =
Options.result "@[%d annotation%s %s ignored,@ being %s.@]"
Options.result "@[%d annotation%s %s ignored,@ being %s.@]"
n
(if n > 1 then "s" else "")
(if n > 1 then "were" else "was")
......@@ -75,26 +75,26 @@ let unmemoized_extend_ast () =
Options.feedback ~level:2 "AST already computed: \
E-ACSL is going to work on a copy.";
let name = Project.get_name (Project.current ()) in
let tmpfile =
let tmpfile =
Extlib.temp_file_cleanup_at_exit ("e_acsl_" ^ name) ".i" in
let cout = open_out tmpfile in
let fmt = Format.formatter_of_out_channel cout in
File.pretty_ast ~fmt ();
let selection =
let selection =
State_selection.diff
State_selection.full
(State_selection.with_dependencies Ast.self)
State_selection.full
(State_selection.with_dependencies Ast.self)
in
let prj =
Project.create_by_copy
~last:false
~selection
(Format.asprintf "%s for E-ACSL" name)
~selection
(Format.asprintf "%s for E-ACSL" name)
in
Project.on prj
(fun () ->
Kernel.Files.set [ tmpfile ];
extend ())
Kernel.Files.set [ tmpfile ];
extend ())
();
Some prj
end else begin
......@@ -103,7 +103,7 @@ E-ACSL is going to work on a copy.";
end
let extend_ast () = match !extended_ast_project with
| To_be_extended ->
| To_be_extended ->
let prj = unmemoized_extend_ast () in
extended_ast_project := Already_extended prj;
(match prj with
......@@ -147,6 +147,8 @@ let generate_code =
apply_on_e_acsl_ast
(fun () ->
Options.feedback "beginning translation.";
let prepared_prj = Prepare_ast.prepare () in
Project.set_current prepared_prj;
let dup_prj = Dup_functions.dup () in
let res =
Project.on
......@@ -157,9 +159,9 @@ let generate_code =
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). *)
(* 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). *)
Project.clear
~selection:(State_selection.with_dependencies !Db.RteGen.self)
~project:prj
......@@ -171,7 +173,10 @@ let generate_code =
prj)
()
in
if Options.Debug.get () = 0 then Project.remove ~project:dup_prj ();
if Options.Debug.get () = 0 then begin
Project.remove ~project:prepared_prj ();
Project.remove ~project:dup_prj ()
end;
Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ());
res)
......@@ -194,7 +199,7 @@ let predicate_to_exp =
Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
Translate.predicate_to_exp
let add_e_acsl_library _files =
let add_e_acsl_library _files =
if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
(* extending the AST as soon as possible reduce the amount of time the AST is
......
(**************************************************************************)
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2012-2016 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file license/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Cil_types
class prepare_visitor prj = object (_)
inherit Visitor.frama_c_copy prj
method !vstmt_aux _ =
Cil.DoChildrenPost (fun stmt ->
match stmt.skind with
| Switch(_,sw_blk,_,_) ->
let new_blk = Cil.mkBlock [ stmt ] in
let new_stmt = Cil.mkStmt (Block new_blk) in
new_blk.blocals <- sw_blk.blocals;
sw_blk.blocals <- [];
new_stmt
| _ -> stmt)
initializer
Project.copy ~selection:(Parameter_state.get_selection ()) prj
end
let prepare () =
Options.feedback ~level:2 "prepare AST for E-ACSL transformations";
File.create_project_from_visitor
"e_acsl_prepare_ast"
(new prepare_visitor)
(**************************************************************************)
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2012-2016 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file license/LGPLv2.1). *)
(* *)
(**************************************************************************)
(** Prepare AST for E-ACSL generation.
* So for this mudule performs the only task:
* - Move declarations of variables declared in the bodies of switch
* statements to upper scopes.
*)
val prepare: unit -> Project.t
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
int main(int argc, char **argv)
{
int __retres;
__e_acsl_memory_init(& argc,& argv,8UL);
__e_acsl_store_block((void *)(& argc),4UL);
{
int *p;
__e_acsl_store_block((void *)(& p),8UL);
switch (argc) {
default: ;
__e_acsl_full_init((void *)(& p));
p = & argc;
break;
}
__e_acsl_delete_block((void *)(& p));
}
__retres = 0;
__e_acsl_delete_block((void *)(& argc));
__e_acsl_memory_clean();
return __retres;
}
......@@ -468,28 +468,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
method private add_delete_stmt ?before env kf vars =
self#add_tracking_fn Misc.mk_delete_stmt ?before env kf vars
(* Abort the execution if E-ACSL is required to monitor a variable
declared within a body of a switch statement. In the present setup
[store_block] will be added after the definition of such variable
and ignored by the executing program, which in turn will lead to
inconsistent tracking state. *)
method private check_switch_declarations stmt kf =
match stmt with
| { skind = Switch(_,blk,_,_) } when List.length blk.blocals > 0 ->
List.iter
(fun vi ->
if Mmodel_analysis.must_model_vi ~kf vi; then begin
Options.error "Variable %s at %a declared in the body of a switch \
statement.\nExecition of a monitored program will fail.\nConsider removing \
such variables of use -simplify-cfg flag of Frama-C to bypass them."
vi.vname
Printer.pp_location vi.vdecl;
assert false
end else
())
blk.blocals
| _ -> ()
method !vstmt_aux stmt =
Options.debug ~level:4 "proceeding stmt (sid %d) %a@."
stmt.sid Stmt.pretty stmt;
......@@ -544,9 +522,6 @@ such variables of use -simplify-cfg flag of Frama-C to bypass them."
let env = self#add_duplicate_store_stmt ~before:stmt env kf duplicates in
function_env := env;
(* Make there are no variables to monitor declared in switches *)
self#check_switch_declarations stmt kf;
let mk_block stmt =
(* be careful: since this function is called in a post action, [env] has
been modified from the time where pre actions have been executed.
......
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