--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Could I determine whether a function is unsupported-function (such as: scanf, fscanf, sprintf, snprintf) by using the API?



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>