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
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
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
(0006328)
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 github.com/acsl-language/acsl?

- 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 - 2019 MantisBT Team
Powered by Mantis Bugtracker