Changeset 3215


Ignore:
Timestamp:
Apr 29, 2013, 9:53:20 PM (4 years ago)
Author:
sacerdot
Message:
  • Version dumped to 0.2
  • New executable cerco to be used with why3
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  
    11PACKAGE=cost-plug-in
    2 VERSION=0.1
     2VERSION=0.2
    33PACKAGE_RES=$(PACKAGE)-$(VERSION).tgz
    44
  • Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/README

    r2749 r3215  
    8585
    8686    % 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  
    1313AC_OUTPUT(frama-c_jessie)
    1414AC_OUTPUT(wrapper/Makefile)
     15AC_OUTPUT(cerco-executable/Makefile)
     16AC_OUTPUT(cerco-executable/cerco)
    1517
  • Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/distributed_files

    r2749 r3215  
    5151wrapper/tests/parity/README
    5252wrapper/tests/parity/parity.lus
     53cerco-executable/
     54cerco-executable/Makefile
     55cerco-executable/makefile.cerco
     56cerco-executable/cerco
Note: See TracChangeset for help on using the changeset viewer.