Changeset 1689 for Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch

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)

Location:

Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch

Files:

• Makefile (modified) (1 diff)
• README (modified) (3 diffs)
• plugin/compute.ml (modified) (2 diffs)
• wrapper (deleted)

Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/Makefile

@@ -4 +4 @@
 all:
         make -C plugin
-        make -C wrapper
 
 install:
         make -C plugin install
-        make -C wrapper install
 
 clean:
         rm -fr $(PACKAGE) $(PACKAGE_RES)
         make -C plugin clean
-        make -C wrapper clean
 
 distclean: clean
         make -C plugin distclean
-        make -C wrapper distclean
 
 dist:

Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/README

@@ -2 +2 @@
 --------------
 
-This is a Frama-C plug-in and a wrapper for Lustre that makes the synthesis of
-the results of the CerCo compiler.
+This is a Frama-C plug-in that makes the synthesis of the results of the CerCo
+compiler, using its indexed labels features.
 
  Requirements
@@ -10 +10 @@
   - Frama-C Carbon
   - CerCo
-  - Lustre compiler (for Lustre files only)
-  - Jessie plug-in and simplify (for verification of Lustre files only)
 
  Compilation
 -------------
 
-  You can compile the plug-in and the wrapper using the following command:
+  You can compile the plug-in using the following command:
 
   % make
@@ -52 +50 @@
     % frama-c -cost-help
 
-  - Lustre wrapper:
-
-    You can run the wrapper for Lustre on a node "node" of a Lustre file
-    "file.lus" using the following command:
-
-    % frama-c_lustre file.lus node
-
-    The result will be in file "file-annotated.c" in the same directory if the
-    name is fresh. Otherwise an integer suffix will be added to the base name of
-    the output file.
-
-    For a complete description of the options, use the command:
-
-    % frama-c_lustre -help

Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/plugin/compute.ml

@@ -654 +654 @@
     let body_cost = Cost_value.reduce e e e body_cost in
     let body_cost = Cost_value.amalgamation body_cost in
+    Printf.printf "%s\n" (to_string body_cost);
     mk_loop_cost_index index 0 v 1 body_cost
 
@@ -1002 +1003 @@
     mk_loop_invariant_counter_no_change counter rel init_value exit_value in
   let invariant_cost =
-    mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id
+     mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id
       counter cost in
   let variant =