cmdline.ml assertion error at line 88

ID0000148: This issue was created automatically from Mantis Issue 148. Further discussion may take place here.

Id	Project	Category	View	Due Date	Updated
ID0000148	Frama-C	Kernel	public	2009-06-05	2014-02-12


Reporter	puccetti	Assigned To	signoles	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	Frama-C Beryllium-20090601-beta1

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

Attachments

myprepro.sh

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information