Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Frama-C is an Open Source static analysis platform with <a href="http://frama-c.com/slicing.html" rel="nofollow noreferrer">a slicer for C programs</a> based on the computation of a Program Dependence Graph.</p> <p>Note that slicing actual programs written in a real programming language such as C involves many special cases and concepts that are skimmed over in scientific publications. Still, I am confident that you won't find anything simpler than Frama-C's PDG computation, first because it is the only Open Source one available (that I know of), and second because any other PDG computation that handled C programs would have to solve the same problems and introduce the same concepts.</p> <p>Here is one example:</p> <pre><code>int a, b, d, *p; int f (int x) { return a + x; } int main (int c, char **v) { p = &amp;b; a = 1; *p = 2; d = 3; c = f(b); } </code></pre> <p>The command <code>frama-c -pdg -pdg-dot graph -pdg-print t.c</code> generates dot files <code>graph.main.dot</code> and <code>graph.f.dot</code> containing the PDG of <code>main()</code> and <code>f()</code> respectively.</p> <p>You can use the <code>dot</code> program to pretty-print one of them thus: <code>dot -Tpdf graph.main.dot &gt; graph.pdf</code></p> <p>The result is below:</p> <p><img src="https://i.stack.imgur.com/LVWYZ.png" alt="PDG of main()"></p> <p>Note the edge from the node <code>c = f(b);</code> to the node <code>*p = 2;</code>. A PDG computation claiming to be useful for C programs must handle aliasing.</p> <p>On the other hand, a slicer using this PDG to slice on the criterion “inputs of statement <code>c = f(b);</code>” would be able to remove <code>d = 3;</code>, which cannot influence the function call, even through the pointer access <code>*p</code>. Frama-C's slicer uses the dependencies indicated by the PDG to keep only the statements that are useful for the user-specified slicing criterion. For instance, the command <code>frama-c -slice-wr c t.c -then-on 'Slicing export' -print</code> produces the reduced program below, where the assignment to <code>d</code> has been removed:</p> <pre><code>/* Generated by Frama-C */ int a; int b; int *p; int f_slice_1(int x) { int __retres; __retres = a + x; return (__retres); } void main(int c) { p = &amp; b; a = 1; *p = 2; c = f_slice_1(b); return; } </code></pre>
    singulars
    1. This table or related slice is empty.
    1. POwhich free tools can I use to generate the program dependence graph for c codes
      singulars
      1. PTQuestion
    1. PTAnswer
    1. This table or related slice is empty.
    1. USPascal Cuoq
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POwhich free tools can I use to generate the program dependence graph for c codes
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COthank you very much for your remarkable help. I am beginning to learn how to use Frama-C . In the reference of Frama-C ,I can not find the meanning of the line in the graph.main.dot graph. What do the different line styles mean ? or is there any material about this.
      singulars
      1. PO
      1. USuser1283336
    2. CO@user1283336 There are 3 kinds of arrows: respectively data, control and address dependencies. The program `int a, b, *p; void main(int x, int y, int z) { p = &a; *p = x; if (y) b = z; } ` contains all 3 kinds of dependencies. Using the same commandlines as in the first example, you should have no difficulty recognizing which is which. There is no user-available description of the internals of the slicer, sorry, only an outside description of how to use it.
      singulars
      1. PO
      1. USPascal Cuoq
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload