Frama-C Bug Tracking System - Frama-C
View Issue Details
0002260Frama-CPlug-in > wppublic2016-12-03 18:332016-12-03 18:33
giorgetti 
correnson 
normalminoralways
assignedopen 
Frama-C Aluminium 
 
0002260: error in Coq file generation
When an ACSL axiomatic in a C file main.c contains a type declaration, say type t; the command frama-c .. -wp main.c -wp-prover coqide .. generates a wrong line Parameter fct : Type. in the file typed_fct/A_coq_.v.
Noticed during a meeting with L. Correnson
No tags attached.
Issue History
2016-12-03 18:33giorgettiNew Issue
2016-12-03 18:33giorgettiStatusnew => assigned
2016-12-03 18:33giorgettiAssigned To => correnson

There are no notes attached to this issue.