Frama-C Bug Tracking System - Frama-C
View Issue Details
0000617Frama-CPlug-in > jessiepublic2010-10-26 15:442010-11-17 12:34
Frama-C Boron-20100401 
0000617: assigns nothing ?
Hi, 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
No tags attached.
Issue History
2010-10-26 15:44jnarbouxNew Issue
2010-10-26 15:44jnarbouxStatusnew => assigned
2010-10-26 15:44jnarbouxAssigned To => cmarche
2010-10-26 17:00pascalNote Added: 0001253
2010-11-15 12:23cmarcheNote Added: 0001279
2010-11-15 12:23cmarcheStatusassigned => confirmed
2010-11-17 12:34cmarcheSeveritymajor => minor

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.
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.