e-acsl translation: unexpected error
ID0001634: This issue was created automatically from Mantis Issue 1634. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001634 | Frama-C | Plug-in > E-ACSL | public | 2014-01-27 | 2014-03-25 |
| Reporter | ThomasJ | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | x86_64 | OS | Ubuntu | OS Version | 12.04 LTS |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
Description :
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.
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).Steps To Reproduce :
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