Frama-C-discuss mailing list archives

benjamin.monate at trust-in-soft.com (Benjamin Monate) · Mon, 12 Jan 2015 16:29:02 +0000

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:

# 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

# 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.pbm

# 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"

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.

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<mailto: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 list
Frama-c-discuss at lists.gforge.inria.fr<mailto: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<mailto: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/c5840cca/attachment-0001.html>
-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: slice.i
Type: application/octet-stream
Taille: 27636 octets
Desc: slice.i
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150112/c5840cca/attachment-0001.obj>