--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on August 2013 ---
While I output the state (the table of value analysis) of each statement within a function by using the module: Db.Value.Table . I recognized that while a statement is unreachable (invalid pointer or call a unsupported-function) , the state of the statement is "NO INFORMATION". I use the following code to output the state of each statement in a function: let output_fundec_state (fundec:Cil_types.fundec) (fmt:Format.formatter) = Format.fprintf fmt "\nState of Function %s with the module Db.Value.Table." fundec.svar.vname; List.iter (fun astmt -> let state = Db.Value.get_stmt_state astmt in Format.fprintf fmt "\nStatement: "; Printer.pp_stmt fmt astmt; Format.fprintf fmt "\nState:"; Db.Value.pretty_state fmt state; ) fundec.sallstmts; ;; So i was wondering if I could use this information to determine the unsupported functions? Kind regards Yours sincerely David -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130827/a7b09a99/attachment.html>