Changeset 1689


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

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

Location:
Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch
Files:
1 deleted
3 edited

Legend:

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

    r1462 r1689  
    44all:
    55        make -C plugin
    6         make -C wrapper
    76
    87install:
    98        make -C plugin install
    10         make -C wrapper install
    119
    1210clean:
    1311        rm -fr $(PACKAGE) $(PACKAGE_RES)
    1412        make -C plugin clean
    15         make -C wrapper clean
    1613
    1714distclean: clean
    1815        make -C plugin distclean
    19         make -C wrapper distclean
    2016
    2117dist:
  • 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
  • Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/plugin/compute.ml

    r1508 r1689  
    654654    let body_cost = Cost_value.reduce e e e body_cost in
    655655    let body_cost = Cost_value.amalgamation body_cost in
     656    Printf.printf "%s\n" (to_string body_cost);
    656657    mk_loop_cost_index index 0 v 1 body_cost
    657658
     
    10021003    mk_loop_invariant_counter_no_change counter rel init_value exit_value in
    10031004  let invariant_cost =
    1004     mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id
     1005     mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id
    10051006      counter cost in
    10061007  let variant =
Note: See TracChangeset for help on using the changeset viewer.