Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001634Frama-CPlug-in > E-ACSLpublic2014-01-27 15:212014-03-25 14:17
ReporterThomasJ 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Platformx86_64OSUbuntuOS Version12.04 LTS
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001634: e-acsl translation: unexpected error
DescriptionI'm trying to create a E-ACSL code for ARM Processors. Therefore i use the arm-gcc instead of the usual gcc. Preprocessing works fine but the e-acsl translation fails.


journal.ml included in project.
Steps To Reproduceframa-c -journal-enable -journal-name blink4500 -e-acsl -cpp-command 'arm-linux-gnueabi-gcc-4.6 -C -E -DUC_ID=4503 -mfloat-abi=softfp -Wall -std=gnu99 -fmessage-length=0 -mcpu=cortex-m4 -mfpu=fpv4-sp-d16 -mthumb -g3 -gdwarf-2 -I. -IXMC4500 -I/usr/arm-linux-gnueabi/include/' Blinky.c LED.c System_XMC4500.c -then-on e-acsl -print -ocode monitored_arm.c
Additional Information[e-acsl] beginning translation.
[kernel] Current source was: System_XMC4500.c:347
         The full backtrace is:
         Called from file "error.ml", line 53, characters 4-7
         Called from file "visit.ml", line 574, characters 6-55
         Called from file "visit.ml", line 588, characters 3-41
         Called from file "cil/src/cil.ml", line 2832, characters 5-52
         Called from file "cil/src/cil.ml", line 2958, characters 14-21
         Called from file "cil/src/cil.ml", line 1847, characters 21-41
         Called from file "cil/src/cil.ml", line 2876, characters 5-86
         Called from file "cil/src/cil.ml", line 1871, characters 13-16
         Called from file "cil/src/cil.ml", line 3009, characters 16-40
         Called from file "cil/src/cil.ml", line 1847, characters 21-41
         Called from file "cil/src/cil.ml", line 3223, characters 14-39
         Called from file "cil/src/cil.ml", line 1847, characters 21-41
         Called from file "cil/src/cil.ml", line 3195, characters 5-91
         Called from file "cil/src/cil.ml", line 3275, characters 16-38
         Called from file "cil/src/cil.ml", line 1871, characters 13-16
         Called from file "cil/src/cil.ml", line 1916, characters 24-57
         Called from file "cil/src/cil.ml", line 3269, characters 5-53
         Called from file "cil/src/cil.ml", line 5895, characters 17-37
         Called from file "cil/src/cil.ml", line 5902, characters 3-20
         Called from file "cil/src/cil.ml", line 1847, characters 21-41
         Called from file "src/kernel/file.ml", line 1948, characters 14-42
         Called from file "src/kernel/file.ml", line 1977, characters 2-48
         Called from file "main.ml", line 152, characters 12-55
         Called from file "src/project/project.ml", line 345, characters 12-15
         Called from file "src/project/project.ml", line 350, characters 17-22
         Re-raised at file "src/project/project.ml", line 350, characters 56-57
         Called from file "main.ml", line 146, characters 5-572
         Called from file "src/project/project.ml", line 345, characters 12-15
         Called from file "src/project/project.ml", line 350, characters 17-22
         Re-raised at file "src/project/project.ml", line 350, characters 56-57
         Called from file "main.ml", line 116, characters 12-34
         Called from file "src/project/state_builder.ml", line 556, characters 17-22
         Called from file "src/kernel/journal.ml", line 434, characters 21-32
         Re-raised at file "src/kernel/journal.ml", line 449, characters 18-19
         Called from file "main.ml", line 199, characters 11-56
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 37, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
         
         Unexpected error (File "pre_analysis.ml", line 694, characters 18-24: Assertion failed).
TagsNo tags attached.
Attached Fileszip file icon Blinky_ARM.zip [^] (517,998 bytes) 2014-01-27 15:21
? file icon preprocessed.i [^] (117,444 bytes) 2014-01-28 11:04 [Show Content]

- Relationships

-  Notes
(0004449)
ThomasJ (reporter)
2014-01-28 10:33
edited on: 2014-01-28 10:33

Using gcc for preprocessing didn't fix the problem:

frama-c -e-acsl -cpp-command 'gcc -C -E -DUC_ID=4503 -Wall -std=gnu99 -fmessage-length=0 -g3 -gdwarf-2 -I. -IXMC4500' Blinky.c LED.c System_XMC4500.c -then-on e-acsl -print -ocode monitored_arm.c

(0004450)
signoles (manager)
2014-01-28 10:44

I guess the bug is not preprocessor-dependent. Unfortunately I cannot reproduce your issue because some system files are missing.

Could you please provide me a single already-preprocessed .i file? One way to generate such a file is to run:

$ frama-c -cpp-command="your_preprocessor_flags" your_c_files -print -ocode preprocessed.i
(0004451)
ThomasJ (reporter)
2014-01-28 11:06

Thanks for the quick response, preprocessed file uploaded. It's quite big for a simple "blink LED" program because of the ARM system functions...
(0004452)
signoles (manager)
2014-01-28 11:24
edited on: 2014-01-28 11:26

Fixed in the dev version. Here is a small patch you can apply against pre_analysis.ml of E-ACSL v0.3:

693c693,694
< | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
---
> | Const _ -> (* possible in case of static address *) false
> | UnOp _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _

(0004953)
signoles (manager)
2014-03-13 15:58

Fixed in E-ACSL 0.4

- Issue History
Date Modified Username Field Change
2014-01-27 15:21 ThomasJ New Issue
2014-01-27 15:21 ThomasJ Status new => assigned
2014-01-27 15:21 ThomasJ Assigned To => signoles
2014-01-27 15:21 ThomasJ File Added: Blinky_ARM.zip
2014-01-28 10:33 ThomasJ Note Added: 0004449
2014-01-28 10:33 ThomasJ Note Edited: 0004449 View Revisions
2014-01-28 10:44 signoles Note Added: 0004450
2014-01-28 10:44 signoles Status assigned => feedback
2014-01-28 11:04 ThomasJ File Added: preprocessed.i
2014-01-28 11:06 ThomasJ Note Added: 0004451
2014-01-28 11:06 ThomasJ Status feedback => assigned
2014-01-28 11:24 signoles Note Added: 0004452
2014-01-28 11:24 signoles Status assigned => resolved
2014-01-28 11:24 signoles Resolution open => fixed
2014-01-28 11:26 signoles Note Edited: 0004452 View Revisions
2014-03-13 15:58 signoles Note Added: 0004953
2014-03-13 15:58 signoles Status resolved => closed
2014-03-13 15:58 signoles Fixed in Version => Frama-C Neon-20140301


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker