Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000617Frama-CPlug-in > jessiepublic2010-10-26 15:442010-11-17 12:34
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000617: assigns nothing ?
DescriptionHi, Using the following example: /*@ ensures \result == 1; assigns \nothing; */ int foo() { int v[9]; v[0] =1; return 1; } I get: [kernel] preprocessing with "gcc -C -E -I. -dD bug.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir bug.jessie [jessie] File bug.jessie/bug.jc written. [jessie] File bug.jessie/bug.cloc written. [jessie] Calling Jessie tool in subdir bug.jessie Generating Why function foo [jessie] Calling VCs generator. gwhy-bin [...] why/bug.why Computation of VCs... File "why/bug.why", line 392, characters 20-42: Unbound variable int_P_v_1_alloc_table make: *** [bug.stat] Erreur 1 is it normal ? if I remove the assign nothing it works. Julien Narboux
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
pascal (reporter)
2010-10-26 17:00

Workaround: you can verify this program with the assigns clause by inserting # pragma SeparationPolicy(none) at the top of the file. Tested with Why 2.26, Frama-C Boron.
cmarche (developer)
2010-11-15 12:23

This is one of the problems with the separation analysis when memory allocation occur, either on the heap or on the stack. The workaround is to deactivate it, as Pascal suggests.

- Issue History
Date Modified Username Field Change
2010-10-26 15:44 jnarboux New Issue
2010-10-26 15:44 jnarboux Status new => assigned
2010-10-26 15:44 jnarboux Assigned To => cmarche
2010-10-26 17:00 pascal Note Added: 0001253
2010-11-15 12:23 cmarche Note Added: 0001279
2010-11-15 12:23 cmarche Status assigned => confirmed
2010-11-17 12:34 cmarche Severity major => minor

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker