0000148: cmdline.ml assertion error at line 88

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

Issue History
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	Checkin
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

Notes
(0000160) 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 =====

Relationships