Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002264Frama-CKernel > ACSL implementationpublic2016-12-20 10:492017-01-04 08:44
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002264: structure in logic not supported?
DescriptionWhen running 'frama-c type.c" on the attached file, I receive the following error message: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing type.c (with preprocessing) type.c:2:[kernel] user error: unexpected token '{' [kernel] user error: stopping on file "type.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input. I took the example straight from acsl-implementation manual (first line on page 27).
TagsNo tags attached.
Attached Filesc file icon type.c [^] (47 bytes) 2016-12-20 10:49 [Show Content]

- Relationships

-  Notes
virgile (developer)
2017-01-04 08:44

I'd tend to think that there is a mismatch between section 2.2.7 and 2.6.8 that introduces logic record types, which are basically equivalent to struct, except that they are defined as OCaml records (i.e. type t = { real x; real y }, without a struct keyword). Note that record types are not more implemented than logic struct types, as shown by figure 2.17. Nevertheless, I feel that we should not keep both constructions. However, this is more an ACSL issue than a Frama-C one. Could you open an issue on

- Issue History
Date Modified Username Field Change
2016-12-20 10:49 jens New Issue
2016-12-20 10:49 jens Status new => assigned
2016-12-20 10:49 jens Assigned To => virgile
2016-12-20 10:49 jens File Added: type.c
2017-01-04 08:44 virgile Note Added: 0006328

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker