--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] about slicing



Thank you for your reply.
Here is another example from susan.c
I run with command line:
frama-c -slice-calls put_image susan.c -then-on "Slicing export" -print

I wish get a slice related with the parameter "in", why I get nothing?

the attached file is susan.c and run log file.

There is any general instruction to solve how to extract a slice and avoid
wrongly using the slicer?


*Huizhan Yi,*
Associate Professor, College of Computer, National University of Defense
Technology,China
Work Phone: 0731-84574650
WeiXin Num: huizhanyi
QQ Num?562538519

On Mon, Jan 12, 2015 at 7:23 AM, BAUDIN Patrick <Patrick.Baudin at cea.fr>
wrote:

>  Hi,
> The given slice is correct: the Slicing plug-in ensures that, each time
> the function main terminates in the original code, it terminates in the
> sliced code and preserves the effects of the call.
> Since the function mains never terminate, it can do what it wants, and
> nothing is the more reduced slice.
> The explanation is given into these messages:
>    [pdg] computing for function main
>    bts1445.i:10:[pdg] warning: no final state. Probably unreachable...
>    [pdg] done for function main
>    [slicing] Nothing to select for unreachable return stmt of main
> Regards,
> -- Patrick Baudin
>
> Le 19/12/2014 17:45, Huizhan Yi a ?crit :
>
>  Hi
>  I am working program slicing with frama-c. I compile and install
> frama-c-Neon-20140301.  When I test some toy applications in the
> frama-c-Neon-20140301/tests/slicing, I find some problem. for example, such
> as the bts1445.i, the result log is
>
> [slicing] slicing requests in progress...
> [value] Analyzing a complete application starting at main
> [value] Computing initial state
> [value] Initial state computed
> [value] Values of globals at initialization
>   x ? {0}
> tests/slicing/bts1445.i:8:[value] entering loop for the first time
> [value] Recording results for main
> [value] done for function main
> [slicing] making slicing project 'Slicing'...ensures that, each time the
> function f terminates in the original code, it terminates in the sliced
> code
>
> [slicing] interpreting slicing requests from the command line...
> [slicing] warning: No internal slicing request from the command line.
> [slicing] warning: Adding an extra request on the entry point of function:
> main.
> [pdg] computing for function main
> tests/slicing/bts1445.i:10:[pdg] warning: no final state. Probably
> unreachable...
> [pdg] done for function main
> [slicing] applying all slicing requests...
> [slicing] applying 1 actions...
> [slicing] applying actions: 1/1...
> [slicing] exporting project to 'Slicing export'...
> [slicing] applying all slicing requests...
> [slicing] applying 0 actions...
> [sparecode] remove unused global declarations from project 'Slicing export
> tmp'
> [sparecode] removed unused global declarations in new project 'Slicing
> export'
> /* Generated by Frama-C */
> void main(void)
> {
>   return;
> }
>
>  It seems that I do not get correct slice for main function.
>
>  I try to slice it with
> frama-c -slice-calls main bts1445.i -then-on "Slicing export" -print
>  It is the same result.
>
>  The source code for bts1445.i is
> /*  run.config
> OPT: -check -slice-calls main -then-on "Slicing export" -print
> OPT: -check -slice-calls f -main f -then-on "Slicing export" -print
> */
> int x = 0;
>
> int main() {
>   while(1)
>     x=0;
>   return x + 1;
> }
>
> int f() {
>   while(1)
>     x=0;
>   return x + 1;
> }
>
>  I think that a right slice is
>
> int x = 0;
>
> int main() {
>   while(1)
>     x=0;
>   return x + 1;
> }
>
>  Why is there the problem? There is any method to solve it?
>
>      *Huizhan Yi,*
> Associate Professor, College of Computer, National University of Defense
> Technology,China
>  Work Phone: 0731-84574650
> WeiXin Num: huizhanyi
> QQ Num?562538519
>
>
> _______________________________________________
> Frama-c-discuss mailing listFrama-c-discuss at lists.gforge.inria.frhttp://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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150112/74afa7ee/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: susan.c
Type: text/x-csrc
Size: 59758 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150112/74afa7ee/attachment-0001.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: susan.log
Type: text/x-log
Size: 229680 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150112/74afa7ee/attachment-0001.bin>