Frama-C Bug Tracking System - Frama-C
View Issue Details
0001634Frama-CPlug-in > E-ACSLpublic2014-01-27 15:212014-03-25 14:17
ThomasJ 
signoles 
normalcrashalways
closedfixed 
x86_64Ubuntu12.04 LTS
Frama-C Fluorine-20130601 
Frama-C Neon-20140301 
0001634: e-acsl translation: unexpected error
I'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.
frama-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
[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).
No tags attached.
zip Blinky_ARM.zip (517,998) 2014-01-27 15:21
https://bts.frama-c.com/file_download.php?file_id=653&type=bug
? preprocessed.i (117,444) 2014-01-28 11:04
https://bts.frama-c.com/file_download.php?file_id=655&type=bug
Issue History
2014-01-27 15:21ThomasJNew Issue
2014-01-27 15:21ThomasJStatusnew => assigned
2014-01-27 15:21ThomasJAssigned To => signoles
2014-01-27 15:21ThomasJFile Added: Blinky_ARM.zip
2014-01-28 10:33ThomasJNote Added: 0004449
2014-01-28 10:33ThomasJNote Edited: 0004449View Revisions
2014-01-28 10:44signolesNote Added: 0004450
2014-01-28 10:44signolesStatusassigned => feedback
2014-01-28 11:04ThomasJFile Added: preprocessed.i
2014-01-28 11:06ThomasJNote Added: 0004451
2014-01-28 11:06ThomasJStatusfeedback => assigned
2014-01-28 11:24signolesNote Added: 0004452
2014-01-28 11:24signolesStatusassigned => resolved
2014-01-28 11:24signolesResolutionopen => fixed
2014-01-28 11:26signolesNote Edited: 0004452View Revisions
2014-03-13 15:58signolesNote Added: 0004953
2014-03-13 15:58signolesStatusresolved => closed
2014-03-13 15:58signolesFixed in Version => Frama-C Neon-20140301

Notes
(0004449)
ThomasJ   
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   
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   
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   
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   
2014-03-13 15:58   
Fixed in E-ACSL 0.4