Project

General

Profile

Actions

Bug #9522

closed

ACSL-By-Example: This application creates an illegal alias

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

Status:
Closed
Priority:
High
Start date:
03/11/2019
Due date:
% Done:

0%

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

Description

WP работает, мы - падаем. Возможно, потому что \separated игнорится. Прикладываю все примеры с такой ошибкой. Думаю, что причина одна и та же. Но лучше протестировать на всем после решения тикета.

why3 ide  --extra-config /home/work/.opam/astraver/lib/jessie/why3/why3.conf partial_sort_normal_c.mlw
[Config] reading extra configuration file /home/work/.opam/astraver/lib/jessie/why3/why3.conf
Error while reading file '../partial_sort_normal_c.mlw':
File "partial_sort_normal_c/../partial_sort_normal_c.mlw", line 4546, characters 16-39:
This application creates an illegal alias
make: *** [partial_sort_normal_c.makefile:15: why3ide] Error 1

Files

partial_sort.normal.c (13.5 KB) partial_sort.normal.c Denis Efremov, 03/11/2019 12:16 PM
selection_sort.normal.c (8.35 KB) selection_sort.normal.c Denis Efremov, 03/11/2019 12:17 PM
reverse.normal.c (2.55 KB) reverse.normal.c Denis Efremov, 03/11/2019 12:19 PM
random_shuffle.normal.c (5.7 KB) random_shuffle.normal.c Denis Efremov, 03/11/2019 12:25 PM
Actions #1

Updated by Denis Efremov almost 5 years ago

  • Status changed from New to Closed
Actions

Also available in: Atom PDF