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

Remove obsolete debug code

parent 08a5f4ca
......@@ -197,23 +197,12 @@ let result_vi kf = match result_lhost kf with
(** {2 Handling the E-ACSL's C-libraries, part II} *)
(* ************************************************************************** *)
let mk_debug_mmodel_stmt stmt =
if Options.debug_atleast 1
&& Options.is_debug_key_enabled Options.dkey_analysis
then
let debug = mk_call ~loc:(Stmt.loc stmt) (mk_api_name "memory_debug") [] in
Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
else
stmt
let mk_full_init_stmt ?(addr=true) vi =
let loc = vi.vdecl in
let stmt = match addr, Cil.unrollType vi.vtype with
match addr, Cil.unrollType vi.vtype with
| _, TArray(_,Some _, _, _) | false, _ ->
mk_call ~loc (mk_api_name "full_init") [ Cil.evar ~loc vi ]
| _ -> mk_call ~loc (mk_api_name "full_init") [ Cil.mkAddrOfVi vi ]
in
mk_debug_mmodel_stmt stmt
let mk_initialize ~loc (host, offset as lv) = match host, offset with
| Var _, NoOffset -> mk_call ~loc
......@@ -229,14 +218,12 @@ let mk_named_store_stmt name ?str_size vi =
let ty = Cil.unrollType vi.vtype in
let loc = vi.vdecl in
let store = mk_call ~loc (mk_api_name name) in
let stmt = match ty, str_size with
match ty, str_size with
| TArray(_, Some _,_,_), None ->
store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
| TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
| _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
| _, Some _ -> assert false
in
mk_debug_mmodel_stmt stmt
let mk_store_stmt ?str_size vi =
mk_named_store_stmt "store_block" ?str_size vi
......@@ -246,17 +233,14 @@ let mk_duplicate_store_stmt ?str_size vi =
let mk_delete_stmt vi =
let loc = vi.vdecl in
let stmt = match Cil.unrollType vi.vtype with
match Cil.unrollType vi.vtype with
| TArray(_, Some _, _, _) ->
mk_call ~loc (mk_api_name "delete_block") [ Cil.evar ~loc vi ]
| _ -> mk_call ~loc (mk_api_name "delete_block") [ Cil.mkAddrOfVi vi ]
in
mk_debug_mmodel_stmt stmt
let mk_readonly vi =
let loc = vi.vdecl in
let stmt = mk_call ~loc (mk_api_name "readonly") [ Cil.evar ~loc vi ] in
mk_debug_mmodel_stmt stmt
mk_call ~loc (mk_api_name "readonly") [ Cil.evar ~loc vi ]
(* ************************************************************************** *)
(** {2 Other stuff} *)
......
......@@ -36,8 +36,6 @@ val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
such a function or if these functions were never registered (only possible
when using E-ACSL through its API. *)
val mk_debug_mmodel_stmt: stmt -> stmt
type annotation_kind =
| Assertion
| Precondition
......@@ -91,7 +89,7 @@ val reorder_ast: unit -> unit
val cty: logic_type -> typ
(* Assume that the logic type is indeed a C type. Just return it. *)
val ptr_index: ?index:Cil_types.exp -> Cil_types.exp
val ptr_index: ?index:Cil_types.exp -> Cil_types.exp
-> Cil_types.exp * Cil_types.exp
(** Split pointer-arithmetic expression of the type `p + i` into its
pointer and integer parts. *)
......
......@@ -114,8 +114,8 @@ class e_acsl_visitor prj generate = object (self)
val global_vars: init option Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
(* Hashtable mapping global variables (as Cil_type.varinfo) to their
initializers aiming to capture memory allocated by global variable
declarations and initilisation. At runtime the memory blocks corresponding
to space occupied by global are recorded via a call to
declarations and initialization. At runtime the memory blocks
corresponding to space occupied by global are recorded via a call to
[__gen_e_acsl_globals_init] instrumented at the beginning of the
[main] function. Each variable stored by [global_vars] will be handled in
the body of [__gen_e_acsl_globals_init] as follows:
......@@ -143,7 +143,7 @@ class e_acsl_visitor prj generate = object (self)
if generate then Project.copy ~selection ~src:cur prj;
Cil.DoChildrenPost
(fun f ->
(* extend the main with forward initialization and put it at end *)
(* extend [main] with forward initialization and put it at end *)
if generate then begin
let must_init =
not (Literal_strings.is_empty ())
......@@ -291,10 +291,10 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
Project.on prj build_initializer ()
end; (* must_init *)
(* Add a call to "__e_acsl_memory_init" that initializes memory
(* Add a call to [__e_acsl_memory_init] that initializes memory
storage and potentially records program arguments. Parameters to
the "__e_acsl_memory_init" are addresses of program arguments or
NULLs if main is declared without arguments. *)
[__e_acsl_memory_init] are addresses of program arguments or
NULLs if [main] is declared without arguments. *)
let build_mmodel_initializer () =
let loc = Location.unknown in
let nulls = [ Cil.zero loc ; Cil.zero loc ] in
......@@ -380,7 +380,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
else Cil.DoChildren
(* Add mappings from global variables to their initializers to [global_vars].
(* Add mappings from global variables to their initializers in [global_vars].
Note that the below function captures only [SingleInit]s. All compound
initializers (which contain single ones) are unrapped and thrown away. *)
method !vinit vi _off _i =
......@@ -390,7 +390,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Cil.DoChildrenPost
(fun i ->
(match is_initializer with
(* Note the use of [add] instead [replace]. This is because a
(* Note the use of [add] instead of [replace]. This is because a
single variable can be associated with multiple initializers
and all of them need to be captured. *)
| true -> Varinfo.Hashtbl.add global_vars vi (Some i)
......@@ -710,11 +710,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| Var vi, NoOffset -> vi.vglob || vi.vformal
| _ -> false
in
(* Options.feedback "%a? %a (%b && %b)"
Printer.pp_lval assigned_lv
Printer.pp_lval checked_lv
(not (may_safely_ignore assigned_lv))
(Pre_analysis.must_model_lval ~kf ~stmt checked_lv);*)
if not (may_safely_ignore assigned_lv) &&
Mmodel_analysis.must_model_lval ~kf ~stmt checked_lv
then
......@@ -722,8 +718,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* must be in the new project to build a new stmt *)
Project.on
prj
Misc.mk_debug_mmodel_stmt
(Misc.mk_initialize loc assigned_lv)
Misc.mk_initialize
(loc assigned_lv)
in
let before = Cil.memo_stmt self#behavior stmt in
let new_stmt = Cil.memo_stmt self#behavior new_stmt in
......
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