0002352: Frama-Clang crashes on error in contract

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002352

Frama-C

Plug-in > clang

public

2018-01-31 18:17

Reporter

jens

Assigned To

virgile

Priority

normal

Severity

crash

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Frama-C 16-Sulfur

Target Version

Fixed in Version

Summary

0002352: Frama-Clang crashes on error in contract

Description

The attached example uses mistakenly the assignment operator = instead of == in the ensures clause.
Frama-Clang crashes on this example.

frama-c -wp -wp-rte assignment_in_contract.cpp
[kernel] Parsing assignment_in_contract.cpp (external front-end)
framaCIRGen: ACSLTermOrPredicate.cpp:7096: Parser::Base::ReadResult Acsl::TermOrPredicate::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "assignment_in_contract.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.

A message along the lines of normal Frama-C
"user error: Assignment operators not allowed in annotations."
would be more helpful.

Tags

No tags attached.

Attached Files

assignment_in_contract.cpp [^] (73 bytes) 2018-01-31 18:17

Relationships

Notes
There are no notes attached to this issue.

Issue History
Date Modified	Username	Field	Change
2018-01-31 18:17	jens	New Issue
2018-01-31 18:17	jens	Status	new => assigned
2018-01-31 18:17	jens	Assigned To	=> virgile
2018-01-31 18:17	jens	File Added: assignment_in_contract.cpp