--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2014 ---
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