View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000148 | Frama-C | Kernel | public | 2009-06-05 16:05 | 2014-02-12 16:56 | ||||
Reporter | puccetti | ||||||||
Assigned To | signoles | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Beryllium-20090601-beta1 | |||||||
Summary | 0000148: cmdline.ml assertion error at line 88 | ||||||||
Description | On Frama-C version Lithium-20081201+dev, running the following script leads to the error message below after approx 1 sec: ____________________________________________________________ script___ #! /bin/zsh PPCTOPDIR=$HOME/free/ppc_new3 XEN3TOPDIR=$HOME/free/xen-3.0.3 MYXENDIR=$XEN3TOPDIR/top PPCSTATEDIR=$MYXENDIR MYCPP="./myprepro.sh -DNDEBUG -D__x86_64__ -D__GNU__ -DBASILE_XEN_PPC_ANALYZED -D__XEN__ \ -DVERBOSE -I $MYXENDIR/include -DGUEST_PAGING_LEVELS=4 -DSHADOW_PAGING_LEVELS=4 -I $MYXENDIR/include \ -I $XEN3TOPDIR/xen/include \ -I $XEN3TOPDIR/xen/include/asm-x86/mach-generic -I $XEN3TOPDIR/xen/include/asm-x86/mach-default" srcfiles=( \ $XEN3TOPDIR/xen/acm/acm_chinesewall_hooks.c \ $XEN3TOPDIR/xen/acm/acm_null_hooks.c \ $XEN3TOPDIR/xen/acm/acm_policy.c \ $XEN3TOPDIR/xen/acm/acm_simple_type_enforcement_hooks.c \ $XEN3TOPDIR/xen/arch/x86/acpi/boot.c \ $XEN3TOPDIR/xen/arch/x86/apic.c \ $XEN3TOPDIR/xen/arch/x86/bitops.c \ $XEN3TOPDIR/xen/arch/x86/boot/mkelf32.c \ $XEN3TOPDIR/xen/arch/x86/compat.c \ $XEN3TOPDIR/xen/arch/x86/cpu/amd.c \ $XEN3TOPDIR/xen/arch/x86/cpu/centaur.c \ $XEN3TOPDIR/xen/arch/x86/cpu/common.c \ $XEN3TOPDIR/xen/arch/x86/cpu/cyrix.c \ $XEN3TOPDIR/xen/arch/x86/cpu/intel.c \ $XEN3TOPDIR/xen/arch/x86/cpu/intel_cacheinfo.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mcheck/k7.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mcheck/mce.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mcheck/non-fatal.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mcheck/p4.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mcheck/p5.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mcheck/p6.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mcheck/winchip.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mtrr/amd.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mtrr/centaur.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mtrr/cyrix.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mtrr/generic.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mtrr/main.c \ $XEN3TOPDIR/xen/arch/x86/cpu/mtrr/state.c \ $XEN3TOPDIR/xen/arch/x86/cpu/rise.c \ $XEN3TOPDIR/xen/arch/x86/cpu/transmeta.c \ $XEN3TOPDIR/xen/arch/x86/delay.c \ $XEN3TOPDIR/xen/arch/x86/dmi_scan.c \ $XEN3TOPDIR/xen/arch/x86/domain_build.c \ $XEN3TOPDIR/top/arch/x86/domain.c \ $XEN3TOPDIR/xen/arch/x86/domctl.c \ $XEN3TOPDIR/top/arch/x86/e820.c \ $XEN3TOPDIR/xen/arch/x86/extable.c \ $XEN3TOPDIR/top/arch/x86/flushtlb.c \ $XEN3TOPDIR/xen/arch/x86/genapic/bigsmp.c \ $XEN3TOPDIR/xen/arch/x86/genapic/default.c \ $XEN3TOPDIR/xen/arch/x86/genapic/delivery.c \ $XEN3TOPDIR/xen/arch/x86/genapic/es7000.c \ $XEN3TOPDIR/xen/arch/x86/genapic/es7000plat.c \ $XEN3TOPDIR/xen/arch/x86/genapic/probe.c \ $XEN3TOPDIR/xen/arch/x86/genapic/summit.c \ $XEN3TOPDIR/xen/arch/x86/xhvm/hvm.c \ $XEN3TOPDIR/xen/arch/x86/hvm/i8254.c \ $XEN3TOPDIR/xen/arch/x86/hvm/i8259.c \ $XEN3TOPDIR/xen/arch/x86/hvm/instrlen.c \ $XEN3TOPDIR/xen/arch/x86/hvm/intercept.c \ $XEN3TOPDIR/xen/arch/x86/hvm/io.c \ $XEN3TOPDIR/xen/arch/x86/hvm/platform.c \ $XEN3TOPDIR/xen/arch/x86/hvm/svm/emulate.c \ $XEN3TOPDIR/xen/arch/x86/hvm/svm/intr.c \ $XEN3TOPDIR/xen/arch/x86/hvm/svm/svm.c \ $XEN3TOPDIR/xen/arch/x86/hvm/svm/vmcb.c \ $XEN3TOPDIR/xen/arch/x86/hvm/vioapic.c \ $XEN3TOPDIR/xen/arch/x86/hvm/vlapic.c \ $XEN3TOPDIR/xen/arch/x86/hvm/vmx/io.c \ $XEN3TOPDIR/xen/arch/x86/hvm/vmx/vmcs.c \ $XEN3TOPDIR/xen/arch/x86/hvm/vmx/vmx.c \ $XEN3TOPDIR/xen/arch/x86/i387.c \ $XEN3TOPDIR/top/arch/x86/i8259.c \ $XEN3TOPDIR/xen/arch/x86/io_apic.c \ $XEN3TOPDIR/xen/arch/x86/irq.c \ $XEN3TOPDIR/xen/arch/x86/microcode.c \ $XEN3TOPDIR/xen/arch/x86/mm/shadow/common.c \ $XEN3TOPDIR/xen/arch/x86/mm/shadow/multi.c \ $XEN3TOPDIR/xen/arch/x86/mpparse.c \ $XEN3TOPDIR/xen/arch/x86/nmi.c \ $XEN3TOPDIR/xen/arch/x86/oprofile/nmi_int.c \ $XEN3TOPDIR/xen/arch/x86/oprofile/op_model_athlon.c \ $XEN3TOPDIR/xen/arch/x86/oprofile/op_model_p4.c \ $XEN3TOPDIR/xen/arch/x86/oprofile/op_model_ppro.c \ $XEN3TOPDIR/xen/arch/x86/oprofile/xenoprof.c \ $XEN3TOPDIR/xen/arch/x86/physdev.c \ $XEN3TOPDIR/xen/arch/x86/platform_hypercall.c \ $XEN3TOPDIR/xen/arch/x86/rwlock.c \ $XEN3TOPDIR/xen/arch/x86/shutdown.c \ $XEN3TOPDIR/xen/arch/x86/smpboot.c \ $XEN3TOPDIR/xen/arch/x86/smp.c \ $XEN3TOPDIR/xen/arch/x86/string.c \ $XEN3TOPDIR/xen/arch/x86/sysctl.c \ $XEN3TOPDIR/xen/arch/x86/time.c \ $XEN3TOPDIR/xen/arch/x86/traps.c \ $XEN3TOPDIR/xen/arch/x86/usercopy.c \ $XEN3TOPDIR/xen/arch/x86/x86_64/asm-offsets.c \ $XEN3TOPDIR/top/arch/x86/x86_64/mm.c \ $XEN3TOPDIR/top/arch/x86/x86_64/traps.c \ $XEN3TOPDIR/xen/arch/x86/x86_emulate.c \ $XEN3TOPDIR/xen/common/acm_ops.c \ $XEN3TOPDIR/xen/common/bitmap.c \ $XEN3TOPDIR/xen/common/domain.c \ $XEN3TOPDIR/xen/common/domctl.c \ $XEN3TOPDIR/xen/common/elf.c \ $XEN3TOPDIR/xen/common/event_channel.c \ $XEN3TOPDIR/xen/common/grant_table.c \ $XEN3TOPDIR/xen/common/kernel.c \ $XEN3TOPDIR/xen/common/keyhandler.c \ $XEN3TOPDIR/xen/common/lib.c \ $XEN3TOPDIR/xen/common/memory.c \ $XEN3TOPDIR/xen/common/multicall.c \ $XEN3TOPDIR/top/common/page_alloc.c \ $XEN3TOPDIR/xen/common/perfc.c \ $XEN3TOPDIR/xen/common/rangeset.c \ $XEN3TOPDIR/xen/common/sched_credit.c \ $XEN3TOPDIR/xen/common/sched_sedf.c \ $XEN3TOPDIR/xen/common/schedule.c \ $XEN3TOPDIR/xen/common/shutdown.c \ $XEN3TOPDIR/xen/common/softirq.c \ $XEN3TOPDIR/top/common/string.c \ $XEN3TOPDIR/xen/common/symbols.c \ $XEN3TOPDIR/xen/common/symbols-dummy.c \ $XEN3TOPDIR/xen/common/sysctl.c \ $XEN3TOPDIR/xen/common/timer.c \ $XEN3TOPDIR/xen/common/trace.c \ $XEN3TOPDIR/xen/common/version.c \ $XEN3TOPDIR/top/common/vsprintf.c \ $XEN3TOPDIR/xen/common/xmalloc.c \ $XEN3TOPDIR/xen/drivers/acpi/tables.c \ $XEN3TOPDIR/top/drivers/char/console.c \ $XEN3TOPDIR/xen/drivers/char/ns16550.c \ $XEN3TOPDIR/xen/drivers/char/serial.c \ $XEN3TOPDIR/xen/drivers/video/font_8x14.c \ $XEN3TOPDIR/xen/drivers/video/font_8x16.c \ $XEN3TOPDIR/xen/drivers/video/font_8x8.c \ $XEN3TOPDIR/top/drivers/video/vga.c \ $XEN3TOPDIR/xen/tools/figlet/figlet.c \ $XEN3TOPDIR/xen/tools/symbols.c ) $PPCTOPDIR/bin/toplevel.opt \ -absolute-valid-range 0x2000-0xFFFFFFFFFFFF0 \ -save $PPCSTATEDIR/opentc.state -val -main cea_main \ -cpp-command "$MYCPP" \ $srcfiles \ cea_main.c cea_4asm.c cea_x86_mm.c cea_x86_setup.c _________________________________________________________________err___ Fatal error: exception Assert_failure("src/kernel/cmdline.ml", 88, 29) Called from file "src/kernel/cmdline.ml", line 96, characters 32-61 Called from file "src/kernel/cmdline.ml", line 141, characters 3-46 Called from file "src/kernel/cmdline.ml", line 147, characters 35-55 Called from file "src/kernel/cmdline.ml", line 156, characters 4-554 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
signoles (manager) 2009-06-05 20:23 |
Note that there is a little syntax change in the command line. You have to write the following command line (add '=' between -cpp-command and "$MYCPP") : ===== $PPCTOPDIR/bin/toplevel.opt \ -absolute-valid-range 0x2000-0xFFFFFFFFFFFF0 \ -save $PPCSTATEDIR/opentc.state -val -main cea_main \ -cpp-command="$MYCPP" \ $srcfiles \ cea_main.c cea_4asm.c cea_x86_mm.c cea_x86_setup.c ===== |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2009-06-05 16:05 | puccetti | New Issue | |
2009-06-05 16:05 | puccetti | File Added: myprepro.sh | |
2009-06-05 16:33 | signoles | Assigned To | => signoles |
2009-06-05 16:33 | signoles | Status | new => acknowledged |
2009-06-05 19:05 | svn | ||
2009-06-05 19:05 | svn | Status | acknowledged => resolved |
2009-06-05 19:05 | svn | Resolution | open => fixed |
2009-06-05 20:23 | signoles | Note Added: 0000160 | |
2009-06-23 18:02 | signoles | Status | resolved => closed |
2009-06-23 18:03 | signoles | Fixed in Version | => Frama-C Beryllium beta-1 |
2013-12-19 01:13 | signoles | Source_changeset_attached | => framac master ec8a4878 |
2014-02-12 16:56 | signoles | Source_changeset_attached | => framac stable/neon ec8a4878 |