0002357: can't handle lemma with 3 labels - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0002357

Frama-C

Plug-in > clang

public

2018-02-08 16:39

2018-02-08 17:24

Reporter

Jochen

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Platform

Sulfur-20171101

OS

OS Version

Ubuntu 17.10

Product Version

Frama-C 16-Sulfur

Target Version

Fixed in Version

Summary

0002357: can't handle lemma with 3 labels

Description

Running "frama-c -wp adjacent_difference_inv_cpp.cpp" on the attached program reports an error in line 6: "logic label `L' not found". The error message disappears when
(1) the file is renamed to "adjacent_difference_inv_cpp.c", and processed by plain Frama-C,
(2) the middle conjunct "foo{L}(1)" is removed in line 6, or
(3) label "M" is omitted in the header of "lem", and the rightmost conjunct is changed to "foo{L}(2)".
Consistently renaming the labels doesn't make the error message vanish.

Tags

No tags attached.

adjacent_difference_inv_cpp.cpp [^] (120 bytes) 2018-02-08 16:39

Relationships

Notes
(0006524) Jochen (reporter) 2018-02-08 16:47 edited on: 2018-02-08 16:52	The the surrounding 'extern "C" { ... }' can be removed without affecting the above description. (However, I apparently don't have permission to do that.)

(0006527) virgile (developer) 2018-02-08 17:24	Issue lies directly in the C++ part of the plugin (ACSL++ parser): produced AST already lacks the L label.

Issue History
Date Modified	Username	Field	Change
2018-02-08 16:39	Jochen	New Issue
2018-02-08 16:39	Jochen	Status	new => assigned
2018-02-08 16:39	Jochen	Assigned To	=> virgile
2018-02-08 16:39	Jochen	File Added: adjacent_difference_inv_cpp.cpp
2018-02-08 16:47	Jochen	Note Added: 0006524
2018-02-08 16:51	Jochen	Note Added: 0006525
2018-02-08 16:51	Jochen	Note Deleted: 0006525
2018-02-08 16:52	Jochen	Note Edited: 0006524	View Revisions
2018-02-08 17:24	virgile	Note Added: 0006527

Copyright © 2000 - 2018 MantisBT Team