Frama-C-discuss mailing list archives

abiao.yang at gmail.com (David Yang) · Wed, 11 Dec 2013 17:38:34 +0000

Dear Boris,

Thank you so much for your prompt reply and such useful code.

It's very very useful for me. I am so sorry for this inconvenient for
wasting your time to debug my code since this is my first time to
transform AST.

Thanks again.

All the best.
-david

On 11 December 2013 17:18, Boris Yakobowski <boris at yakobowski.org> wrote:
> Hi,
>
> There are many problems with your code. First, you should use a single
> copy visitor. This is simpler and less error-prone than creating a
> copy of the AST that you mutate later, as you are currently doing.
> Second, you are not registering the new function you are creating as a
> kernel_function, which explains the crash. Finally, you are not
> creating varinfos for the formal arguments of the new function, which
> is probably not a good idea. (And finally you should override
> vstmt_aux, not vstmt.)
>
> I've updated your code for the first two points. The third one remains
> to be done, but should be less complex. You can probably find some
> inspiration in file frama-c/src/misc/filter.ml, in the method
> build_proto.
>
> HTH,
>
>
> On Tue, Dec 10, 2013 at 4:30 PM, David Yang <abiao.yang at gmail.com> wrote:
>> 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
>>
>> _______________________________________________
>> 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
>
>
>
> --
> Boris
>
> _______________________________________________
> 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