Frama-C-discuss mailing list archives

abiao.yang at gmail.com (David Yang) · Tue, 10 Dec 2013 15:30:31 +0000

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>