Changeset 1689 for Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch
- Timestamp:
- Feb 13, 2012, 3:54:58 PM (9 years ago)
- 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 4 4 all: 5 5 make -C plugin 6 make -C wrapper7 6 8 7 install: 9 8 make -C plugin install 10 make -C wrapper install11 9 12 10 clean: 13 11 rm -fr $(PACKAGE) $(PACKAGE_RES) 14 12 make -C plugin clean 15 make -C wrapper clean16 13 17 14 distclean: clean 18 15 make -C plugin distclean 19 make -C wrapper distclean20 16 21 17 dist: -
Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/README
r1462 r1689 2 2 -------------- 3 3 4 This is a Frama-C plug-in and a wrapper for Lustre that makes the synthesis of5 the results of the CerCo compiler.4 This is a Frama-C plug-in that makes the synthesis of the results of the CerCo 5 compiler, using its indexed labels features. 6 6 7 7 Requirements … … 10 10 - Frama-C Carbon 11 11 - CerCo 12 - Lustre compiler (for Lustre files only)13 - Jessie plug-in and simplify (for verification of Lustre files only)14 12 15 13 Compilation 16 14 ------------- 17 15 18 You can compile the plug-in and the wrapperusing the following command:16 You can compile the plug-in using the following command: 19 17 20 18 % make … … 52 50 % frama-c -cost-help 53 51 54 - Lustre wrapper:55 56 You can run the wrapper for Lustre on a node "node" of a Lustre file57 "file.lus" using the following command:58 59 % frama-c_lustre file.lus node60 61 The result will be in file "file-annotated.c" in the same directory if the62 name is fresh. Otherwise an integer suffix will be added to the base name of63 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 654 654 let body_cost = Cost_value.reduce e e e body_cost in 655 655 let body_cost = Cost_value.amalgamation body_cost in 656 Printf.printf "%s\n" (to_string body_cost); 656 657 mk_loop_cost_index index 0 v 1 body_cost 657 658 … … 1002 1003 mk_loop_invariant_counter_no_change counter rel init_value exit_value in 1003 1004 let invariant_cost = 1004 mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id1005 mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id 1005 1006 counter cost in 1006 1007 let variant =
Note: See TracChangeset
for help on using the changeset viewer.