--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Could I get the statement that caused the dead code programatically?



Dear all,

I found two functions in Db.Value:

(* access the cvalue.v before a statement *)
let cv_bef = !Db.Value.access Cil_types.Kstmt(stmt) lval in
(* access the cvalue.v after a statement *)
let cv_aft  = !Db.Value.access_after Cil_types.Kstmt(stmt) lval in

besides, there is another function without any description:
Cvalue.V.is_bottom cv

If the value of lval is not bottom before a statement and is bottom
after the statement, whether this statement is the statement that
caused other statements to be dead code?

Thanks,
-david

The code for detecting the statement is:

List.iter
(fun stmt ->
    let lvals = Visitor_util.get_stmt_lvals stmt in
    List.iter
    (fun lval ->
        let loc = !Db.Value.lval_to_loc Cil_types.Kglobal
CilE.warn_none_mode lval in

        try
            let cv_bef = !Db.Value.access (Cil_types.Kstmt(stmt)) lval in
            let cv_aft = !Db.Value.access_after (Cil_types.Kstmt(stmt)) lval in

            if (not (Cvalue.V.is_bottom cv_bef)) &&
(Cvalue.V.is_bottom cv_aft) then begin
                Self.result "stmt %a @." Printer.pp_stmt stmt;
            end
        with
        | err -> Self.result "[try-catch]Error: %s while access_after
lval(%a) ." (Printexc.to_string err) Printer.pp_lval lval;
    ) lvals;
) fundec.sallstmts;

On 5 January 2014 01:25, David Yang <abiao.yang at gmail.com> wrote:
> Dear all,
>
> I want to programatically get the statement(Cil_types.stmt)  or the
> expression (Cil_types.expr) or the left value (Cil_types.lval) that
> caused other statement to be dead code in value analysis.
>
> For example, if a function has the following three kinds of
> statements, those statements after these three statements are detected
> to be dead code from value analysis result.
> 1. y = a[8] + 6; /* assume the memory access is out of bounds */
> 2. if(0) {..}
> 3. x = k + 5; /* k is not initialized. */
>
> How can I programatically get these statements by using the Db.Value.
> state information or the Cvalue.V.t information or the Locations
> information?
>
> The API document lacks detail description for the abstract
> interpretation related API functions. Could it possible to add some
> description for these functions in later frama-c release?
>
> Thank you very much.
>
> -david