Ignore:
Timestamp:
Feb 13, 2012, 3:54:58 PM (8 years ago)
Author:
tranquil
Message:

kept out the wrapper (which I did not touch, so not sure it works)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/README

    r1462 r1689  
    22--------------
    33
    4 This is a Frama-C plug-in and a wrapper for Lustre that makes the synthesis of
    5 the results of the CerCo compiler.
     4This is a Frama-C plug-in that makes the synthesis of the results of the CerCo
     5compiler, using its indexed labels features.
    66
    77 Requirements
     
    1010  - Frama-C Carbon
    1111  - CerCo
    12   - Lustre compiler (for Lustre files only)
    13   - Jessie plug-in and simplify (for verification of Lustre files only)
    1412
    1513 Compilation
    1614-------------
    1715
    18   You can compile the plug-in and the wrapper using the following command:
     16  You can compile the plug-in using the following command:
    1917
    2018  % make
     
    5250    % frama-c -cost-help
    5351
    54   - Lustre wrapper:
    55 
    56     You can run the wrapper for Lustre on a node "node" of a Lustre file
    57     "file.lus" using the following command:
    58 
    59     % frama-c_lustre file.lus node
    60 
    61     The result will be in file "file-annotated.c" in the same directory if the
    62     name is fresh. Otherwise an integer suffix will be added to the base name of
    63     the output file.
    64 
    65     For a complete description of the options, use the command:
    66 
    67     % frama-c_lustre -help
Note: See TracChangeset for help on using the changeset viewer.