Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] about slicing

  • Subject: [Frama-c-discuss] about slicing
  • From: huizhanyi at gmail.com (Huizhan Yi)
  • Date: Mon, 12 Jan 2015 09:23:24 -0500
  • In-reply-to: <54B3BCDF.1090808@cea.fr>
  • References: <CAFZNyL7iNh+u1b-vG4Z3h_HxSE+M5s4c8oErQB=8J08+XhKLMA@mail.gmail.com> <54B3BCDF.1090808@cea.fr>
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>