Frama-C-discuss mailing list archives

boris at yakobowski.org (Boris Yakobowski) · Wed, 11 Dec 2013 18:18:34 +0100

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: transfer.ml
Type: text/x-ocaml
Size: 3092 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131211/898b5e86/attachment.bin>