Changeset 3215 for Deliverables
- Timestamp:
- Apr 29, 2013, 9:53:20 PM (7 years ago)
- Location:
- Deliverables/D5.1/frama-c-cost-plugin/Nitrogen
- Files:
-
- 3 added
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/Makefile.in
r2749 r3215 1 1 PACKAGE=cost-plug-in 2 VERSION=0. 12 VERSION=0.2 3 3 PACKAGE_RES=$(PACKAGE)-$(VERSION).tgz 4 4 -
Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/README
r2749 r3215 85 85 86 86 % frama-c -jessie annotated-file.c 87 88 - cerco script 89 90 The best results are obtained when the why3 Frama-C plug-in is also 91 installed. We provide a script that combines calls to the Frama-C and the 92 why3 plug-ins, behaving like an improved Jessie script. The syntax of the 93 script is 94 95 cerco [-ide] [-untrusted] filename.c 96 97 The file filename.c is compiler using either the CerCo trusted compiler 98 acc-trusted or the CerCo untrusted compiler acc, according to the 99 -untrusted flag. The script produces both the object code filename.hex 100 and the annotated source code filename-acc-annotated.c. Then it invokes 101 the Frama-C plug-in and the Jessie/why3 plug-ins to automatically certify 102 the annotations. If the -ide flag is passed, the why3 IDE is opened to 103 manually run the provers on the proof obligations. -
Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/configure.ac
r2749 r3215 13 13 AC_OUTPUT(frama-c_jessie) 14 14 AC_OUTPUT(wrapper/Makefile) 15 AC_OUTPUT(cerco-executable/Makefile) 16 AC_OUTPUT(cerco-executable/cerco) 15 17 -
Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/distributed_files
r2749 r3215 51 51 wrapper/tests/parity/README 52 52 wrapper/tests/parity/parity.lus 53 cerco-executable/ 54 cerco-executable/Makefile 55 cerco-executable/makefile.cerco 56 cerco-executable/cerco
Note: See TracChangeset
for help on using the changeset viewer.