Provide an option to run Coq from Frama-C

ID0001686: This issue was created automatically from Mantis Issue 1686. Further discussion may take place here.

Id	Project	Category	View	Due Date	Updated
ID0001686	Frama-C	Plug-in > wp	public	2014-03-12	2017-03-14


Reporter	jens	Assigned To	correnson	Resolution	no change required
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

When proving external Coq-lemma for WP it might be interesting to run Coq from Frama-C, e.g.,

  frama-c -wp-coq Foo.v

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information