Commit d47813a3 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:archi] move functions from E-ACSL to Kernel_function

parent a0816617
...@@ -559,10 +559,27 @@ let is_definition kf = ...@@ -559,10 +559,27 @@ let is_definition kf =
| Definition _ -> true | Definition _ -> true
| Declaration _ -> false | Declaration _ -> false
let is_first_stmt kf stmt =
try
let first = find_first_stmt kf in
Stmt.equal stmt first
with No_Statement ->
false
let is_return_stmt kf stmt =
try
let return = find_return kf in
Stmt.equal stmt return
with No_Statement -> false
let is_entry_point kf = let is_entry_point kf =
let main, _ = Globals.entry_point () in let main, _ = Globals.entry_point () in
equal kf main equal kf main
let is_main kf =
let name = get_name kf in
Datatype.String.equal name "main"
let returns_void kf = let returns_void kf =
let result_type,_,_,_ = Cil.splitFunctionType (get_type kf) in let result_type,_,_,_ = Cil.splitFunctionType (get_type kf) in
match Cil.unrollType result_type with match Cil.unrollType result_type with
......
...@@ -183,8 +183,23 @@ val is_entry_point: t -> bool ...@@ -183,8 +183,23 @@ val is_entry_point: t -> bool
option -main). option -main).
@since Sodium-20150201 *) @since Sodium-20150201 *)
val is_main: t -> bool
(** @return true iff the given function is the function called 'main' in the
program.
@since Frama-C+dev *)
val returns_void : t -> bool val returns_void : t -> bool
val is_first_stmt: t -> stmt -> bool
(** @return true iff the statement is the first statement of the given
function.
@since Frama-C+dev *)
val is_return_stmt: t -> stmt -> bool
(** @return true iff the statement is the return statement of the given
function.
@since Frama-C+dev *)
(* ************************************************************************* *) (* ************************************************************************* *)
(** {2 Getters} *) (** {2 Getters} *)
(* ************************************************************************* *) (* ************************************************************************* *)
......
...@@ -442,14 +442,8 @@ let register_predicate kf pred state = ...@@ -442,14 +442,8 @@ let register_predicate kf pred state =
branch (not considering the exception handlers) *) branch (not considering the exception handlers) *)
let doStmt stmt = let doStmt stmt =
let _, kf = Kernel_function.find_from_sid stmt.sid in let _, kf = Kernel_function.find_from_sid stmt.sid in
let is_first = let is_first = Kernel_function.is_first_stmt kf stmt in
try Stmt.equal stmt (Kernel_function.find_first_stmt kf) let is_last = Kernel_function.is_return_stmt kf stmt in
with Kernel_function.No_Statement -> assert false
in
let is_last =
try Stmt.equal stmt (Kernel_function.find_return kf)
with Kernel_function.No_Statement -> assert false
in
Dataflow.Post Dataflow.Post
(fun state -> (fun state ->
let state = Env.default_varinfos state in let state = Env.default_varinfos state in
......
...@@ -26,23 +26,6 @@ open Cil_datatype ...@@ -26,23 +26,6 @@ open Cil_datatype
let dkey = Options.dkey_translation let dkey = Options.dkey_translation
(* ************************************************************************** *)
(* Utilities *)
(* ************************************************************************** *)
(* [TODO ARCHI] move it in another module *)
let is_main kf =
Datatype.String.equal (Kernel_function.get_name kf) "main"
(* [TODO ARCHI] move it *)
let is_first_stmt kf stmt =
try Stmt.equal stmt (Kernel_function.find_first_stmt kf)
with Kernel_function.No_Statement -> assert false
let is_return_stmt kf stmt =
try Stmt.equal stmt (Kernel_function.find_return kf)
with Kernel_function.No_Statement -> assert false
(* ************************************************************************** *) (* ************************************************************************** *)
(* Code *) (* Code *)
(* ************************************************************************** *) (* ************************************************************************** *)
...@@ -264,7 +247,7 @@ let add_new_block_in_stmt env kf stmt = ...@@ -264,7 +247,7 @@ let add_new_block_in_stmt env kf stmt =
(* Remove local variables which scopes ended via goto/break/continue. *) (* Remove local variables which scopes ended via goto/break/continue. *)
let del_vars = Exit_points.delete_vars stmt in let del_vars = Exit_points.delete_vars stmt in
let env = Memory_observer.delete_from_set ~before:stmt env kf del_vars in let env = Memory_observer.delete_from_set ~before:stmt env kf del_vars in
if is_return_stmt kf stmt then if Kernel_function.is_return_stmt kf stmt then
let env = let env =
if Functions.check kf then if Functions.check kf then
(* must generate the post_block before including [stmt] (the (* must generate the post_block before including [stmt] (the
...@@ -287,7 +270,7 @@ let add_new_block_in_stmt env kf stmt = ...@@ -287,7 +270,7 @@ let add_new_block_in_stmt env kf stmt =
let b, env = let b, env =
Env.pop_and_get env new_stmt ~global_clear:true Env.After Env.pop_and_get env new_stmt ~global_clear:true Env.After
in in
if is_main kf && Mmodel_analysis.use_model () then begin if Kernel_function.is_main kf && Mmodel_analysis.use_model () then begin
let stmts = b.bstmts in let stmts = b.bstmts in
let l = List.rev stmts in let l = List.rev stmts in
match l with match l with
...@@ -443,9 +426,9 @@ and inject_in_stmt env kf stmt = ...@@ -443,9 +426,9 @@ and inject_in_stmt env kf stmt =
in in
(* initial environment *) (* initial environment *)
let env = let env =
if is_first_stmt kf stmt then if Kernel_function.is_first_stmt kf stmt then
let env = let env =
if is_main kf then if Kernel_function.is_main kf then
env env
else else
let env = let env =
...@@ -514,7 +497,7 @@ and inject_in_block (env: Env.t) kf blk = ...@@ -514,7 +497,7 @@ and inject_in_block (env: Env.t) kf blk =
(* keep the return (enclosed in a generated block) at the end; (* keep the return (enclosed in a generated block) at the end;
preceded by clean if any *) preceded by clean if any *)
let init, tl = let init, tl =
if is_main kf && Mmodel_analysis.use_model () then if Kernel_function.is_main kf && Mmodel_analysis.use_model () then
free_stmts @ [ potential_clean; ret ], tl free_stmts @ [ potential_clean; ret ], tl
else else
free_stmts @ [ ret ], l free_stmts @ [ ret ], l
...@@ -588,7 +571,7 @@ let inject_in_fundec main fundec = ...@@ -588,7 +571,7 @@ let inject_in_fundec main fundec =
Builtins.update vi.vname vi; Builtins.update vi.vname vi;
(* track function addresses but the main function that is tracked internally (* track function addresses but the main function that is tracked internally
via RTL *) via RTL *)
if not (is_main kf) then Global_observer.add vi; if not (Kernel_function.is_main kf) then Global_observer.add vi;
(* exit point computations *) (* exit point computations *)
if Functions.instrument kf then Exit_points.generate fundec; if Functions.instrument kf then Exit_points.generate fundec;
Options.feedback ~dkey ~level:2 "entering in function %a." Options.feedback ~dkey ~level:2 "entering in function %a."
...@@ -599,7 +582,7 @@ let inject_in_fundec main fundec = ...@@ -599,7 +582,7 @@ let inject_in_fundec main fundec =
add_generated_variables_in_function env fundec; add_generated_variables_in_function env fundec;
add_malloc_and_free_stmts kf fundec; add_malloc_and_free_stmts kf fundec;
(* setting main if necessary *) (* setting main if necessary *)
let main = if is_main kf then Some fundec else main in let main = if Kernel_function.is_main kf then Some fundec else main in
Options.feedback ~dkey ~level:2 "function %a done." Options.feedback ~dkey ~level:2 "function %a done."
Kernel_function.pretty kf; Kernel_function.pretty kf;
env, main env, main
......
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