PolySpace的使用问题
最近装了PolySpace，按照说明文档上说的使用光盘中自带的Demo_c里边的sample.c练习，先使用client方式，执行开始，编译都是通过的，可是intermediate时出问题了，总是提示“This program cannot be run in standalne mode.”实在不解，有没有哪位大虾遇到过类似问题的，帮着解答解答。下面是log
<polyspace-c R2007aplus PID4916 PGID5520>
<polyspace-viewer V4.2.1.10>
Type /cygdrive/e/Result/Single_file/kill-rte-kernel on host LJW to halt Verifier process
Options used with Verifier:
-polyspace-version=R2007aplus
-from=scratch
-date=10/04/2013
-main-generator-calls=unused
-lang=C
-results-dir=e:\Result\Single_file
-author=ymt
-main-generator-writes-variables=public
-target=sparc
-voa=true
-continue-with-red-error=true
-verif-version=1.0
-O=-O2
-prog=New_Project
-to=Software Safety Analysis level 4
-I1=e:\PL\sources
-desktop=true
-dos=true
-OS-target=Solaris
-continue-with-existing-host=true
Verifying host configuration ...
Memory > 380MB : OK (1.99 GB)
Swap > 1GB : OK (3.99 GB)
Min(4GB,Swap) >= Min(4GB,Memory) : OK
Tmp space available in C:\PolySpace\PolySpace_Common\PST_Cygwin\tmp >= 10MB : OK (16.69 GB)
*** Configuration of the host : OK
Checking license ...
License is OK
PolySpace Technologies C static program verifier
Copyright (c) 1999-2013 PolySpace Technologies
All rights reserved.
Starting at: Apr 10, 2013 22:12:23
Host: CYGWIN_NT-5.1 LJW 1.3.17(0.67/3/2) i686
User: ymt
**********************************************************
***
*** Verifying C sources
***
**********************************************************
Copying sources to C-ALL ...
Number of files : 1
Number of lines : 248
Number of lines without comments : 136
OS-target solaris implies: -D__STDC__ -D__GNUC__=2 -D__GNUC_MINOR__=8 -D__GCC_NEW_VARARGS__ -Dunix
-D__unix -D__unix__ -Dsparc -D__sparc -D__sparc__ -Dsun
-D__sun -D__sun__ -D__svr4__ -D__SVR4
Verifying sources ...
Verifying example.c
Verifying cross-files ANSI C compliance
Stubbing standard library functions ...
Stubbing unknown functions ...
* Function get_bus_status is pure. Returns an initialized value.
* Function random_int is pure. Returns an initialized value.
* Function random_float is pure. Returns an initialized value.
Generating the Main ...
Generating call to function: RTE
Doing code transformations ...
**********************************************************
***
*** C sources verification done
***
**********************************************************
Ending at: Apr 10, 2013 22:12:57
User time for suif: 34.3real, 4u + 4.5s (0.2gc)
Starting at: Apr 10, 2013 22:12:58
**********************************************************
***
*** Beginning C to intermediate language translation
***
**********************************************************
This program cannot be run in standalone mode
-------------------------------------------------------------------
--- ---
---Verifier has encountered an internal error. ---
---Please contact your technical support. ---
--- ---
-------------------------------------------------------------------
Failure at: Apr 10, 2013 22:12:59
User time for polyspace-c: 37real, 4.3u + 5.1s (0.2gc)
Exiting because of previous error
***
*** End of PolySpace Verifier analysis
*** lz的的操作系统是否在server 2003系统上，这是polyspace 2007a自身的问题。
页:
[1]
