--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on December 2013 ---
Dear all, I add these three lines of code into the transfer.ml file for value analysis. The new transfer.ml file can be found in the attachment. (* value analysis *) Project.set_current prj; Globals.set_entry_point "main" true; !Db.Value.compute (); But Unexpected error was found in this line: Db.Value.compute (); The command I used here is: frama-c -load-script transfer.ml pfunc.c Could anybody help me out of this? Thank you very much. Error msgs is in below. -------------------------------------------------------------------------------------------------------------------- [kernel] preprocessing with "gcc -C -E -I. pfunc.c" Before transfering: /* Generated by Frama-C */ typedef int p_func(int *, int ); int main(p_func *func, int *arg1, int arg2) { int result; result = (*func)(arg1,arg2); return result; } [value] Analyzing an incomplete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization [kernel] Current source was: pfunc.c:8 The full backtrace is: Raised at file "src/kernel/globals.ml", line 261, characters 14-23 Called from file "src/project/state_builder.ml", line 556, characters 17-22 Called from file "src/value/eval_exprs.ml", line 1273, characters 39-68 Called from file "src/value/eval_stmt.ml", line 322, characters 27-76 Called from file "src/value/eval_slevel.ml", line 276, characters 38-47 Called from file "list.ml", line 74, characters 24-34 Called from file "src/value/eval_slevel.ml", line 346, characters 26-79 Called from file "cil/src/ext/dataflow.ml", line 294, characters 29-47 Called from file "cil/src/ext/dataflow.ml", line 461, characters 8-21 Called from file "cil/src/ext/dataflow.ml", line 465, characters 9-22 Called from file "src/value/eval_funs.ml", line 73, characters 9-32 Called from file "src/value/eval_funs.ml", line 278, characters 8-61 Called from file "src/value/eval_funs.ml", line 346, characters 10-110 Called from file "src/value/eval_funs.ml", line 564, characters 11-40 Re-raised at file "src/value/eval_funs.ml", line 580, characters 47-50 Called from file "src/project/state_builder.ml", line 839, characters 9-13 Re-raised at file "src/project/state_builder.ml", line 847, characters 15-18 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 732, characters 2-9 Called from file "src/kernel/cmdline.ml", line 212, characters 4-8 Unexpected error (Not_found). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Fluorine-20130601. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines -------------------------------------------------------------------------------------------------------------------- On 10 December 2013 12:01, David Yang <abiao.yang at gmail.com> wrote: > Dear Guillaume Petiot, > > Thank you so much. It helps a lot. > > I am sorry for any inconvenience for not carefully enough. > > I can do that now by adding this code, similar with using "-then-on". > Project.set_current prj; > > Additionally, whether could I achieve this by using the copy visitor? > > Thanks. > Best wishes, > -david > > On 10 December 2013 07:44, PETIOT Guillaume <Guillaume.PETIOT at cea.fr> wrote: >> Hi, >> >> You applied your transformation on the AST of project prj (called "transfer") when you did >> Project.on prj transform() >> >> but you call the Printer on the current project ("default"). So you have to replace the call to the Printer by something like >> Project.on prj (fun () -> >> Format.printf "\n\nAfter transfering:\n%a" Printer.pp_file (Ast.get ()) >> ) () >> So that the Ast.Get() will return the AST of project "transfer". >> >> >> You can also print the AST by invoking frama-c like this: frama-c -load-script transfer.ml pfunc.c -then-on transfer -print >> >> >> Regards. >> -- >> Guillaume Petiot, PhD student >> CEA LIST >> >> ________________________________________ >> From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] on behalf of David Yang [abiao.yang at gmail.com] >> Sent: Tuesday, December 10, 2013 3:47 AM >> To: Frama-C public discussion >> Subject: [Frama-c-discuss] how to modify stmt in AST by using a visitor >> >> Dear all, >> >> Inspired by Virgile 's insert_stmt script in this mailing list: >> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2012-March/003141.html >> >> I am writing a similar script to transform all call stmt of using >> function pointer to a regular call stmt. >> >> For example, in file "pfunc.c": >> /* --------------pfunc.c--------------------- */ >> typedef int p_func (int *, int); >> >> int main (p_func* func, int *arg1, int arg2) >> { >> int result; >> >> result = (*func)(arg1, arg2); >> >> return result; >> } >> /*-------------end----------------*/ >> >> the func variable is a function pointer type. I want transform this >> call to a regular call statement. >> >> The command I used here is : >> frama-c -load-script transfer.ml pfunc.c >> >> You could download this two files and then run these script directly >> as long as you has frama-c in your computer. >> >> Attached please find these two files for this command. >> >> But the ast file is not changed by this script. >> >> Is there anybody could help me fixing this problem? >> Thank you very much. >> >> PS: The frama-c version I used here is: Fluorine-20130601 >> >> All the best, >> -david >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- A non-text attachment was scrubbed... Name: transfer.ml Type: application/octet-stream Size: 1898 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131210/54e1b4ba/attachment.obj> -------------- next part -------------- A non-text attachment was scrubbed... Name: pfunc.c Type: text/x-csrc Size: 158 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131210/54e1b4ba/attachment.c>