structure in logic not supported?
ID0002264: This issue was created automatically from Mantis Issue 2264. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0002264 | Frama-C | Kernel > ACSL implementation | public | 2016-12-20 | 2017-01-04 |
Reporter | jens | Assigned To | virgile | Resolution | open |
Priority | normal | Severity | major | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
When 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).