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