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: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Mon, 12 Jan 2015 13:23:59 +0100
  • In-reply-to: <CAFZNyL7iNh+u1b-vG4Z3h_HxSE+M5s4c8oErQB=8J08+XhKLMA@mail.gmail.com>
  • References: <CAFZNyL7iNh+u1b-vG4Z3h_HxSE+M5s4c8oErQB=8J08+XhKLMA@mail.gmail.com>
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 list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150112/12d29f6e/attachment.html>