Slicing with Frama-c

0
votes

I installed frama-c with opam on my MacOs. I need to slice Hello World by manually. I mean not with Gui. I searched on the internet but I could not understand how do it. My english is not well enough. So can somebody help me to slice HelloWorld.c ?

1
ocamlframa-cprogram-slicing
Unless you describe precisely what you did (i.e. source code HelloWorld.c and Frama-C's command line that has been use), the result you obtained and why it differs from what you expected, it will be difficult to give an appropriate answer. - Virgile

1 Answers

1
votes

To launch Frama-C's slicing from the command-line, you must have a C file that parses, and a slicing criterion (return code, accesses to a global variable, statement, etc). The various available criterion are described at http://frama-c.com/slicing.html.

Furthermore, if you want to slice e.g. on a statement, you will have to use slicing pragmas, with the following syntax:

/*@ slice pragma stmt; */
    Preserves the effects of the next statement. 
/*@ slice pragma expr e; */
    Preserves the value of the ACSL expression e at this control-flow point.