--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] about slicing



Hi,

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?


TrustInSoft Analyzer is a distribution of Frama-C extended with proprietary plugins and tools that increase the productivity and lower the cost of the industrial deployments.
It comes with a full set of professional support services. You may ask for more details at contact at trust-in-soft.com<mailto:contact at trust-in-soft.com>.

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

This is not a function : this is a command line tool : as explained above, ?it generates the proper filesystem stubs: an existing in.pbm file with an arbitrary content and an empty out.pbm file?.

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

Yes : it generates tis_main and and the call to the original 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?

tis-analyzer is a superset of 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.

I mean exactly what I have written above : you will not be able to analyze the source code with frama-c. Just read this code to understand what it does.

Regards,
Benjamin Monate
TrustInSoft Founder&CTO
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150113/bd840d13/attachment.html>