Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002260Frama-CPlug-in > wppublic2016-12-03 18:332016-12-03 18:33
Reportergiorgetti 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in Version 
Summary0002260: error in Coq file generation
DescriptionWhen 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.
Additional InformationNoticed during a meeting with L. Correnson
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-12-03 18:33 giorgetti New Issue
2016-12-03 18:33 giorgetti Status new => assigned
2016-12-03 18:33 giorgetti Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker