Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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