photo

Dimo


KOSTAL SofiaSoft Bulgaria OOD

Last seen: 9 months 前 |  自 2013 起处于活动状态

Followers: 0   Following: 0

消息

统计学

  • Thankful Level 2
  • Thankful Level 1
  • Revival Level 1
  • First Answer

查看徽章

Feeds

排序方式:

提问


Orange OBAI check in Polyspace Code Prover R2015a
The code snippet below is verified with CodeProver R2015a. The tool detects an orange OBAI at line 11033 (iter [-2^31...2^31+1])...

6 years 前 | 1 个回答 | 0

1

个回答

提问


Polyspace assumption regarding global/static variable
Hello, In R2015a in codeprov_ref.pdf (page 5-10) under *External Variables* topic is written: *Polyspace verification work...

6 years 前 | 1 个回答 | 0

1

个回答

已回答
Mismatch between polyspace error message and the code line
Hello Alexander, The behavior is really very strange. The code is ANSI C compliant so don't think the reason is in it. I have...

8 years 前 | 0

提问


Mismatch between polyspace error message and the code line
Hello, When I click on the error in Result Summary pane of Polyspace Code Prover (R2015a) the result is empty line in Source ...

8 years 前 | 2 个回答 | 0

2

个回答

提问


Polyspace Code Prover 2015a: Unexpexted error (parallel: task: MJSUnableToSubmitResult)
Hello, The compilation process is successful and verification starts. After some time I get this error message on the Polyspa...

8 years 前 | 0 个回答 | 0

0

个回答

已回答
Polyspace 2015a orange check IDP (Illegally dereferenced pointer)
Hi, I was wrong. The error really doesn't occur even array definitions were made locally. Dimo

8 years 前 | 0

已回答
Polyspace 2015a orange check IDP (Illegally dereferenced pointer)
Hi Alex, Thank you for your reply. Yes, the code is more complex than I have described. The interesting is that the code ...

8 years 前 | 0

已回答
Files are not generated with Polyspace Code Prover R2015a
Have you tried this: If this error occurs, try increasing the Java® heap size. The default heap size in a 64-bit architec...

8 years 前 | 0

提问


Polyspace 2015a orange check IDP (Illegally dereferenced pointer)
Hello, Can someone explain me the following Polyspace warning, especially the text in bold? Warning: pointer may be outsid...

8 years 前 | 4 个回答 | 0

4

个回答

提问


An unexpected error occurred during the Polyspace Jobs Manager execution
Hello, When I run Polyspace with *Batch* option selected, I get this: Error: An unexpected error occurred during the Polys...

8 years 前 | 0 个回答 | 0

0

个回答

提问


Unreachable functions don't appear in the report
Hello, I'm trying to simulate a source code containing functions that are not called in the code. In *Results Explorer* polys...

9 years 前 | 1 个回答 | 0

1

个回答

提问


Polyspace for C error messages: invalid storage class for a parameter/a declaration here must declare a parameter
I get a lot of error messages in header files: For example: invalid storage class for a parameter extern volatile u08 ...

11 years 前 | 1 个回答 | 0

1

个回答