Changeset 3215 for Deliverables

Timestamp:

Apr 29, 2013, 9:53:20 PM (7 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:

• Makefile.in (modified) (1 diff)
• README (modified) (1 diff)
• cerco-executable (added)
• cerco-executable/Makefile.in (added)
• cerco-executable/cerco.in (added)
• configure.ac (modified) (1 diff)
• distributed_files (modified) (1 diff)

Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/Makefile.in

@@ -1 +1 @@
 PACKAGE=cost-plug-in
-VERSION=0.1
+VERSION=0.2
 PACKAGE_RES=$(PACKAGE)-$(VERSION).tgz
 

Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/README

@@ -85 +85 @@
 
     % frama-c -jessie annotated-file.c
+
+  - cerco script
+
+    The best results are obtained when the why3 Frama-C plug-in is also
+    installed. We provide a script that combines calls to the Frama-C and the
+    why3 plug-ins, behaving like an improved Jessie script. The syntax of the
+    script is
+
+           cerco [-ide] [-untrusted] filename.c
+
+    The file filename.c is compiler using either the CerCo trusted compiler
+    acc-trusted or the CerCo untrusted compiler acc, according to the
+    -untrusted flag. The script produces both the object code filename.hex
+    and the annotated source code filename-acc-annotated.c. Then it invokes
+    the Frama-C plug-in and the Jessie/why3 plug-ins to automatically certify
+    the annotations. If the -ide flag is passed, the why3 IDE is opened to
+    manually run the provers on the proof obligations.

Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/configure.ac

@@ -13 +13 @@
 AC_OUTPUT(frama-c_jessie)
 AC_OUTPUT(wrapper/Makefile)
+AC_OUTPUT(cerco-executable/Makefile)
+AC_OUTPUT(cerco-executable/cerco)
 

Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/distributed_files

@@ -51 +51 @@
 wrapper/tests/parity/README
 wrapper/tests/parity/parity.lus
+cerco-executable/
+cerco-executable/Makefile
+cerco-executable/makefile.cerco
+cerco-executable/cerco