Frama-C-discuss mailing list archives

huizhanyi at gmail.com (Huizhan Yi) · Mon, 12 Jan 2015 12:07:53 -0500

*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>