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 - 2019 MantisBT Team
Powered by Mantis Bugtracker