0002348: unknown variable in contract is not treated as an error

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002348

Frama-C

Plug-in > clang

public

2018-01-30 16:31

2018-01-30 18:03

Reporter

jens

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Target Version

Fixed in Version

Summary

0002348: unknown variable in contract is not treated as an error

Description

The attached C/C++ code is treated differently by Frama-C and Frama-Clang
The C file 'unknown_variable.c' is correctly rejected by Frama-C with wit the the message

    frama-c -wp -wp-rte unknown_variable.c

   [kernel] user error: stopping on file "unknown_variable.c" that has errors. Add
    '-kernel-msg-key pp' for preprocessing command.

When processing this file as C++ code

   frama-c -wp -wp-rte unknown_variable.cpp

Frama-Clang only emits a warning (by the kernel) and continues processing

   Parsing unknown_variable.cpp (external front-end)
unknown_variable.cpp:6:18: unknown identifier 'c'
Now output intermediate result

In my opinion, the C++ contract should be rejected as well.

Tags

No tags attached.

Attached Files

unknown_variable.c [^] (88 bytes) 2018-01-30 16:31 [Show Content] [Hide Content]

extern int a;

/*@
   assigns a;
   ensures a == c;
*/
void foo(int b)
{
    a = b;
}

unknown_variable.cpp [^] (88 bytes) 2018-01-30 16:31

Relationships

Notes
(0006512) virgile (developer) 2018-01-30 18:03	If I'm not mistaken, Frama-Clang implements the old "continue-annot-error" behavior, but nevertheless the warning should have come from the plug-in, not the kernel.

Issue History
Date Modified	Username	Field	Change
2018-01-30 16:31	jens	New Issue
2018-01-30 16:31	jens	Status	new => assigned
2018-01-30 16:31	jens	Assigned To	=> virgile
2018-01-30 16:31	jens	File Added: unknown_variable.c
2018-01-30 16:31	jens	File Added: unknown_variable.cpp
2018-01-30 18:03	virgile	Note Added: 0006512