title: Slicing using frama-c
body: <p>I'm using <strong>frama-c</strong> in order to do some experiments on program slicing. The tool is great and there are a lot of different types of slicing (by result or by statement, for example). I'm using a program data structure like:</p>
  
  <pre><code>typedef struct ComplexData {
      int x;
      int y;
      char string_[100];
      size_t n;
  } ComplexData;
  </code></pre>
  
  <p>It's just an example in order to understand how <em>frama-c</em> can slice the program by the result produced by the function. Basically, the <em>main</em> method calls a function which returns a value of the type <em>ComplexData</em>. <strong>How the comparison between different executions is performed? There is a check for each value of the struct?</strong> Like <a href="http://latex.codecogs.com/gif.latex?x_1%20%3D%20x_2%20%5C%20%5Cwedge%20%5C%20y_1%20%3D%20y_2%20%5C%20%5Cwedge%20%5C%20string%20%3D%20string%5E%7B%27%7D%20%5C%20%5Cwedge%20%5C%20n_1%20%3D%20n_2" rel="nofollow noreferrer">this</a>?</p>