Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000148Frama-CKernelpublic2009-06-05 16:052014-02-12 16:56
Reporterpuccetti 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000148: cmdline.ml assertion error at line 88
DescriptionOn 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
TagsNo tags attached.
Attached Files? file icon myprepro.sh [^] (514 bytes) 2009-06-05 16:05

- Relationships

-  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
=====

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker