Project

General

Profile

Actions
Copy link

Bug #9523

closed

ACSL-By-Example: this kind of memory access is not currently supported: *\result

Added by Denis Efremov about 5 years ago. Updated about 5 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Mikhail Mandrykin
Start date:
03/11/2019
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

Работает в WP, мы падаем с ошибкой.

[kernel] Parsing equal_range2.normal.c (with preprocessing)
[Jessie2] Starting Jessie translation
[Jessie2] Warning: \separated is not supported by Jessie. This predicate will be ignored
[Jessie2] Warning: \valid_read is not supported by Jessie. It will be treated as \valid
[Jessie2] equal_range2.normal.c:72:25: Failure: 
  this kind of memory access is not currently supported: *\result
[Jessie2] equal_range2.normal.c:72:25: User Error: 
  Unsupported feature(s).
  Jessie plugin can not be used on your code.
[Jessie2] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in Jessie2 aborted: invalid user input.

Files

equal_range2.normal.c (5.56 KB) equal_range2.normal.c Denis Efremov, 03/11/2019 12:29 PM
Actions
Copy link
 #1

Updated by Denis Efremov about 5 years ago

  • Status changed from New to Closed
Actions
Copy link

Also available in: Atom PDF