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

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>