--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on January 2015 ---
*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 11:29 AM, Benjamin Monate < benjamin.monate at trust-in-soft.com> wrote: > Hi, > > You have to perform a proper value analysis before trying to slice your > code. > Reading the Value Analysis manual will help: > http://frama-c.com/download/value-analysis-Neon-20140301.pdf > <http://frama-c.com/download/value-analysis-Neon-20140301.pdf.> > Your source code is using the C standard library and relies on the command > line arguments (argc,argv). > This kind of not self-contained code needs to be analyzed within a proper > environment. > You may write it this environment by hand but you need to have a bit of > experience with simpler example before-hand. > > Just to show you an example, I have done this on your code using some of > the tools bundled with Frama-C within its TrustInSoft Analyzer distribution: > What is TrustInSoft Analyzer? it is a C standard library? > > # First we generate the proper filesystem stubs: an existing in.pbm file > with an arbitrary content and an empty out.pbm file > monate at TrustInSoft-III:~/BUGS/susan$ tis-mkfs -add-file in.pbm > -nb-max-files 6 -generic out.pbm:1:0:0 > What specific function is tis-mkfs? > > # Then we generate generate the calling environment: only two arguments > : in.pbm followed by out.pbm > monate at TrustInSoft-III:~/BUGS/susan$ tis-mk-main -f -- in.pbm out.pb > Here the tis-mk-main add the call tis_main->main? > > # The we run your slicing command > monate at TrustInSoft-III:~/BUGS/susan$ tis-analyzer -main tis_main > -slice-calls put_image susan.c tis-main-dummy.c mkfs_filesystem.c > /home/tis/share/tis/__tis_mkfs.c -then-on "Slicing export" > tis-analyzer has the same function as frama-c? > > And we obtain the attached slice.i file. > You will probably not be able to analyze slice.i with the Open Source > version of Frama-C as the sliced code relies on specific builtins to handle > dynamic allocation. > You mean I cannot compile the slice.i code since it depend on some internal library. > > Note that I had to fix two bugs in your code to obtain this result: the > function get_image and put_image are declared as returning an int but have > no return statement. > > Hope this helps, > Benjamin > > ------------------------------ > *De :* Frama-c-discuss <frama-c-discuss-bounces at lists.gforge.inria.fr> de > la part de Huizhan Yi <huizhanyi at gmail.com> > *Envoy? :* lundi 12 janvier 2015 15:23 > *? :* Frama-C public discussion > *Objet :* Re: [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 >> > > > _______________________________________________ > 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/a50dfe1f/attachment.html>