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
Assigned Tocorrenson 
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker