0001789: Crashes when using logic in assigns statement

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001789

Frama-C

Kernel > ACSL implementation

public

2014-05-28 22:13

2015-03-17 22:17

Reporter

Ian

Assigned To

correnson

Priority

normal

Severity

crash

Reproducibility

always

Status

closed

Resolution

fixed

Platform

Ubuntu

OS Version

Product Version

Frama-C Neon-20140301

Target Version

Fixed in Version

Frama-C Sodium

Summary

0001789: Crashes when using logic in assigns statement

Description

WP crashes when using a statement defined with 'logic'

Steps To Reproduce

Create the file logic_assigns.c :
#include <stddef.h>

int *var_ptr;

/*@
    logic int *the_var = var_ptr;
*/

/*@
    //assigns var_ptr; // Works
    assigns the_var; // WP Crashes
*/
void function(){
    var_ptr = NULL;
}

void main(){
    function();
}

With the above file, run:
frama-c -cpp-command 'gcc -C -E -x c' -pp-annot -wp logic_assigns.c

and the following output is received:
[kernel] preprocessing with "gcc -C -E -x c -dD logic_assigns.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] failure: Non-assignable term (the_var{Pre})
[kernel] Current source was: logic_assigns.c:15
         The full backtrace is:
         Raised at file "src/kernel/log.ml", line 524, characters 30-31
         Called from file "src/kernel/log.ml", line 518, characters 9-16
         Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
         Called from file "src/wp/Context.ml", line 31, characters 12-17
         Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
         Called from file "src/wp/LogicSemantics.ml", line 786, characters 21-75
         Called from file "list.ml", line 57, characters 20-23
         Called from file "src/wp/LogicSemantics.ml", line 808, characters 27-51
         Called from file "src/wp/cfgWP.ml", line 412, characters 6-147
         Called from file "src/wp/Warning.ml", line 155, characters 14-18
         Called from file "src/wp/cfgWP.ml", line 468, characters 22-126
         Called from file "src/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
         Called from file "src/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
         Called from file "src/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
         Called from file "src/wp/Context.ml", line 68, characters 14-17
         Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
         Called from file "src/wp/calculus.ml", line 334, characters 27-62
         Called from file "src/wp/calculus.ml", line 341, characters 23-45
         Called from file "src/wp/calculus.ml", line 613, characters 20-43
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 586, characters 20-43
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 589, characters 20-43
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 589, characters 20-43
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 579, characters 20-43
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 574, characters 20-43
         Called from file "src/wp/calculus.ml", line 536, characters 19-40
         Called from file "src/wp/calculus.ml", line 699, characters 40-59
         Called from file "set.ml", line 288, characters 38-41
         Called from file "map.ml", line 169, characters 20-25
         Called from file "map.ml", line 169, characters 10-18
         Called from file "map.ml", line 169, characters 10-18
         Called from file "src/wp/calculus.ml", line 699, characters 4-64
         Called from file "src/wp/calculus.ml", line 745, characters 19-51
         Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62
         Called from file "src/lib/bag.ml", line 96, characters 16-24
         Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837
         Called from file "src/wp/Model.ml", line 111, characters 17-20
         Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
         Called from file "src/wp/Model.ml", line 117, characters 19-36
         Called from file "src/wp/register.ml", line 435, characters 17-42
         Called from file "src/wp/register.ml", line 574, characters 17-24
         Re-raised at file "src/wp/register.ml", line 578, characters 29-31
         Called from file "src/wp/register.ml", line 575, characters 17-24
         Re-raised at file "src/wp/register.ml", line 579, characters 32-34
         Called from file "src/wp/register.ml", line 575, characters 17-24
         Re-raised at file "src/wp/register.ml", line 579, characters 32-34
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 37, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 214, characters 4-8

         Plug-in wp aborted: internal error.
         Please report as 'crash' at http://bts.frama-c.com/. [^]
         Your Frama-C version is Neon-20140301.
         Note that a version and a backtrace alone often do not contain enough
         information to understand the bug. Guidelines for reporting bugs are at:
         http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines [^]

Tags

No tags attached.

Attached Files

logic_assigns.c [^] (228 bytes) 2014-05-28 22:13 [Show Content] [Hide Content]

#include <stddef.h>

int *var_ptr;

/*@
    logic int *the_var = var_ptr;
*/

/*@
    //assigns var_ptr;  // Works
    assigns the_var;    // WP Crashes
*/
void function(){
    var_ptr = NULL;
}

void main(){
    function();
}

Relationships

Notes
(0005173) virgile (developer) 2014-05-29 13:19	Arguably, the issue lies in the kernel, that should not allow in assigns clause a logic variable which by definition is immutable. On the contrary, assigns *the_var; would be a perfectly valid clause. (NB: the_var in fact depends on the program state's, but you still can't modify it as a logic variable, you can only assign var_ptr).

(0005178) correnson (manager) 2014-06-02 14:07	Transform to user-error

(0005179) correnson (manager) 2014-06-02 14:27	Fix committed to master branch.

Issue History
Date Modified	Username	Field	Change
2014-05-28 22:13	Ian	New Issue
2014-05-28 22:13	Ian	Status	new => assigned
2014-05-28 22:13	Ian	Assigned To	=> correnson
2014-05-28 22:13	Ian	File Added: logic_assigns.c
2014-05-29 13:13	virgile	Assigned To	correnson => virgile
2014-05-29 13:19	virgile	Note Added: 0005173
2014-05-29 13:19	virgile	Category	Plug-in > wp => Kernel > ACSL implementation
2014-06-02 10:40	correnson	Status	assigned => closed
2014-06-02 10:40	correnson	Assigned To	virgile => correnson
2014-06-02 10:40	correnson	Resolution	open => no change required
2014-06-02 14:07	correnson	Note Added: 0005178
2014-06-02 14:07	correnson	Status	closed => assigned
2014-06-02 14:27	correnson	Note Added: 0005179
2014-06-02 14:27	correnson	Status	assigned => resolved
2014-06-02 14:27	correnson	Resolution	no change required => fixed
2015-03-17 22:17	signoles	Fixed in Version	=> Frama-C Sodium
2015-03-17 22:17	signoles	Status	resolved => closed