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 ## Attachments - [Blinky_ARM.zip](/uploads/d3777e008da2b3ee3882101d9950e0f8/Blinky_ARM.zip) - [preprocessed.i](/uploads/a17ecac1bec1d4a4b5d8ece091b8625a/preprocessed.i)